It appears to me that for the GM to execute a change that switches to a new theorem-prover or proof-verifier, the Gödel Machine must prove that if the proof-verifier
accepts P, then P.
The verifier has to translate a meta-language result into an object-language result.
Löb’s Theorem establishes that for any proof system capable of encoding its own proof process, |- Provable(‘P’) → P if and only if |- P.
But if an AI does believe that (AI |- P) → P, Löb’s construction permits an automatic proof of P
You didn’t write it out like this, but I’m going to guess that in the first quote you mean: For GM to change its verifier, V1, to V2, GM.V1 must prove that for all C of interest, if “C is provable by GM.V2” then C. More pithily, we need ∀C: V1 |- ◻_V2(C) → C. If we add that V2 is logically equivalent to V1, that reduces to ∀C:V |-[]C->C, which we obviously can’t have as an axiom because of Lob. Setting them equivalent makes ◻_V2(C) into a meta-language result, which you claimed it was, so I’m guessing that’s also what you’re doing.
However, the first quote has a different interpretation than “∀C: V1 |- ◻_V2(C)-> C”, and it seems to work. It requires we stop talking about the old modal provability predicate, []X, which might be read as “there exists some term a la godel numbering that encodes a proof of X”, or ∃t:proof(t,#X). Instead of a predicate that aks whether there exists a term t, we use a predicate that asks whether a specific t encodes a proof of X, proof(t,#X). I’ll write that as [[t]]X, after S. Artemov work on such intuitionist / justificational logic. I’ve been told that Artemov’s results are too messy and might not establish what he attemps, so I’ll just mention him name, skip the citations, and present the part that makes sense to me so far. I’d really like to know whether it makes sense to you too.
Instead of the reflection principle, |-◻C->C, which is nice and easy and darn that Lob for taking it from us, we use |-[[t]]C → C. which is roughly as nice! I still haven’t entirely grokked why we can have []C and yet not derive C, but I would be down right shocked if we couldn’t infer C from a proof which gives C. That might not be a “wrap around the towers of meta”-type Inference of Awesome, but it makes sense without having to do magic; it’s the sort of thing I would expect that humans are actually doing in their heads. And of course, when we have [[t]]C, then we will have []C. Maybe Lob just confuses me because I do an attribute substitution from []C to [[t]]C!
With this new predicate in mind, we can now we can write a modified version of what we want the GM to prove. Actually, mathematical logic is still ridiculously new to me, so I’m not very confident the following is right, but I really think that something like this is right: For GM.V1 to rewrite V1 to V2, at the very least we want GM.V1 to prove that for all statements of interest C, if we have constructed a term t which encodes of proof for C from V2, then some magic Gödelian procedure allows us to transform t into s, a new term which encodes a proof of C from V1. If V2 is logically equivalent to V1 then t should work as our s, and we can juxt say ∀C: V1 |- [t]-> C, the old principle of “believe once it’s proved, not once it’s proved provable”.
Now we can add inference rules to LCF-style provers once we prove them, without having to just expand macros that synthesize the primitive inference rules. We might even be able to transform deductive systems like PA into more powerful ones like ZF provided the AI has some non-logical ability to judge usefullness and there actually is such a magic Gödelian procedure that ensures our funny little half-meta-reflexive soundness criterion.
P2 constructs a t which encodes a proof for q from P2, then procedure x allows us to transform t into z, which encodes a proof of q from P1
You once wrote on the SL4 mailing list
You didn’t write it out like this, but I’m going to guess that in the first quote you mean: For GM to change its verifier, V1, to V2, GM.V1 must prove that for all C of interest, if “C is provable by GM.V2” then C. More pithily, we need ∀C: V1 |- ◻_V2(C) → C. If we add that V2 is logically equivalent to V1, that reduces to ∀C:V |-[]C->C, which we obviously can’t have as an axiom because of Lob. Setting them equivalent makes ◻_V2(C) into a meta-language result, which you claimed it was, so I’m guessing that’s also what you’re doing.
However, the first quote has a different interpretation than “∀C: V1 |- ◻_V2(C)-> C”, and it seems to work. It requires we stop talking about the old modal provability predicate, []X, which might be read as “there exists some term a la godel numbering that encodes a proof of X”, or ∃t:proof(t,#X). Instead of a predicate that aks whether there exists a term t, we use a predicate that asks whether a specific t encodes a proof of X, proof(t,#X). I’ll write that as [[t]]X, after S. Artemov work on such intuitionist / justificational logic. I’ve been told that Artemov’s results are too messy and might not establish what he attemps, so I’ll just mention him name, skip the citations, and present the part that makes sense to me so far. I’d really like to know whether it makes sense to you too.
Instead of the reflection principle, |-◻C->C, which is nice and easy and darn that Lob for taking it from us, we use |-[[t]]C → C. which is roughly as nice! I still haven’t entirely grokked why we can have []C and yet not derive C, but I would be down right shocked if we couldn’t infer C from a proof which gives C. That might not be a “wrap around the towers of meta”-type Inference of Awesome, but it makes sense without having to do magic; it’s the sort of thing I would expect that humans are actually doing in their heads. And of course, when we have [[t]]C, then we will have []C. Maybe Lob just confuses me because I do an attribute substitution from []C to [[t]]C!
With this new predicate in mind, we can now we can write a modified version of what we want the GM to prove. Actually, mathematical logic is still ridiculously new to me, so I’m not very confident the following is right, but I really think that something like this is right: For GM.V1 to rewrite V1 to V2, at the very least we want GM.V1 to prove that for all statements of interest C, if we have constructed a term t which encodes of proof for C from V2, then some magic Gödelian procedure allows us to transform t into s, a new term which encodes a proof of C from V1. If V2 is logically equivalent to V1 then t should work as our s, and we can juxt say ∀C: V1 |- [t]-> C, the old principle of “believe once it’s proved, not once it’s proved provable”.
Now we can add inference rules to LCF-style provers once we prove them, without having to just expand macros that synthesize the primitive inference rules. We might even be able to transform deductive systems like PA into more powerful ones like ZF provided the AI has some non-logical ability to judge usefullness and there actually is such a magic Gödelian procedure that ensures our funny little half-meta-reflexive soundness criterion.
P2 constructs a t which encodes a proof for q from P2, then procedure x allows us to transform t into z, which encodes a proof of q from P1