Puzzle: Does the following prove that PA is inconsistent?

Let PA mean the Peano axioms, let Con(PA) mean that the Peano axioms are consistent, and let Incon(PA) mean that the Peano axioms are inconsistent.

Godel's 2nd Incompleteness Theorem says that Con(PA) is not a theorem of PA, unless PA is inconsistent. Now consider the following argument that Con(PA) is a theorem of PA:

(PA and Incon(PA)) implies Con(PA), since (PA and Incon(PA)) is a contradiction, and a contradiction implies anything.

(PA and Con(PA)) implies Con(PA), obviously.

Therefore, [(PA and Incon(PA)) or (PA and Con(PA))] implies Con(PA).

Then since PA is logically equivalent to [(PA and Incon(PA)) or (PA and Con(PA))], we can conclude that PA implies Con(PA).

Therefore, by Godel's 2nd Incompleteness Theorem, PA is inconsistent.

Where is the error? There has to be an error, or else all of mathematics is wrong.

• I suppose the first does not work. From jsut "knownig" that PA is incosistent, you do not obtian a speicic proof of some $P\land \neg P$ – Hagen von Eitzen Feb 28 '17 at 17:55
• Your argument that "(PA and Incon(PA)) implies Con(PA)" does not appear to make sense. If you're assuming PA and Incon(PA), then you're working in a structure that is not the usual natural numbers; that structure thinks PA has a proof of Con(PA), but the fact that some non-standard structure thinks Con(PA) has a proof does not mean that Con(PA) is true in that non-standard structure. – Henning Makholm Feb 28 '17 at 17:55

The error is when you write

(PA and Incon(PA)) implies Con(PA), since if PA is inconsistent, PA implies that everything is both true and false.

All that (PA and Incon(PA)) implies is that PA proves Con(PA) (if PA were inconsistent, would you really believe that therefore 0=1?); and this is true internally to PA as well. That is, PA proves $$(*)\quad\mbox{If I am inconsistent, then I prove Con(PA),}$$

but PA does not prove $$(**)\quad\mbox{If I am inconsistent, then Con(PA)}.$$

That is, PA does not know that it is sound: in general, for most sentences $\varphi$, PA does not prove "If PA proves $\varphi$ then $\varphi$ is true." In fact, by Lob's theorem the only sentences for which PA proves this are the ones which PA already proves to be true!

Note that by turning your argument around, you in fact prove:

If PA is consistent, then so is PA+Incon(PA).

Relatedly, in the same way that iterated consistency principles can be used to provide a hierarchy of extensions of PA, iterated soundness principles also provide such a hierarchy (although they are usually called reflection principles in this context). So not only does PA not prove its own soundness (even for $\Sigma^0_1$ sentences!), but it is so far from proving its own soundness that adding soundness principles to it can yield tons of additional strength.

• I made the sentence that you quoted clearer. – Craig Feinstein Feb 28 '17 at 18:22
• @CraigFeinstein It's still wrong - again, the issue is that PA does not prove "if I am inconsistent, then [arbitrary sentence] is true," it just proves "if I am inconsistent, then [arbitrary sentence] is provable." – Noah Schweber Feb 28 '17 at 18:25
• I don't understand. Why isn't PA + Incon(PA) a contradiction? If Incon(PA) is true, then PA is false. – Craig Feinstein Feb 28 '17 at 18:47
• @CraigFeinstein For simplicity, let's switch from PA to a finitely axiomatizable theory T to which Goedel's theorems apply (plenty of these exist, e.g. ACA_0). I'm making this switch since there are technical oddities that can crop up when talking about non-finitely-axiomatiable theories, which are interesting but get in the way of this question. What you're really asking is: "How can S=T+Incon(T) be consistent?" Well, try to prove 0=1 in S; how would you do it? S can prove "I prove 0=1", but there's no way in S to transform this into an outright proof of 0=1 (cont'd) – Noah Schweber Feb 28 '17 at 18:59
• since S doesn't prove its own soundness. That is, S can't prove "the things I prove are true." The argument "If S is true, then S is consistent" sounds trivial, but if we unravel it it amounts to a claim of soundness: how do we know that a true theory only proves true things? Note that this sounds like a general principle which a sufficiently strong theory ought to prove; however, it crucially makes use of the general notion of truth, and Tarski's theorem gets in the way of even stating it. – Noah Schweber Feb 28 '17 at 19:05

$PA+Incon(PA)$ does not prove that $Con(PA)$. What we have is that if $PA$ is inconsistent then it proves $Con(PA)$ (or that if $PA$ proves $Incon(PA)$ then it also proves $Con(PA)$). These two statements are different.

You're mixing up to different meanings of "inconsistent".

Let $\operatorname{Provable(X)}$ be "$X$ encodes a provable statement".

For any proposition $P$, let $\ulcorner P \urcorner$ be the encoding of $P$ as an integer. There is a theorem:

Theorem If $P$ is provable, then $PA$ implies $\operatorname{Provable(\ulcorner P \urcorner)}$

A proof sketch of this theorem is

• Take any proof of $P$
• Encode the proof as a natural number
• Construct that natural number in $PA$

Your mistake is assuming the converse holds as well. In particular, from $PA \text{ and } \operatorname{Provable(\operatorname{Incon}(PA))}$, one cannot conclude that $PA$ is inconsistent.

Roughly speaking, the problem is that first-order logic does not prove the infinitary theorem $x = 0 \vee x = 1 \vee x = 2 \vee \cdots$; thus, if some model of $PA$ has a number encoding a proof of $\ulcorner P \urcorner$, one cannot assume said number is actually a natural number1, which means we cannot assume that it can be decoded into a proof of $P$.

Put differently, in any model of $PA \wedge \operatorname{Incon}(PA)$, the proof of $\operatorname{Incon}(PA)$ is infinitely long, so it doesn't count as a proof. (the length of the proof is a number in the model, of course, so the model thinks its a finite number, but the model can be nonstandard and have infinitely large numbers)

1: I use "natural number" to refer specifically to the natural numbers appearing in whatever ambient theory we have developed formal logic; e.g. the model given by the decimals