Various diagonal arguments, such as those found in the proofs of the halting theorem, Cantor's theorem, and Gödel‘s incompleteness theorem, are all instances of the Lawvere fixed point theorem

yoooooo

Follow

I feel like it was a lot of work getting to the incompleteness theorem tho
Like Cantor's diagonal argument is just some number trickery and the halting problem's not all that convoluted once you have the idea of a Turing machine down
Incompleteness took me an entire textbook after all

I wanna do my own mechanization of this
Martin Escardo has one I might follow but I'd read Lawvere's paper first
But I wanna do it

@ionchy i replicated one of escardo's proofs and it wasn't that bad

Sign in to participate in the conversation
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.