= 27d567bc2d48d9f40e9ccc20ea370b15)
gjm comments on A proof of Löb's theorem in Haskell - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (8)
Nice!
I had the impression that in some sense the existence of the fixpoint was the core of the theorem; unless I've misunderstood, the proof here simply assumes it's given. Is it in fact straightforward (albeit inconvenient) to add the necessary fixpoint-making machinery to the proof?
You can choose how deep you want to go:
1) Assume the existence of one particular fixpoint. That's what I've done in the post.
2) Assume the existence of fixpoints for all formulas with one propositional variable, and get (1) as an immediate corollary. That's not straightforward in Haskell because there are no type-level lambdas, but it's easy in Agda.
3) Actually spell out a proof of (2), which is known as the diagonal lemma. You could probably do that in Agda, but I haven't tried and haven't seen anyone try. Also it's not obvious which assumptions to use. Ideally we'd want a full account of Gödel numberings, but that would be a lot of work.