The first proper post in this series explaining Gödel’s Incompleteness Theorems and their proofs. If you aren’t familiar with basic formal logic, do take a look at Part 0, since this part starts where Part 0 left off.

Markers to sections (it’s still worth going through them in sequence!):

• Completeness (and syntax vs semantics)
• Gödel’s Completeness Theorem
• Gödel’s Incompleteness Theorems
• Models
• Peano Axioms and Arithmetic

To recap, we left the previous part on a cliffhanger, asking the following question:

If we manage to prove a statement $\varphi$ within a system of axioms $T$, it follows $\varphi$ is TRUE within $T$ (because $T$ is sound). But does it work the other way around? That is, if $\varphi$ is TRUE within $T$, is $\varphi$ provable?

To answer this, we must finally say hello to the one notion we have not yet introduced; completeness.

A formal system $S$ is sound, if and only if its rules of inference only prove statements which are TRUE within $S$, ie. all provable statements are TRUE in the formal system.

Conversely, a formal system $S$ is complete, if and only if all TRUE statements in $S$ can be derived from its rules of inference, ie. all TRUE statements are provable in the formal system.

However, this is only a partially correct definition of completeness. Turns out we have many kinds of completeness! The above is just the definition of semantic completeness.

The second stronger type of completeness we’ll see, is syntactical completeness. A formal system $S$ is syntactically complete if for every statement $\varphi$ in the language of $S$, either $\varphi$ or $\lnot \varphi$ can be proven within $S$. This is also called negation completeness.

But what do syntax and semantics actually mean?

Syntax is what the grammar/rules of the formal system allows; semantics is what the formal system wants to do and gives meaning to the formal system. More abstractly, semantics is the black box, syntax is the implementation. Ideally, syntax should always follow semantics, ie. express the system’s intent as closely as possible.¹

TRUE / FALSE are semantic notions (is this statement allowed, according to what I want my formal system to do?); ‘provable’/’unprovable’ are syntactic notions (can I derive this statement from the axioms of my formal system, via its rules of inference?).

Semantic consequence (if $S$ is TRUE, $\varphi$ is TRUE):
$S \vDash \varphi$

Syntactical consequence ($\varphi$ can be proved from $S$):
$S \vdash \varphi$

Alright, so why did we bring all this up? Turns out, there’s a Gödel’s Completeness Theorem as well. Mind you, the Completeness Theorem and the Incompleteness Theorems refer to different kinds of completeness!

Eh, ‘model’? We’ll talk about this in a bit, but for now, stay put.

We won’t go through the proof here (got enough on our hands with the Incompleteness Theorems already!), but this basically says that any sound first-order system is also semantically complete.

Everything TRUE in first-order logic (FOL) is also provable!

What about the syntactic completeness of FOL? Sadly, neither FOL nor propositional logic is syntactically complete; for instance, the propositional logic statement $A$ is not provable, neither is $\lnot A$.

Phew, we finally have enough tools to tackle the Incompleteness Theorems. Let’s go!

The statement’s pretty clear as it is; note that we’re talking about syntactical completeness here (or rather, lack thereof), not semantic completeness.

As for this statement, it tells us that any reasonably strong formal system can be proved consistent only in a system stronger than itself.

‘Certain amount of elementary arithmetic’? Sounds pretty vague, but it refers to any logical system which is at least as powerful as Peano Arithmetic (ie. contains the successor function, addition, and multiplication of natural numbers).

These two theorems together say that any sound system capable of basic arithmetic must have some TRUE statement we cannot prove (since either $\varphi$ or $\lnot \varphi$ must be TRUE, but we can’t prove either)

More strikingly, if this system is consistent (sound, free of contradictions), we simply cannot prove it to be so without a stronger system.

This is a really big deal!

Not only is Peano Arithmetic incomplete (both syntactically and semantically), we can’t even prove it’s sound! (although we know it is)

Cool, so now we know what’s the hoopla all about. You rub your hands together and say, “Awesome, let’s get down to the proof!”

At this point, sure we can understand the proof, but it’s worth appreciating some of the finer aspects of these theorems. Time to tie up a few loose ends.

Models

»“I don’t like how we’ve defined semantics so hand-wavily. Isn’t there a better way to frame our intent in some formal, math-y way?”

Indeed, there is. You may have noticed that for a particular semantic definition, we may express it using different syntax.

