Well, that would mean “somewhere P == Q”, no? Which roughly means that for some point x in the underlying space, we have P.x == Q.x .
I believe my notation was indicating that the equality was dependent on the scalar context. For example, for punctual, conjunctive f , we can calculate:
|[ Context: x => y
f.x
!= { x == x /\ y , f is punctual }
f.(x /\ y)
== { f is conjunctive }
f.x /\ f.y
]|
which allows us to conclude:
[ (x => y) => (f.x => f.y) ] ,
or that f is punctually monotonic. There’s no way to carry out that first step using the conventions in Chapter 4 (I believe) of Dijkstra and Scholten’s Predicate Calculus and Program Semantics .
It’s been a long, long time since I wrote those JAWs but I’ll re-read the note and let me know if you have more questions.
+j