At the very least, it looks like your third note should be removed.
From the rest of your comment, I think that’s probably a typo and it’s the second note you’re concerned about? Or I’m misunderstanding?
PA_K proves “K=0 or PA(1) is consistent”, by analogy.
I agree with this and with your proof of it.
PA_K proves: “For all extended-language sentences ‘C’, if PA_K proves ‘C’, then for all n, PA(n+1) proves instPA(n,‘C’).”
...
So if PA_K says K>10, we have a huge problem here.
Right, the assertion you quote would fail in the system proposed in the second note—let’s call it PA_K[2] for short. (And in PA_K itself, you do not have K>10.) Instead, I believe you have
PA_K[2] proves: “For all extended-languange sentences ‘C’, if PA_K[2] proves ‘C’, then there is an m such that for all n>=m, PA(n+1) proves instPA(n,‘C’).”
(In the proof, we fix a proof of ‘C’ and choose m such that if the axiom “K>k” is used in the proof of ‘C’, then m>k.)
It’s quite possible that something else in my proof idea fails if you replace PA_K by PA_K[2], but I’d like to table that question for now while I’m working on trying to fix the proof. (I’m happy to continue talking about the consistency of PA_K[2], if you’re interested in that, I just don’t want to get into whether the proof about AI_K can be modified into a proof for “AI_K[2]” before I’ve figured out whether I can fix the first one.)
Please keep the questions coming, it’s very good to have someone thinking about these things in technical detail.
[ETA: fixed a typo; in the thing that I conjecture PA_K[2] proves, I accidentally wrote ‘PA_K’ instead of ‘PA_K[2]’.]
Yes, I meant that the comment introducing PA_K[2] should be weakened somehow because it is easily understood as something introducing contradictory system.
From the rest of your comment, I think that’s probably a typo and it’s the second note you’re concerned about? Or I’m misunderstanding?
I agree with this and with your proof of it.
Right, the assertion you quote would fail in the system proposed in the second note—let’s call it PA_K[2] for short. (And in PA_K itself, you do not have K>10.) Instead, I believe you have
PA_K[2] proves: “For all extended-languange sentences ‘C’, if PA_K[2] proves ‘C’, then there is an m such that for all n>=m, PA(n+1) proves instPA(n,‘C’).”
(In the proof, we fix a proof of ‘C’ and choose m such that if the axiom “K>k” is used in the proof of ‘C’, then m>k.)
It’s quite possible that something else in my proof idea fails if you replace PA_K by PA_K[2], but I’d like to table that question for now while I’m working on trying to fix the proof. (I’m happy to continue talking about the consistency of PA_K[2], if you’re interested in that, I just don’t want to get into whether the proof about AI_K can be modified into a proof for “AI_K[2]” before I’ve figured out whether I can fix the first one.)
Please keep the questions coming, it’s very good to have someone thinking about these things in technical detail.
[ETA: fixed a typo; in the thing that I conjecture PA_K[2] proves, I accidentally wrote ‘PA_K’ instead of ‘PA_K[2]’.]
Yes, I meant that the comment introducing PA_K[2] should be weakened somehow because it is easily understood as something introducing contradictory system.
Ok, included a warning with a link to our discussion for now.