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