A Theory That Proves Its Own Inconsistency

(This is Yan Sheng.)

$\newcommand{\bb}{\mathbb}\newcommand{\Con}{\operatorname{Con}}$I once read this mind-bending blog post by Joel David Hamkins that proves this result:

Theorem: There is a Turing machine program $P$ such that for any function $f:\bb N\to\bb N$, there is a model of Peano arithmetic in which $P$ computes $f$ on the standard natural numbers.

Read that again: there is a single Turing machine that outputs any given function—even uncomputable ones (!!)—if you run it in the correct universe. If this statement doesn’t surprise you, I’m not sure what else would (unless you work in logic or set theory; I’m convinced that those people routinely believe as many as six impossible things before breakfast).

A extraordinary claim needs an extraordinary proof, and when I read through Hamkins’s argument I came across a lesser absurdity: a theory that proves its own inconsistency. Since all my knowledge of formal logic is from folklore, this post is my attempt to informally explain (to myself, at least) how such a theory can be constructed, and why it is not a contradiction in terms.

Consistency

The great insight of Gödel’s incompleteness theorems is the arithmetisation of logic: the rules of logical deduction can be executed entirely in terms of natural numbers, for instance in the system of Peano arithmetic (PA).

First, we can encode logical formulas as natural numbers. There are many different possible ways to do this, but nowadays I can just say “convert the formula into bytes and interpret it as an integer”, and that basically works.

However, only a subset of the formulas that we can write down actually make sense; these are called well-formed formulas. (For example, “$r\,\wedge\rightarrow pq\,\neg$” is not well-formed, while “$0=1$” is.) Roughly speaking, well-formed formulas can be built up inductively from atomic formulas; in other words, well-formed formulas are exactly those that can appear in some (finite) sequence of formulas, such that each formula in the sequence either

• is an atomic formula; or
• can be formed by the rules for combining previous formulas.

In principle, we can restate this entire definition so that we only refer to the natural numbers encoding the formulas, and never talk about the formulas themselves. Hence we can translate the statement

$n$ encodes a well-formed formula

into the language of PA (i.e., into a well-formed formula in PA), for any natural number $n$.

Similarly, a proof of some formula $p$ is just a (finite) sequence of well-formed formulas whose last term is $p$, such that each formula in the sequence either

• is an axiom; or
• follows from previous formulas by the inference rules of logic.

These formal manipulations of symbols can also be done within PA, so we can write formulas that mean

$n$ encodes a proof of $p$

for any natural number $n$ and formula $p$.

Hence there is a formula in PA that states the consistency of PA itself, namely$$\Con(PA)\coloneqq\neg\exists n\,[n\text{ encodes a proof of ``}0=1\text{'' in PA}].$$

The theory that proves its own inconsistency

Consider the theory $T$, which is PA with one extra axiom:$$T\coloneqq PA+\neg\Con(PA).$$Assuming that PA is consistent, I claim that $T$ is a consistent theory, but $T$ proves $\neg\Con(T)$. The interested reader can pause here and try figuring out why for themselves! (If PA is inconsistent then the claim is still true because PA would prove every statement, but in that case we have a bigger problem.)

First, by Gödel’s second incompleteness theorem, PA cannot prove $\Con(PA)$, so no contradiction arises when we add $\neg\Con(PA)$ as an axiom to PA. Hence $T$ is consistent.

Next, consider the following statement:

Proposition: $\neg\Con(PA)\rightarrow\neg\Con(T).$

Proof: Suppose that $n$ encodes a proof of “$0=1$” in PA. Since every axiom of PA is also an axiom of $T$, we have that $n$ also encodes a proof of “$0=1$” in $T$, and we are done.

The crux is to observe that the above proof can be translated entirely into PA; hence PA proves $\neg\Con(PA)\rightarrow\neg\Con(T)$, so $T$ also proves it. But $\neg\Con(PA)$ is an axiom of $T$, so $T$ proves $\neg\Con(T)$, i.e., $T$ proves its own inconsistency!

How is this possible?

Resolving the paradox

Taking a closer look, let us unpack what $\neg\Con(T)$ says:$$\exists n\,[n\text{ encodes a proof of ``}0=1\text{'' in }T].$$But since $T$ is consistent, we actually have

For each natural number $n$, $T$ proves that $n$ does not encode a proof of “$0=1$”.

The important thing to note is that the above sentence is not a formula in $T$, but a statement in the meta-theory.

So we see the heart of this apparent contradiction: $T$ proves a statement of the form $\exists n\,[P(n)]$, but cannot actually exhibit an example of $n$ where $P(n)$ is true! The technical term for this phenomenon is $\omega$-inconsistency.

Philosophical implications

Since I’m not nearly qualified enough to know what all this really means, I’ll list here some opinions from people who are.

Robert Seely notes that consistency is actually a rather weak property of a theory: our example $T$ is consistent but unsound, in that it proves the false (by assumption) arithmetic statement $\neg\Con(T)$. More disconcertingly, there is no logical contradiction if we suppose the following three statements are all true:

1. ZFC (the usual set theory axioms for all of mathematics) is consistent;
2. For any even integer $n>2$, $n$ is a sum of two prime numbers (Goldbach’s conjecture); and
3. ZFC proves that there exists an even integer $n>2$ that is not the sum of two prime numbers.

So the relationship between truth and provability is really subtle; a consistent theory can even prove a false arithmetical statement. Of course, the exact moral of this story would be different to a Platonist, a formalist, and an intuitionist, since even the notion of truth in itself varies across the different philosophies.

Also, there is a different interpretation of the resolution of the paradox. By Gödel’s completeness theorem, $T$ is consistent implies that $T$ has a model $M$, say in ZFC. Then in $M$, there is an actual “natural number” $n$ that encodes a proof of “$0=1$”; it just happens that $M$ is a nonstandard model of arithmetic, so $n$ is not a “standard” natural number, and the proof encoded by $n$ is of nonstandard length, hence invalid. So we should really modify one of the statements we made above to read:

For each standard natural number $n$, $T$ proves that $n$ does not encode a proof of “$0=1$”.

But then John Baez raises the following question: what exactly is the “standard model” of the natural numbers? We can define this as any model of second-order Peano arithmetic, which is provably unique up to isomorphism in ZFC. However, ZFC itself has nonstandard models (if ZFC is consistent, then so is $ZFC+\neg\Con(ZFC)$, which then has a model by Gödel’s completeness theorem). Then some such nonstandard model of ZFC could have the “wrong” standard model of natural numbers, and how could we tell then?

Finally, a short post by cousin_it observes that for any formal system (eg. ZFC), you can encode statements and proofs of that formal system as natural numbers in PA. Hence the ability to resolve all arithmetical implications of PA is equivalent to the ability to resolve all logical implications of any formal system! It is mind-boggling to me that there is a statement about natural numbers in PA which is equivalent to $\Con(ZFC)$, and is hence undecidable in ZFC.

My set theory professor once told me, in the context of the continuum hypothesis and forcing, that no one really understands the nature of the power set of the natural numbers (equivalently, the real numbers). Perhaps at this point I could go one step further to say that I don’t really understand the nature of the natural numbers either, not anymore…