Thanks for digging deeper! This is much easier to answer: PA_K does not prove PA(1) consistent. As I noted at the end of the post, it’s conservative over PA(1), which means that it proves a sentence in the base language only if PA(1) does. The reason is that if C is a sentence in the base language and x is a proof of it, then inst(1,x) is a proof of inst(1,C), but since C doesn’t contain any occurrences of K, inst(1,C) = C.
At the very least, it looks like your third note should be removed.
It is easy to prove that PA(n) is monotonically growing in strength.
By induction, PA(0) is inside PA(K). It is even obvious in PA_K.
PA_K proves “PA(K) proves ‘falsehood’ implies ‘falsehood’”, as ‘falsehood’ is a constant falsehood without reference to K, and is in the base language.
PA_K proves “PA(0) proves ‘falsehood’ implies PA(K) proves ‘falsehood’, which implies ’falsehood”, by provable monotonicity.
PA_K proves “PA(0) is consistent”, because I just collapse the logical steps in the previous statement.
PA_K proves “K=0 or PA(1) is consistent”, by analogy.
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’).”
(direct quote, hopefully understood correctly)
‘falsehood’ is a formula and it doesn’t change under substitutions. So, “PA_K proves ‘falsehood’ implies PA(1) proves ‘falsehood’”
So we can combine PA_K-PA(1) relation and PA(1) conditional consistency and get:
PA_K proves: “K=0 or PA_K is consistent”
So if PA_K says K>10, we have a huge problem here.
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.
Thanks for digging deeper! This is much easier to answer: PA_K does not prove PA(1) consistent. As I noted at the end of the post, it’s conservative over PA(1), which means that it proves a sentence in the base language only if PA(1) does. The reason is that if C is a sentence in the base language and x is a proof of it, then inst(1,x) is a proof of inst(1,C), but since C doesn’t contain any occurrences of K, inst(1,C) = C.
Does that help?
Not much yet.
At the very least, it looks like your third note should be removed.
It is easy to prove that PA(n) is monotonically growing in strength.
By induction, PA(0) is inside PA(K). It is even obvious in PA_K.
PA_K proves “PA(K) proves ‘falsehood’ implies ‘falsehood’”, as ‘falsehood’ is a constant falsehood without reference to K, and is in the base language.
PA_K proves “PA(0) proves ‘falsehood’ implies PA(K) proves ‘falsehood’, which implies ’falsehood”, by provable monotonicity.
PA_K proves “PA(0) is consistent”, because I just collapse the logical steps in the previous statement.
PA_K proves “K=0 or PA(1) is consistent”, by analogy.
PA_K proves:
(direct quote, hopefully understood correctly)
‘falsehood’ is a formula and it doesn’t change under substitutions. So, “PA_K proves ‘falsehood’ implies PA(1) proves ‘falsehood’”
So we can combine PA_K-PA(1) relation and PA(1) conditional consistency and get:
PA_K proves: “K=0 or PA_K is consistent”
So if PA_K says K>10, we have a huge problem here.
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.