Now let’s extend the language of PA by a constant symbol K, and define PAK := Peano Arithmetic (actually, the natural extension of PA to this new language) + for all formulas ‘C’ of the base language: “if PA(K) proves ‘C’, then C”.
Either I didn’t understand how PA(K) is constructed at all, or this instantly dies by Lob’s Theorem. If any language L proves ‘If L proves C, then C’, then L proves C. So if PA(K) has “If PA(K) proves 2=1, then 2=1” then PA(K) proves 2=1.
My understanding is that, confusingly, PA(K) =/= PAK. PA(K) is defined such that, if K=n, then PA(K)=PA(n) defined earlier. PAK is defined in terms of PA(K).
(Rereads.) I don’t feel like I’ve been handed a construction of PA(K), just some properties it’s supposed to have. We have a constant language, containing one constant symbol, that allegedly becomes equal to PA(SSS0) the moment you add one axiom that says SSS0=K. All the PA(n) are different languages with different axioms, the larger n having strictly more axioms. You can define PA(w) by schematizing all the axioms for every n, but if PA(K) is using some larger axiom schema like this, I’d like to know exactly what that larger schema is. It is not obvious to me how to fill in this blank so that PAK becomes effectively equal to PA(n+1) when an axiom K=n is added. In particular there are questions like whether the expression (K-1) can appear in a proof, and so on. I’m being told that PAK can prove things that PA(4) can’t, but becomes only as strong as PA(4) when the axiom K=4 is added. That’s a bit suspicious; why can’t I prove the same things again, just not using that axiom? If it’s only equal over the base language, then what new things can be proven in the extended language, using which axioms?
Would anyone care to write out a concrete example of what this language is supposed to do when generating new AIs? As it stands I can’t visualize the language itself.
K was just said to be a constant symbol, but fine.
PA_K is supposed to be a new name, not some vector PA indexed by K. But that’s just notation, and I agree it was a bad choice.
PAK has just been defined, allegedly, but if PA(K) != PAK then I have no idea what PA(K) is, for it was not defined.
PA(.) is a function that takes a number and returns an axiom system (formalized presumably in the form of a recursive enumeration the axioms). On the metalevel, writing PA(K) makes no sense, since you can only apply PA(.) to a number, and on the metalevel, K doesn’t denote a number, only a symbol.
However, you can formalize the function PA(.) in the language of Peano Arithmetic, and if you extend that language by a constant symbol K, you can apply this formalized version of the function to this constant symbol. PA_K is Peano Arithmetic (in the language with K) extended by the axiom schema “If PA(K) proves ‘C’, then C.” Here C ranges over the statements of the base language, and ‘C’ is its Gödel number (written as a unary literal). PA(K) is the object-level recursive enumeration given by the formalized function PA(.) applied to the constant symbol K; it should be standard that given a recursive enumeration of axioms, you can formalize in the language of PA the assertion that a particular number (‘C’) is the Gödel number of a theorem that follows from these axioms.
I don’t see how you can have a constant language, containing one constant symbol, that becomes equal to PA(SSS0) the moment you add one axiom that says SSS0=K.
[Nit: A language cannot be equivalent to a proof system, but I assume that you can’t see how you can have a proof system P in the extended language that becomes equivalent to PA(SSS0) the moment that axiom is added.] That challenge is trivial: let P be the set of axioms {”SSS0=K implies A” | A an axiom of PA(SSS0)}. I’m doing something different, but still.
Would anyone care to write out a concrete example of what this language is supposed to do when generating new AIs? As it stands I can’t visualize the language itself.
I think if the above didn’t help, it might be more helpful for me to first do a writeup of my now-hopefully-fixed proof, since the new version is simpler and IMO provides much better intuition (I at least now feel like I understand what’s going on here in a way that I didn’t quite before); I’ll have to replace PA_K by yet another proof system, and I’ll make my metalanguage more explicit about quoting/unquoting when writing it up, so it might be more useful to have that as the starting base before digging into details.
ETA:
Details are often important in reflective reasoning, I’ve found. In particular there are questions like whether the expression (K-1) can appear in a proof, and so on.
The more precise metalanguage will hopefully also help with this.
Does the following language do the same thing as PAK?
PAS = PA + schema over Formulas of one variable:
- For all N, for all P:
-- if P proves-in-PAS 'Formula(N+1)', then Formula(N)
(Actually, on second thought, I retract that, you do want the special symbol so that proving 4 > 3 doesn’t get you 3 > 3. But now I need to see if the same problem applies to the original logic as soon as you add K=3...)
if x proves “p is safe for K steps”, then inst(n,x) is a PA(n+1) proof of “p is safe for n steps”
Only if we redefine PA(n) so that e.g. PA(3) is defined in terms of a PA(.) schema and contains an axiom schema stating provable(PA(3), ‘x’)->x; and then redefine PAK accordingly. (This seems possible, but it’s definitely an extra step that for all I know could trip up somewhere, and ought to be stated explicitly.) If we don’t take it, then inst(n, x) gives us something that seems like it ought to be provable by analogy, but isn’t a direct translation, because the original PA(n) didn’t contain a provability formula quantified over PA(.) into which we could plug K=n; and since I think we were proving things about inst later, that’s not good.
Only if we redefine PA(n) so that e.g. PA(3) is defined in terms of a PA(.) schema and contains an axiom schema stating provable(PA(3), ‘x’)->x; and then redefine PAK accordingly.
But that’s not a redefinition—that was the definition! [ETA: except you need PA(2) instead of PA(3) in the provable(_,_) predicate, of course.]
Either I didn’t understand how PA(K) is constructed at all, or this instantly dies by Lob’s Theorem. If any language L proves ‘If L proves C, then C’, then L proves C. So if PA(K) has “If PA(K) proves 2=1, then 2=1” then PA(K) proves 2=1.
PAK != PA(K)
PAK is the language that Benja is defining there, while PA(K) is just the Kth-level PA in the PA hierarchy.
That’s exactly right, and Will_Sawin is right about it being confusing—perhaps I should have used a more creative name for PA_K.
My understanding is that, confusingly, PA(K) =/= PAK. PA(K) is defined such that, if K=n, then PA(K)=PA(n) defined earlier. PAK is defined in terms of PA(K).
(Rereads.) I don’t feel like I’ve been handed a construction of PA(K), just some properties it’s supposed to have. We have a constant language, containing one constant symbol, that allegedly becomes equal to PA(SSS0) the moment you add one axiom that says SSS0=K. All the PA(n) are different languages with different axioms, the larger n having strictly more axioms. You can define PA(w) by schematizing all the axioms for every n, but if PA(K) is using some larger axiom schema like this, I’d like to know exactly what that larger schema is. It is not obvious to me how to fill in this blank so that PAK becomes effectively equal to PA(n+1) when an axiom K=n is added. In particular there are questions like whether the expression (K-1) can appear in a proof, and so on. I’m being told that PAK can prove things that PA(4) can’t, but becomes only as strong as PA(4) when the axiom K=4 is added. That’s a bit suspicious; why can’t I prove the same things again, just not using that axiom? If it’s only equal over the base language, then what new things can be proven in the extended language, using which axioms?
Would anyone care to write out a concrete example of what this language is supposed to do when generating new AIs? As it stands I can’t visualize the language itself.
PA_K is supposed to be a new name, not some vector PA indexed by K. But that’s just notation, and I agree it was a bad choice.
PA(.) is a function that takes a number and returns an axiom system (formalized presumably in the form of a recursive enumeration the axioms). On the metalevel, writing PA(K) makes no sense, since you can only apply PA(.) to a number, and on the metalevel, K doesn’t denote a number, only a symbol.
However, you can formalize the function PA(.) in the language of Peano Arithmetic, and if you extend that language by a constant symbol K, you can apply this formalized version of the function to this constant symbol. PA_K is Peano Arithmetic (in the language with K) extended by the axiom schema “If PA(K) proves ‘C’, then C.” Here C ranges over the statements of the base language, and ‘C’ is its Gödel number (written as a unary literal). PA(K) is the object-level recursive enumeration given by the formalized function PA(.) applied to the constant symbol K; it should be standard that given a recursive enumeration of axioms, you can formalize in the language of PA the assertion that a particular number (‘C’) is the Gödel number of a theorem that follows from these axioms.
[Nit: A language cannot be equivalent to a proof system, but I assume that you can’t see how you can have a proof system P in the extended language that becomes equivalent to PA(SSS0) the moment that axiom is added.] That challenge is trivial: let P be the set of axioms {”SSS0=K implies A” | A an axiom of PA(SSS0)}. I’m doing something different, but still.
I think if the above didn’t help, it might be more helpful for me to first do a writeup of my now-hopefully-fixed proof, since the new version is simpler and IMO provides much better intuition (I at least now feel like I understand what’s going on here in a way that I didn’t quite before); I’ll have to replace PA_K by yet another proof system, and I’ll make my metalanguage more explicit about quoting/unquoting when writing it up, so it might be more useful to have that as the starting base before digging into details.
ETA:
The more precise metalanguage will hopefully also help with this.
Try two:
Does the following language do the same thing as PAK?
Ha! I’m not sure what the exact relation to PAK is, but PAT is almost exactly what I’m using in my new proof:
(“PPT” for “parametric polymorphism trick, v 0.2″.) [ETA: added “K>0” condition.]
PAK proves all which your PAT does, but probably not the other way around.
I think this bit is all that’s strictly necessary in the proof though.
Does the following language do the same thing as PAK?
(Actually, on second thought, I retract that, you do want the special symbol so that proving 4 > 3 doesn’t get you 3 > 3. But now I need to see if the same problem applies to the original logic as soon as you add K=3...)
(Still trying to read, will comment as I go.)
Only if we redefine PA(n) so that e.g. PA(3) is defined in terms of a PA(.) schema and contains an axiom schema stating provable(PA(3), ‘x’)->x; and then redefine PAK accordingly. (This seems possible, but it’s definitely an extra step that for all I know could trip up somewhere, and ought to be stated explicitly.) If we don’t take it, then inst(n, x) gives us something that seems like it ought to be provable by analogy, but isn’t a direct translation, because the original PA(n) didn’t contain a provability formula quantified over PA(.) into which we could plug K=n; and since I think we were proving things about inst later, that’s not good.
But that’s not a redefinition—that was the definition! [ETA: except you need PA(2) instead of PA(3) in the provable(_,_) predicate, of course.]