22 views

Skip to first unread message

May 4, 2020, 2:15:08 AM5/4/20

to Calculational Mathematics

Hi Jeremy,

Would it be fair to view

P

!= {...}

Q

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

Agape,

Eric

May 4, 2020, 8:09:13 AM5/4/20

to calculationa...@googlegroups.com

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.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu