Question about Godel's 2nd Theorem

[lugita15]

Let Con(PA) be the sentence of arithmetic which translates as "Peano Arithmetic is consistent." Then according to Godel's 2nd incompleteness theorem, assuming PA is consistent then PA can neither prove Con(PA) nor its negation. And in fact, if T contains PA and T is (omega-) consistent, then T can neither prove Con(T) nor its negation. In particular, if PA+Con(PA) is consistent then PA+Con(PA) can neither prove Con(PA+Con(PA)) nor its negation.

But consider the following piece of reasoning: if PA is consistent, then Con(PA) is true, so PA+Con(PA) is consistent, so Con(PA+Con(PA)) is true. My question is, why can't this reasoning by formalized in PA, so that within PA you can prove Con(PA) implies Con(PA+Con(PA))? If you could prove that, then since you can obviously prove Con(PA) within PA+Con(PA), you would be able to prove Con(PA+Con(PA)) within PA+Con(PA), which is a contradiction. So where am I going wrong?

We can even talk about this in terms of model theory. There are nonstandard models of PA in which Con(PA) does not hold: basically, you have infinitely large natural numbers, and you have infinitely long proofs of a contradiction in PA. This does not mean that PA is inconsistent, because there are no proofs of finite length of this contradiction. So are there also nonstandard models of PA+Con(PA) in which Con(PA+Con(PA)) does not hold?

Any help would be greatly appreciated.

Thank You in Advance.

 

[Citan Uzuki]

Then according to Godel's 2nd incompleteness theorem, assuming PA is consistent then PA can neither prove Con(PA) nor its negation.

Not quite. Godel's theorem implies that if PA is consistent then PA cannot prove Con(PA), but to show that PA cannot prove ¬Con(PA) requires ω-consistency. Similarly, showing PA+Con(PA) cannot prove ¬Con(PA+Con(PA)) also requires ω-consistency.

But consider the following piece of reasoning: if PA is consistent, then Con(PA) is true, so PA+Con(PA) is consistent, so Con(PA+Con(PA)) is true. My question is, why can't this reasoning by formalized in PA, so that within PA you can prove Con(PA) implies Con(PA+Con(PA))?

Because truth is not definable in PA, or any consistent extension of it. So you cannot even state "Con(PA+Con(PA)) is true" in PA.

So are there also nonstandard models of PA+Con(PA) in which Con(PA+Con(PA)) does not hold?

Yes.

 

[Preno]

Not quite. Godel's theorem implies that if PA is consistent then PA cannot prove Con(PA), but to show that PA cannot prove ¬Con(PA) requires ω-consistency. Similarly, showing PA+Con(PA) cannot prove ¬Con(PA+Con(PA)) also requires ω-consistency.

Technically true, but neither premise is needed - PA is true, hence a fortiori it is (ω-)consistent.

Because truth is not definable in PA, or any consistent extension of it. So you cannot even state "Con(PA+Con(PA)) is true" in PA.

It is the case that you cannot define a single truth predicate in PA which would cover arbitrary sentences, but you can define a sequence of truth predicates in PA for sentences of bounded complexity (Σ_n-sentences). So the question is well-posed.

The problem is, however, that such truth predicates behave just as non-standardly in non-standard models as provability predicates such as Con do.