Ancestors

Toot

Written by Andrew Helwer on 2025-01-12 at 17:57

Am I remembering wrong or is there some particular popular essay on why constructive mathematics is the way to go? After working through a weird proof that uses the law of the excluded middle to pop a bunch of propositions into existence out of nowhere I am feeling sympathetic lol

[#]AskFedi #Constructivism

=> More informations about this toot | More toots from ahelwer@discuss.systems

Descendants

Written by Jarrod Urban on 2025-01-12 at 20:18

@ahelwer no matter where in you go in mathematics you will not be able to avoid logic.

Do you mind sharing the proof you were working through?

=> More informations about this toot | More toots from jarrodu@social.tchncs.de

Written by Andrew Helwer on 2025-01-12 at 22:50

@jarrodu it's from page 102 of A Science of Concurrent Programs by Leslie Lamport (https://lamport.azurewebsites.net/tla/science-book.html).

It's an example of how to prove a statement in temporal logic, specifically a "leads to" statement where saying that P leads to Q is denoted P ↝ Q. Other important operators are always (□) and eventually (◇).

=> More informations about this toot | More toots from ahelwer@discuss.systems

Written by Jarrod Urban on 2025-01-13 at 06:32

@ahelwer I took a quick look. It is mostly logic. It would also take me some time to work through it.

Thanks for sharing. It has been a while since I thought about Lamport.

=> More informations about this toot | More toots from jarrodu@social.tchncs.de

Written by Jarrod Urban on 2025-01-13 at 06:43

@ahelwer maybe you can find a reference in the bibliography of this paper.

https://web.archive.org/web/20060209210015/http://staff.science.uva.nl/~anne/hhhist.pdf

If you find anything good. Please let me know. It would be an interesting read for me.

=> More informations about this toot | More toots from jarrodu@social.tchncs.de