A preliminary post in this series explaining Gödel’s Incompleteness Theorems and their proofs. Feel free to skip this and go straight to Part 1 if you’re already familiar with basic formal logic.

To start off, let’s take a look at the theorems themselves (in fancy text, no less) and the things we need to know before disecting them word-by-word. Let’s go!

Alright, key words to note:

• Consistent
• Formal system (and proving something in a formal system)
• ‘Elementary’ arithmetic (and ‘certain amount’ thereof)
• Language (of a formal system)
• Incomplete

I’ll be spending this post falling through the rabbit hole of logic and informally exploring the above terms (except the notion of completeness) via the questions below:

• What is a set?
• What are axioms?
• What is first-order logic?
• Meaning of something being ‘true’ and something being ‘provable’

Click the points above to jump to particular sections, although they’re best read in order.

Sets¹

What a set isn’t: any well-defined collection of elements. (see Naive Set Theory²)
What a set is: erm…

To be fair, I’m not really correct; the naive definition isn’t wrong per se, just that it gave birth to a bunch of paradoxes like most notably…

Another nice description ³: “Consider a group of barbers who shave only those men who do not shave themselves. Suppose there is a barber in this collection who does not shave himself; then by the definition of the collection, he must shave himself. But no barber in the collection can shave himself. (If so, he would be a man who does shave men who shave themselves.)”

We’ve arrived at a contradiction, ie. naive set theory is inconsistent! It became obvious we needed to set better rules for what sets can and can’t do (to avoid such inconsistencies), which leads us to…

Axioms⁴

It’s worth reminding ourselves that we can’t just ‘assume’ the existence of most things we’ve learnt in school. We’re just trying to come up with a bunch of rules which are free of contradictions to start off our ‘math universe’ with.

We’ll call these rules axioms, and a collection of such rules as an axiomatic system. The notion of ‘proving’ axioms is meaningless, because axioms are merely a starting point from which we derive fancier things. There is no concept of them being TRUE or FALSE; they’re just… there. (something can only be TRUE or FALSE under some axiomatic system; what happens when there is none?)

The only requirements for making up an axiomatic system of your own, are:

• It should be consistent (i.e. sound, impossible to derive a contradiction from it)
• It should be non-redundant (none of the axioms should be deriveable from the others)

Seriously, that’s it; just a bunch of rules which can’t be reduced further.

So all the math I’ve been doing so far is only true under a certain axiomatic systems? If I come up with another such system, is it possible for it suddenly render some parts of math untrue? OMG.

Remember Euclid’s Postulates in geometry? You can kick out the 2nd or the 5th postulates and you’d get a fresh discipline of math called Non-Euclidean Geometry (where the angles of a triangle can sum to more than 180 degrees!), which is perfectly legit (yes, it’s consistent and non-redundant). Point is, as long as it satisfies the above two properties, it’s all fair game. Math people come up with weird shit all the time.

Coming back to sets.

Zermelo-Fraenkel set theory (ZFC) is one such axiomatic system for sets which is consistent and non-redundant. Similarly, the Peano axioms are for natural numbers. Don’t worry, we’ll be coming back to these again in more detail when we discuss Gödel’s Theorems.

Also, it’s worth noting that Peano Arithmetic (which is a bit ifrom the Peano Axioms!) is not unique to the naturals and that other non-natural numbers do obey Peano Arithmetic, namely because it is a ‘weaker first-order system’. What is that? Read on…

First-order logic⁵

Before we go into first-order logic, let’s first understand what is a formal system with a little example.

To construct a valid sentence, we’ll define a few rules:

• article is always followed by noun
• noun is always followed by verb or .
• A valid sentence must always start with an article <- Starting point (axiom)

‘Symbols’ allowed:

• Articles - the, a
• Nouns - boy, girl, ball, flower
• Verbs - smells, sees

So, valid sentence: the girl sees a ball .
Invalid sentence: boy flower girl the

To construct any sentence (the ‘language’), we can put these ‘symbols’ into any order we like

We require the rules (‘rules of inference’) only to construct valid ones (set of ‘theorems’), and similarly to check whether a given sentence is valid (a ‘decision procedure’ to output TRUE or FALSE). And ta-da, we have a formal system!

It’s simply a framework with strict rules to model certain behaviour.

The first formal system we’re going to see, propositional logic, is pretty straightforward. Every statement (‘proposition’) only has a set of symbols (say $p$, $q$, $r$) and a set of operations (AND - $\land$, OR - $\lor$, NOT - $\lnot$, IMPLIES - $\Rightarrow$) acting on them. The output is TRUE or FALSE.

It’s worth noting that these ‘symbols’ aren’t variables; they can only represent static facts and be either TRUE or FALSE. For example:

• $p \triangleq \text{ Dogs are animals}$
• $q \triangleq \text{ Animals have fur}$
• $r \triangleq \text{ Dogs have fur}$
• $p \land q \implies r$

You might notice there’s a lot of repetition. There’s no way we can say $\text{Cat is an animal}$ without assigning it to some variable $s$, when we really just could replace $\text{Dog}$ with $\text{Cat}$. More importantly, $r$ is not a natural logical consequence of $p$ and $q$; we’ve had to artificially define it to be so.

What we’d like to have is some system where we can define functions of objects, like $\text{Animal(Dog)}$ or $\text{Animal(Cat)}$.

Enter first-order logic (FOL), propositional logic’s richer sibling.

FOL adds on two extra components, predicates and quantifiers.

We can think of predicates as functions which return boolean values, like the binary predicate $x \in y$ can be represented as $\text{belongs(x, y)}$. We can also have predicates taking multiple variables.

Quantifiers, hint, hint, quantify a variable; ie. indicate the quantity of the variable(s) attached to some predicate. For instance, we can say ‘for all values of x, predicate $P(x)$ is true’, ie. $\forall x P(x)$. We can also say, ‘there exists some value of x such that $P(x)$ is true’, ie. $\exists x P(x)$.

Earlier example now more appropriately expressed in FOL:

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

Beautiful, innit?

Finally, first-order logic is called so because it allows quantifiers to act on variables, but not predicates or functions of those variables. While second-order logic allows quantifiers to range over predicates and functions of objects (and beyond for higher-order logic).

But, how do we figure out whether a given statement is provable within a formal system say, within first-order logic? Heck, what does a statement being TRUE even mean?

True versus Provable

A more informal look at this problem here⁶.

The more I read about logic, the more confused I got about what does TRUE mean, so let’s start off with the definition of proofs (taken from this⁷).

Given a statement $\varphi$ to prove within a system of axioms $T$, we have a finite sequence of statements $\varphi_1 \ldots \varphi_k$, such that:

• $\varphi_k = \varphi$, which means we’re done, and,
• For every $i \lt k$, $\varphi_i$ is either an axiom, or it was derived from previous statements using axioms and rules of inference.

If we manage to prove $\varphi$, 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?

Alas, this question signals the end of this long post, for we must finally call upon our friend Gödel to answer this.