A result on the incompleteness of mathematics

Suppose somebody comes up to you (keeping a healthy six-foot distance) and claims to have a formal proof system that is simultaneously

(1) sound (if x is provable from X then x is logically entailed by X)
(2) complete (if x is logically entailed by X then x is provable from X), and
(3) finite (all proofs are finitely long).

They also tell you that this proof system is in a language that is rich enough to express natural number arithmetic. Then what you can immediately conclude is that their language and semantics are insufficient to define the natural numbers. That is, there is no set of sentences X in their language such that ℕ is the only model of X. For any set of sentences you choose, there will be other non-standard models of arithmetic that are consistent with all these sentences.

I want the strength of this to sink in. Our only assumptions are syntactic in nature (our proof system being sound and complete, and proofs only being finitely long). And our result is a semantic limitation: that the structure of natural numbers are not definable by any set of sentences. And importantly, when I say “any set of sentences”, I mean any set of sentences, not just any recursively enumerable set of sentences. You could literally just define the set of all sentences in L that correspond to true statements about the natural numbers, and that would still not be enough to uniquely pin down the natural numbers! There will always be these extra non-standard interpretations of all your sentences that correspond to very different mathematical structures with bizarre properties.

Here’s an outline of the proof.

Let F be a proof system for some semantics Ω such that the following hold:

1. F is sound.
   If X ⊢ x, then X ⊨ x.
2. F is complete.
   If X ⊨ x, then X ⊢ x.
3. Every proof in F is finite.

From these three assumptions we can prove compactness. Compactness is the property of a logic that says that a set of sentences X has a model if and only if every finite subset of X has a model. And from compactness, there’s a really nice little proof that ℕ is not definable.

So, our proof is in two steps: first we show compactness, then we show that compactness entails the undefinability of ℕ. Let’s go through in more detail now.

Compactness

Definition of compactness: A set of sentences X is satisfiable if and only if every finite subset of X is satisfiable.

First, briefly:

X is satisfiable
iff (by soundness and completeness)
X is consistent
iff (by finite proofs)
Every finite subset of X is consistent
iff (by soundness and completeness)
Every finite subset of X is satisfiable.

And now, in more detail:

• X is satisfiable
  iff (by definition)
• X has a model
  iff (by definition)
• For no a does X ⊨ a and X ⊨ (¬a)
  iff (by soundness and completeness)
• For no a does X ⊢ a and X ⊢ (¬a)
  iff (by finite proofs)
• For every finite Y ⊆ X, for no a does Y ⊢ a and Y ⊢ (¬a)
  iff (by soundness and completeness)
• For every finite Y ⊆ X, for no a does Y ⊨ a and Y ⊨ (¬a)
  iff (by definition)
• For every finite Y ⊆ X, Y has a model
  iff (by definition)
• For every finite Y ⊆ X, Y is satisfiable

And that’s the proof! Ok, now that we’ve established compactness, let’s establish some of its consequences (of which there are many. Compactness has massive consequences for the expressive capabilities of your logic.)

Undefinability of ℕ

Suppose that ℕ were definable in some language L where compactness holds. Then there is some set of L-sentences X such that ℕ is a model of X, and no other structures are a model of X. Intuitively, this means that the set of sentences X “pins down” the natural numbers, so that you know that when you start by assuming X, you really are talking about the natural numbers and no other mathematical structures. Now we’ll derive a contradiction.

We start by adding to L a new constant symbol, call it c. We now create a new set of sentences Y by starting with X and adding assertions that c ≠ n, for every natural number n. Y = X ∪ {c ≠ 0, c ≠ 1, c ≠ 2, …}. (The exact terms for 0, 1, 2, and so on will depend on your language; for instance in standard first order PA, Y would be X ∪ {c ≠ 0, c ≠ S0, c ≠ SS0, …}, where S is the successor function).

Now we ask: Does Y have a model? The answer is yes! To prove this we apply compactness. Y has a model as long as every finite subset of Y has a model. But any finite subset of Y only includes finitely many of the sentences in X (for which we already know ℕ is a model) as well as finitely many of the sentences of the form “c ≠ n”. But this means that no finite subset of Y asserts c to be distinct from every natural number! For any finite subset of the sentences in Y, we can always find some natural number to assign to c by just choosing one that hasn’t yet been referenced! And therefore ℕ is a model of every finite subset of Y.

So since every finite subset of Y has a model, Y itself has a model! But this model must satisfy every sentence in Y, and Y contains the assertion that c is none of the natural numbers. So in this model, there is some number that is distinct from all the natural numbers. In other words, this model is distinctly not ℕ! Let’s call it ℕ*.

Alright, so we have that the new set of sentences Y that we constructed has a non-standard model ℕ*. But what about our original set of sentences X, which was supposed to categorically describe ℕ? Unfortunately, ℕ* is also a model of X! Why? Well, X is strictly weaker than Y. We got from X to Y by adding axioms, so all that we could have done in that process is remove potential models, not add any new ones. Any model of Y has to have been a model of X from the start! So X does not uniquely describe the natural numbers.

Proof by contradiction! ℕ cannot be defined in a compact logic.

Summary

From just three simple and intuitively desirable properties of proof systems (soundness, completeness, and finite proofs), we derived compactness. And then we showed that no compact logic is capable of defining natural numbers. It turns out that from compactness you can also prove the undefinability of the collection of finite groups, of connected graphs, of the real numbers, of finite-diameter graphs, and many other structures of interest.

This result is pretty stunning in the limitations it implies for the axiomatic method of mathematics. In one sense, it’s actually stronger than the incompleteness theorems, because we never said anything about our set of sentences used to characterize the natural numbers being effectively enumerable, much less decidable. What this means is that no language that has a proof system meeting the above three requirements has the expressive capabilities to pin down the natural numbers. Even by just collecting all the true sentences of arithmetic in the language, we still don’t have enough to fully specify the structure we’re trying to talk about!

To phrase it in the converse: If you want to talk about the natural numbers, you have to be willing to accept a logic which is either unsound, incomplete, or has infinitely long proofs. And none of these seem very appealing to me! The choice is yours: if you want to speak about natural numbers, the language you use to do so will either have insufficient expressive capabilities to actually pin down the topic of conversation (such that everything you say might be interpreted as having to do with a completely different mathematical structure), OR it will have an unsatisfactory proof system (such that you have no good procedure for verifying the truth of arbitrary sentences).