= 27d567bc2d48d9f40e9ccc20ea370b15)
Kutta comments on A quick sketch on how the Curry-Howard Isomorphism kinda appears to connect Algorithmic Information Theory with ordinal logics - LessWrong
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
= f037147d6e6c911a85753b9abdedda8d){kind=logo}
Comments (27)
I'd like to ask a not-too-closely related question, if you don't mind.
A Curry-Howard analogue of Gödel's Second Incompleteness Theorem is the statement "no total language can embed its own interpreter"; see the classic post by Conor McBride. But Conor also says (and it's quite obviously true), that total languages can still embed their coinductive interpreters, for example one that returns in the partiality monad.
So, my question is: what is the logical interpretation of a coinductive self-interpreter? I feel I'm not well-versed enough in mathematical logic for this. I imagine it would have a type like "forall (A : 'Type) -> 'Term A -> Partiality (Interp A)", where 'Type and 'Term denote types and terms in the object language and "Interp" returns a type in the meta-language. But what does "Partiality" mean logically, and is it anyhow related to the Löbstacle?
The logical interpretation of a coinductive self-interpreter is something that says, roughly, "If you keep feeding me computing power, someday I might self-interpret!". And indeed, if you eventually feed it enough compute-power, it will self-interpret. You just wouldn't be able to prove ahead of time that it does so.
"Partiality" in PL terms means "the type contains \Bot, the Bottom element". The Bottom element is the type-theoretic element for representing nontermination.
If you can construct \Bot-the-element, you can prove \Bot-the-type, which is also called False, and implies all other propositions and types by the Principle of Explosion. The Second Incompleteness Theorem roughly says:
"In order to self-verify, you must prove that your proof procedure implements the logic you believe in an infinite number of cases. Normally you could try to do that by induction, but since you only have a finite-sized axiom scheme to go on, while your language is Turing-complete, you will never have enough information to verify every possible proof of every possible theorem via inductive application of your axioms, so you'll have to check some 'by hand.' That will take infinite time, so you'll never finish. Or, if you presume that you did finish, it meant you proved \Bot and thus obtained all other propositions by Explosion."
LoL!