How is it possible for PA+¬Con(PA) to be consistent?

Question

I'm having some trouble understanding how a certain first-order theory isn't just straight-up inconsistent.

Let $PA$ be the axioms of (first-order) Peano arithmetic and let $C$ be the following statement:

$\not \exists $ $n$, $n$ is the Gödel Number of a proof that $1 = 0$.

Since $PA$ proves (rather trivially) that $1 \neq 0$, any proof that $1 = 0$ within $PA$ would be a contradiction and hence an inconsistency. On the other hand, any contradiction provable from $PA$ would be able to be used to derive a proof that $1 = 0$ via the principle of explosion. Thus, a statement of the consistency of $PA$ is logically equivalent to $C$.

Suppose that we have an oracle giving that $PA$ is consistent. Then a first-order theory consisting of $PA$ + $\neg C$ must also be consistent because if it weren't, we would have a proof of $C$ from $PA$. This violates the incompleteness theorems. Thus, the consistency of $PA$ implies the consistency of $PA$ + $\neg C$.

On the other hand, $\neg C$ states that there exists some number $n$ such that $n$ encodes a proof of $1 = 0$ in the system of $PA$. This seems, prima facie, like a contradiction. The way that you (apparently) get out of it is to say that while $PA$ + $\neg C$ does state that such a number exists, no particular number with this property will ever be able to be constructed from $PA$ (at least not if $PA$ is consistent) so no contradiction is ever found.

We are also guaranteed that no standard natural number would work so $PA$ + $\neg C$ does not admit the standard model of arithmetic as a model. This is where the name $\omega$-inconsistent comes from, as $\omega$ is a well-recognized symbol for the standard natural numbers.

