eli_sennesh comments on A quick sketch on how the Curry-Howard Isomorphism kinda appears to connect Algorithmic Information Theory with ordinal logics - LessWrong

11 [deleted] 19 April 2015 07:35PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (27)

You are viewing a single comment's thread. Show more comments above.

Comment author: [deleted] 29 June 2015 11:11:18PM *  0 points [-]

So, my question is: what is the logical interpretation of a coinductive self-interpreter?

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.

But what does "Partiality" mean logically, and is it anyhow related to the Löbstacle?

"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."