A question regarding JAW88

[Eric Macaulay]

Hi Jeremy,

Would it be fair to view

    P

!=    {...}

    Q

as a proof of ¬[¬(P=Q)] ?

Agape,

Eric

[Jeremy Weissmann]

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

On May 4, 2020, at 02:15, Eric Macaulay <elih...@gmail.com> wrote:



--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/a8e75d90-b888-4ac9-8282-304d89ce1b7e%40googlegroups.com.