First, note that PA already (“quickly”) proves “If AIK(p) doubles down, then PA_K proves ‘p is safe for K steps’”. In PA_K, it follows that “If AI_K(p) doubles down, and K>0, then inst(K-1, ‘p is safe for K steps’)”.
It looks like you have moved from “PA_K proves that PA_K proves that p is K-step safe” to “PA_K proves that p is K-step safe” here. This would be adding consistency of entire PA_K to PA_K, which is not allowed.
You probably meant something else, but as it is written I failed to understand this. Could you please
explain?
Ok, first note that here I’m applying what I proved in the whole previous paragraph, so it’s not as easy to explain as one single step of reasoning. That said, the short answer is that what I’ve actually done is to pass from “PA_K proves that PA_K proves that p is K-step safe” to “PA_K proves that p is (K-1)-step safe”: note that inst(K-1, ‘p is safe for K steps’) means that K-1 is substituted for K in the thing in quotes...
...except, there is a problem with that, namely that inst(n,x) was supposed to be a meta-level function that substitutes the numeral corresponding to n for each occurrence of K in x. On the meta-level, (K-1) is just an expression, not a definite value, so this doesn’t work. Argh, I had thought about that problem, but I thought I’d fixed it… I’ll have to think about it & update the post. Thanks!
I’m applying what I proved in the whole previous paragraph, so it’s not as easy to explain as one single step of reasoning
OK
Formalizing the above argument in Peano Arithmetic, and writing instPA(n,x) for the object-level encoding of the meta-level function, we can prove: “For all extended-language sentences ‘C’, if PAK proves ‘C’, then for all n, PA(n+1) proves instPA(n,‘C’).”
Oh, this is the place that I should have pointed out. Sorry.
If I understand this correctly, “PA_K proves that if PA_K proves ‘C’, PA(1) proves instPA(0, ‘C’)”. Also, PA_K should prove all simple things from PA(2), like PA(1) being consistent. Let us consider ‘C’ being plain “falsehood”. Then we shall get “PA_K proves that PA(1) is not contradictory and if PA_K is contradictory, PA(1) is contradictory”. For the benefit of casual reader: this would imply that PA_K contains PA and proves its own consistency, which implies that PA_K is contradictory.
This means I missed something very basic about what goes on here. Could you point out what exactly, please?
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.
It looks like you have moved from “PA_K proves that PA_K proves that p is K-step safe” to “PA_K proves that p is K-step safe” here. This would be adding consistency of entire PA_K to PA_K, which is not allowed.
You probably meant something else, but as it is written I failed to understand this. Could you please explain?
Ok, first note that here I’m applying what I proved in the whole previous paragraph, so it’s not as easy to explain as one single step of reasoning. That said, the short answer is that what I’ve actually done is to pass from “PA_K proves that PA_K proves that p is K-step safe” to “PA_K proves that p is (K-1)-step safe”: note that inst(K-1, ‘p is safe for K steps’) means that K-1 is substituted for K in the thing in quotes...
...except, there is a problem with that, namely that inst(n,x) was supposed to be a meta-level function that substitutes the numeral corresponding to n for each occurrence of K in x. On the meta-level, (K-1) is just an expression, not a definite value, so this doesn’t work. Argh, I had thought about that problem, but I thought I’d fixed it… I’ll have to think about it & update the post. Thanks!
OK
Oh, this is the place that I should have pointed out. Sorry.
If I understand this correctly, “PA_K proves that if PA_K proves ‘C’, PA(1) proves instPA(0, ‘C’)”. Also, PA_K should prove all simple things from PA(2), like PA(1) being consistent. Let us consider ‘C’ being plain “falsehood”. Then we shall get “PA_K proves that PA(1) is not contradictory and if PA_K is contradictory, PA(1) is contradictory”. For the benefit of casual reader: this would imply that PA_K contains PA and proves its own consistency, which implies that PA_K is contradictory.
This means I missed something very basic about what goes on here. Could you point out what exactly, please?
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.