Turns out, we can do it the other way around as well!

As in, for a particular syntax, we may assign different meanings to it. This is called an interpretation of the language of this formal system. After all, this soup of symbols and rules we’ve defined has no meaning unless we give it one!

Remember, TRUE and FALSE are semantic notions and are dependent on the interpretation (meaning) of our formal system.

Alright, a concrete example (taken from here²):

• Domain: A chess set
• Individual constants: $a$: The white King, $b$: The black Queen, $c$: The white King’s pawn
• $F(x)$: $x$ is a piece
• $G(x)$: $x$ is a pawn
• $H(x)$: $x$ is black
• $I(x)$: $x$ is white
• $J(x, y)$: $x$ can capture $y$

In the interpretation $I$ of $L$:

A set of TRUE sentences $S$: $F(a)$, $G(c)$, $H(b)$, $I(a)$, $J(b, c)$.
A set of FALSE sentences: $J(a, c)$, $G(a)$.

For a set of statements (‘theory’) $S$ which is TRUE according to interpretation $I$, $I$ is a model for the theory.

Finally, the standard model for Peano Arithmetic is the set of natural numbers $\mathbb{N}$, but other ‘non-standard’ models for arithmetic do exist!

We can finally see the Completeness Theorem in all its glory. It says that a statement is provable in a first-order theory $T$ if and only if it is TRUE in all possible models of $T$.

»“The Completeness and the Incompleteness Theorems sound contradictory to me, halp!”³⁴

The Incompleteness Theorems tell us that given a first-order theory $T$ capable of performing basic arithmetic, it contains certain statements which are TRUE but unprovable.

By the Completeness Theorem, this unprovable TRUE statement, is simply TRUE within the standard model, because if it was TRUE in every model of $T$, it would be provable as well.

There exists some model of $T$ in which the statement is FALSE!

»“Alright, so how do I find this elusive non-standard model in which our truths become FALSE?”

Ah, we stop right here because we wade into model theory, and the author’s understanding ends at this point. Take a look at the Löwenheim–Skolem theorem and this MathOverflow answer if you’re curious.

»“Okay, so could you at least give me a real example of something TRUE but unprovable?”

Check out the Paris-Harrington theorem! It was the first concrete example of something which is TRUE, but not provable in Peano Arithmetic (although it can be proven in second-order arithmetic). Original paper here.

Peano Axioms and Arithmetic

»“We’ve been talking about Peano Arithmetic for a while now, but what is it exactly? Also, where did the Peano Axioms go?”

Alright, time to state the Peano Axioms:

It’s all pretty cute till here, after which we see the axiom of induction, which causes a few problems…

This is sometimes also stated as:

So what’s the problem? The axiom of induction ranges over predicates (or sets of natural numbers), which means it’s in second-order logic. Seeing it in fancy notation makes it clearer.

$\forall P.[[P(0) \land \forall (k \in \mathbb{N}.[P(k) \implies P(S(k))]] \implies \forall (n \in \mathbb{N}).P(n)]$

$\text{where $P$ is any predicate, and $k$ and $n$ are both natural numbers.}$

Second-order logic is a fresh can o’ worms, so we convert the second-order axiom of induction into a first-order axiom schema, which is basically a countably infinite set of formulas matching a particular form.

Sounds confusing. Let’s use an old example statement from FOL:

• $\forall x(Animal(x) \implies Fur(x))$

We’d like to convert this to propositional logic, but also retain its original meaning. What we do is define a zeroth-order axiom schema which looks similar to the above, but is actually a countably infinite set of all the animals ever (assuming there are infinite kinds of animals).

So we now essentially have an infinite set of zeroth-order axioms:

• $p_1 \triangleq \text{ Dogs are animals} \implies \text{ Dogs have fur}$
• $p_2 \triangleq \text{ Cats are animals} \implies \text{ Cats have fur}$
• $p_3 \triangleq \text{ Lions are animals} \implies \text{ Lions have fur}$
• $\ldots$

Back to the second-order axiom of induction. We convert it into a countably infinite set of axioms containing the induction axiom for every predicate $\varphi$ we can ever create.

To obtain Peano Arithmetic, we kick out the axiom of induction from the Peano Axioms and replace it with this fancy schema.

Peano Arithmetic is the first-order formulation of the Peano Axioms.

Now that we know what the theorems mean, we’ll take on the proofs in the next post!