This seems like a cop-out. Does not the mere existence of such a number (even if we can't construct it, we could name it with a symbol) guarantee that there exists a (non-constructable) proof that $PA$ is inconsistent, and thus the composite theory is inconsistent as well? I could see how this might not be a problem in intuitionistic logic, but we are working in classical first-order logic with the law of excluded middle. How is this not a paradox?

Answer 1

As is being discussed in the comments, the non-standard proofs in non-standard models of $\mathsf{PA}$ are not trustworthy (in that they're not sound). I'll give a sort of 'toy model' illustrating the intuition about why this is the case.

In a Hilbert-style deduction calculus you have some starting set of axioms and one or more deduction rules (often just modus ponens). A proof is a sequence $$ \varphi_0,\varphi_1,\dots,\varphi_n$$ of sentences satisfying that for each $i\leq n$, either $\varphi_i$ is an axiom or there are $j,k<i$ such that $\varphi_k = (\varphi_j \to \varphi_i)$.

Given such a derivation, the argument that we should believe $\varphi_n$ (provided that we believe in the axioms and in modus ponens) is ultimately an inductive proof. We argue that we should believe $\varphi_0$ and that if we believe $\varphi_i$ for all $i<j$, then we should believe $\varphi_j$.

Non-standard models are a lot more complicated than what I'm about to describe, but this really gets to the heart of the matter. Suppose we're in a non-standard model of arithmetic and the numbers look like this: $$ 0, 1, 2, \dots, \infty - 2, \infty - 1, \infty, \infty + 1, \infty +2,\dots,$$ where '$\infty$' is some fixed infinite non-standard number. Now suppose I give you a derivation that lives in this model which looks like this: $$\varphi_0, \varphi_1,\varphi_{-2},\dots, \varphi_{\infty - 2},\varphi_{\infty-1}, \varphi_{\infty}.$$ This may very well be a derivation in the above sense (as in each step is either an axiom or follows from two previous steps by modus ponens), but the existence of such an object doesn't imply that $\varphi_\infty$ is a trustworthy statement. In fact (and this is the really toy part as I'll explain in a second), we could just have

• $\varphi_i = ((0= 1)\to(0 = 1))$ for each (externally) finite $i$,
• $\varphi_{\infty+i} = (0 = 1)$ for each integer $i$.

This sequence of sentences satisfies the definition (each $\varphi_i$ for $i$ finite is an axiom and $\varphi_{\infty+i}$ follows from $\varphi_0$ and $\varphi_{\infty + i -1}$ by modus ponens) but clearly the conclusion is not supported because the proof of it is relying on an infinite regress. (And this is even ignoring the possibility of sentences that are infinitely long, which is another issue.)

---

Now, the reason that this is a toy model is that clearly we have a failure of induction. The sequence I've defined satisfies that $\varphi_0 = \varphi_0$ and that for each $i$, if $\varphi_i = \varphi_0$, then $\varphi_{i+1} = \varphi_0$, yet it is not true that for all $i$, $\varphi_i = \varphi_0$. In fact, non-standard models of arithmetic are much harder to describe than what I've given above (and in some sense cannot be described 'explicitly'). In an actual model of $\mathsf{PA} + \neg\mathrm{Con}(\mathsf{PA})$, the proof of $0=1$ is ultimately unsound for the same reason (ill-foundedness of the implicit proof tree, or in other words a conclusion relying on an infinite regress), but the 'gap' or 'jump' is much harder to locate in some precise sense.

Answer 2

In the proof of the completeness theorem guaranteeing that a consistent theory like $PA + \neg \text{Con}(PA)$ has a model, roughly (as I understand it) the model construction process adjoins a nonstandard number $n$ to the natural numbers which satisfies the statement you are using to code $\neg \text{Con}(PA)$ and then makes up a bunch of other numbers that are necessary to still get a model of PA, e.g. $n + 1, n^2$, and so forth, roughly analogous to how you adjoin elements to fields to get field extensions.

$n$ is not "actually a number" in the sense that it is not $1$ and it is not $1 + 1$ and it is not $1 + 1 + 1$, etc., it is just this wacky element of a nonstandard model of PA. It certainly does not correspond to any "actual proof of a contradiction" that you could write down; an actual proof has a standard Godel code. It is just that you've constructed this complicated sentence which has the intended interpretation that if you give it a standard natural number $k$ it is supposed to tell you whether or not $k$ is the Godel code of a contradiction in $PA$. But the behavior of this complicated sentence on nonstandard natural numbers doesn't necessarily have anything to do with this intended interpretation.

Here is a loose analogy I find helpful. In the theory of, say, fields you could imagine defining $a \le b$ iff $\exists c : b - a = c^2$. In a real closed field this reproduces a nice ordering making any such field (such as $\mathbb{R}$) an ordered field. However, suppose we now adjoin an element $i$ satisfying $i^2 = -1$ to such a field. Then $a \le b$ no longer defines an order at all, since it no longer satisfies trichotomy. The introduction of this element $i$ has broken the intended interpretation of this symbol, but the intended interpretation is something we layer on top of the bare definition, which is just about the existence of a square root.

One lesson you could take away from all of this is that consistency is not all that great. $PA + \neg \text{Con}(PA)$ may be consistent, assuming $PA$ is consistent, but with this assumption this theory is not arithmetically sound (it proves a false fact about arithmetic, namely $\neg \text{Con}(PA)$).

Answer 3

The other answers are good, but I think that the following general comments may be helpful.

Conceptually, there is a distinction between arithmetic operations on natural numbers, and syntactic operations on strings. We tend to forget about this, because for the most part, the mathematical literature only studies axiomatic systems for numbers, not axiomatic systems for strings. It can be conceptually helpful to introduce a formal language, such as what David Auerbach (How to say things with formalisms) calls "Syntax" or what Quine (Mathematical Logic) calls "protosyntax," which directly expresses statements about strings, and syntactic operations on strings. Doing this helps clarify that assertions about proofs and assertions about numbers are a priori two separate things.

The reason we usually don't bother with a separate formal language for syntax is that the arithmetization of syntax allows us to rephrase syntactic operations on strings as arithmetic operations on natural numbers. Once we understand how to translate between strings and numbers, we can dispense with "protosyntax." We can pretend that an arithmetic statement about numbers "says" that some formal system is consistent.

However, we have to be careful once we start considering formal systems for natural numbers (such as first-order Peano arithmetic) that admit nonstandard models. When you work in such a system, even a statement such as, "There exist $x, y, z > 0$ and $n>2$ such that $x^n+y^n = z^n$" has to be interpreted with care, because the variables $x$, $y$, and $z$ could range over the elements of some nonstandard model, in which case the sentence doesn't mean what you might carelessly think that it means. It's no longer Fermat's Last Theorem per se, but "Fermat's Last Theorem for rings that satisfy the first-order Peano axioms."

The need to be careful becomes doubly important when you are exploiting the arithmetization of syntax to use numbers as a surrogate for syntactic entities. The arithmetic statement that you're pretending is a statement about "consistency" (a syntactic concept) doesn't necessarily mean what you might carelessly think it means, if nonstandard models are being considered. In fact, I would say that instead of asking why there isn't a contradiction, you should first ask yourself, "Why should I think that this formal sentence of arithmetic says anything about syntax at all?" I think that if you approach the matter from this perspective, you're less likely to get confused.

Answer 4

What you are encountering is essentially the phenomenon first explicated by Gödel; it is no less counterintuitive or phenomenal to me that \begin{gather*} \newcommand\ZF{\mathsf{ZF}}\DeclareMathOperator\Con{\mathsf{Con}}\newcommand\KP{\mathsf{KP}} \ZF+\neg \Con(\ZF), \\ \KP+\neg \Con(\KP), \\ \textsf{Homotopy Type Theory}+\neg \Con(\textsf{Homotopy Type Theory}), \end{gather*} etc. are all consistent theories, but they are because consistency is a fundamentally metatheoretic concept, in the most inextricable sense of the word. This is highlighted in a quote from the text Inexhaustibility: A Non-Exhaustive Treatment by Torkel Franzén, who is himself quoting Gödel:

It is this theorem [the second incompleteness theorem] which makes the incompletability of mathematics particularly evident. For, it makes it impossible that someone should set up a certain well-defined system of axioms and rules and consistently make the following assertion about it: All of these axioms and rules I perceive (with mathematical certitude) to be correct, and moreover I believe that they contain all of mathematics. If somebody makes such a statement he contradicts himself. For if he perceives the axioms under consideration to be correct, he also perceives (with the same certainty) that they are consistent. Hence he has a mathematical insight not derivable from his axioms.

That this insight is underivable from our axiomatic system of choice is an essential feature of any foundational system falling prey to the mild conditions in Gödel’s theorems, and because of this it makes perfect sense that we can assume our base theory to be inconsistent and have a new, consistent theory — consistency of our base theory was never provable to begin with, so adding the negation of this statement (or any other statement underivable from our axioms) will again yield a consistent system of axioms.

That this runs counter to our naïve intuition is understandable, but one of the main gifts offered forth by Gödel is this correction of basic human intuition; the sooner one adopts it as their new intuition, the sooner this apparently confusing and counterintuitive landscape of theories and consistency claims begins to take form.

Answer 5

The negation of Con(PA) isn't consistent with second-order number theory, and genuine number theory, I believe, is at least second-order. See also Are there first-order statements that second order PA proves that first order PA does not?

Edit: Let me expand on this, since probably my claim about second-order number theory versus first-order isn't the majority opinion.

First-order induction in PA only states induction, as an axiom schema, for a countably infinite set of "subsets" of the set of natural numbers. Second-order induction states induction, as a single axiom, for "every subset" of the set of natural numbers. Second-order number theory with the appropriate semantics is categorical, while first-order is not, and most number theorists, including myself, believe the structure of natural numbers to be unique up to isomorphism.

I think the reason that PA plus the negation of Con(PA) is consistent is so counterintuitive is that we forget that PA is a first-order theory and neglect to take into account that very few number theorists restrict their reasoning to first-order logic and to PA. The subtleties that arise by restricting to first-order logic are very well understood (Lowenheim-Skolem theorems, etc.) and in this particular instance are addressed by @JamesHanson's excellent answer.

I'm sorry if this answer does not directly address the question, but I thought it was important to say and it couldn't fit in the comments.