= 27d567bc2d48d9f40e9ccc20ea370b15)
cousin_it comments on A proof of Löb's theorem in Haskell - Less Wrong
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)
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.