This is what the tattoo on my arm looks like (well – looked like right after I got it. You can still see the skin being noticably red/pale around it). It’s been designed by my flatmate at the time, Gwen. Without the arm it looks like this:


Probably still not too legible, so let’s get rid of the decoration (sorry, Gwen) and we get this here:

G(x) := \neg\text{Prov}(\text{sub}(x,x))\Rightarrow\text{PA}\vdash G(\ulcorner G\urcorner)\leftrightarrow\neg\text{Prov}(\ulcorner G(\ulcorner G\urcorner)\urcorner)

This statement represents the central idea behind the proof of Gödel’s incompleteness theorems – which to me represent the pinnacle of mathematical ingenuity, elegance and beauty. So let me try to explain why.

Yes, I’ve already written about the incompleteness theorems in previous iterations of this blog, but a) they don’t exist anymore, b) I can’t let my tattoo unexplained on a math blog and 3) Gödel is awesome 😉

Disclaimer: I’m trying to explain a quite technical mathematical theorem without misrepresenting it, but also without all the gritty technical details. The latter means I’ll skip over and simplify a lot of details that are important if you want to fully understand the theorem, its proof and especially its implications. So be careful not to draw conclusions from this post alone and keep in mind, that this is just a simplification.

 For all practical purposes, the language of mathematics is first-order predicate logic. It’s an extremely simple, yet highly extensible language with just a handful of fixed symbols:

Symbol Meaning Usage
\wedge “and” A \wedge B
\vee (inclusive) “or” A \vee B
\neg “not” \neg A
\to “implies” A \to B
\leftrightarrow “if and only if” A \leftrightarrow A
\doteq “equals” a \doteq b
\forall “for all” \forall x\; x \doteq x
\exists “there exists” \forall y\exists x\; \neg x\doteq y

…plus parentheses and, depending on the specific context, a finite number of variables and symbols representing constants, functions or relations. The grammar of first-order logic is recursive and fully defined by just a handful of rules – it’s hard to come up with a (useful) language that is even simpler. Which is why it should probably be somewhat surprising, that according to general experience and mathematical folklore, every mathematical statement can be expressed in this language, i.e. can be reduced to just a handful of symbols put together according to just a handful of simple rules.

Now, this also allows for defining what a proof is; namely a sequence of formulas, such that every formula in the sequence “is derivable / provable from” the previous ones. And as it turns out, this “is provable from” can further be reduced to just a handful of rather simple proof rules, such as:

\dfrac{A,\quad A\to B}{B}.

“If A is true and A\to B is true, then B is true.”

There are lots of different proof calculi (i.e. sets of proof rules), but for our purposes all we need to care about is, that a calculus exists that is complete. And that is what Gödel showed in his Ph.D. thesis in 1929: There is a proof calculus for first-order logic such that every statement, that logically follows from a set of premises (axioms), can be proven in that calculus.

In a certain sense that means that all of mathematics can be reduced to putting a couple of symbols together to form sentences, according to very simple rules, and applying a couple of very simple proof rules to them to form new theorems. All of math, once reduced to first-order logic, is just simple, purely syntactical manipulation of symbols. I don’t need to know what the symbols mean, or why the proof rules are valid – I just need to apply them, like moves in a game.

Now for the incompleteness theorems: They concern the search for a set of axioms, that is

  1. sufficiently powerful to form a foundation for all of mathematics,
  2. not contradictory (i.e. can not prove contradictions, otherwise it is completely useless) and
  3. complete in the sense, that every possible statement can – on the basis of these axioms – either be proven or disproven.

There already was a contestant for that set of axioms – as it turned out, set theory is incredibly powerful in that regard, and a theory of sets was (and still is, though now with certain restrictions) indeed a plausible candidate for a basis of “all of mathematics”. Just the points 2. and 3. still needed to be proven. And that’s what Gödel tried next. Instead, in 1931 he proved that that was impossible.

Instead of immediately going for a foundational set of axioms such as set theory, let’s restrict ourselves to a much simpler theory, Peano arithmetic. The Peano axioms try to axiomatize the natural numbers (0,1,2,3,…) and use only the additional symbols “0“, “S“, “+” and “\cdot” – where the symbol S is the successor function (i.e. S(0)=1, S(1)=S(S(0))=2 etc.). The axioms are all rather simple, e.g. \forall x \neg S(x)\doteq0 (0 is not a successor”) or \forall x\forall y (S(x)\doteq S(y) \to x\doteq y) (“For any natural numbers x,y, if the successors of x and y are equal, then so are x and y). So Peano arithmetic can only talk about natural numbers, and addition and multiplication on them – nothing else. But of course, every candidate set of axioms for all of mathematics should at the very least have natural numbers, so if we fail here already, we might have a problem.

However, Gödel realized that the natural numbers are already complex enough to be able to encode formulas themselves! Nowadays that shouldn’t be too surprising – computers encode everything as numbers after all, but it turned out, that that fact kills all hope for a complete foundational axiom system.

Here’s one way to do that: To start off, we assign every symbol in our language to a unique number – e.g. we can just enumerate them:

Symbol Number
\wedge 1
\vee 2
\neg 3
\to 4
\doteq 5

That still leaves us with plenty of room for additional symbols, and for variables we just use the numbers >100.

Now a formula is just a sequence of symbols, and every symbol has a unique number, so we can e.g. use the uniqueness of prime factorizations to encode formulas just as uniquely:

For any sequence of symbols (s_1 , s_2 , s_3 , . . . ) we first take the corresponding sequence of numbers ( n_1 , n_2 , n_3 , . . . ) and multiply those as powers of the first prime numbers, like so: 2^{n_1} \cdot 3^{n_2} \cdot 5^{n_3} \cdot . . .. This will yield some huge number, but which one doesn’t matter – the only important thing is, that it exists and that we could compute it if we wanted to.

And if we decompose that number back into its prime factors, we will get our original sequence of numbers back, and thus our original sequence of symbols, i.e. our formula. So for each formula \varphi, we get a unique number \ulcorner\varphi\urcorner that encodes that formula – called its Gödel number. And it’s easy to determine, whether any number is a Gödel number – we just need to look at its prime factorization and check whether they observe the rather simple (and on the basis of numbers easily computable) grammar of first-order logic. Which means, by talking about Gödel numbers, Peano arithmetic can talk about formulas.

Next, remember that proofs are also just sequences of formulas (or their Gödel numbers) obeying certain rather simple rules, so by the same encoding we can assign numbers to proofs – just take the powers of primes of the Gödel numbers of the formulas in the proof. The consequence of that is, that the claim “the formula \varphi is provable” is equivalent to the statement “there is a number p that encodes a proof for the number \ulcorner\varphi\urcorner, which is just a relation on numbers. In fact, the relation p encodes a proof for \varphi is – since the proof calculus is rather simple and easy to verify – computable and ultimately reducible to “simple” arithmetic on natural numbers, which means Peano arithmetic can talk about the provability of formulas.

Let me repeat that: In talking just about numbers and simple arithmetic, we can also talk about formulas and whether they are provable!

So let’s do that now:

We first add a new symbol \text{Prov}(x) to our list, just as an abbreviation for the (otherwise rather complicated) formula for the property, that x is a Gödel number that corresponds to a provable formula, i.e. \text{Prov}(\ulcorner\varphi\urcorner) is true, if the formula \varphi is provable in Peano arithmetic.

Furthermore, we add a function symbol \text{sub}(n,m), that substitutes the free variable x (if existent!) in the formula with Gödel number n by the number m and yields the Gödel number of the resulting formula. Meaning: If the formula with Gödel number n is a property of numbers (like being prime or being even – or being a Gödel number of a provable formula 😉 ), then \text{sub}(n,m) is the Gödel number of the formula that claims that property for the number m  – this is just a rather “simple” arithmetic computation, so unproblematic.

For example, let \varphi be the formula x\doteq0. Its Gödel number is \ulcorner x\doteq0\urcorner, so if we apply \text{sub} to that and, say, the number 0, we get \text{sub}(\ulcorner x\doteq0\urcorner,0)\;=\;\ulcorner 0\doteq 0\urcorner. , which is the Gödel number of a provable formula, so \text{Prov}(\ulcorner 0\doteq 0\urcorner) (i.e. \text{Prov}(\ulcorner\text{sub}(\ulcorner x\doteq0\urcorner,0)\urcorner)) is true.

We’re now ready to look at my tattoo again:

G(x) := \neg\text{Prov}(\text{sub}(x,x))\Rightarrow\text{PA}\vdash G(\ulcorner G\urcorner)\leftrightarrow\neg\text{Prov}(\ulcorner G(\ulcorner G\urcorner)\urcorner)

What this tells us is: We define the formula G to be the formula \neg\text{Prov}(\text{sub}(x,x)) which states that the formula that results from applying the property with Gödel number x to the number x itself is not provable.

Let for example P be the property x is a prime number”, which by the way, as a formula looks like this:

P:=\neg x \doteq S(0) \wedge \forall y\forall z (y\cdot z \doteq x \to (y\doteq S(0) \vee z\doteq S(0)))

x\neq 1 and for all numbers y,z: If y\cdot z=x, then either y=1 or z=1

then G(\ulcorner P\urcorner) states, that it is not provable (in Peano arithmetic), that the Gödel number of P is itself a prime number.

…now it just so happens, that G is itself a property of numbers – in particular of Gödel numbers. So what happens, if we apply G to its own Gödel number? Well, this:

G(\ulcorner G\urcorner) = \neg\text{Prov}(\text{sub}(\ulcorner G\urcorner , \ulcorner G\urcorner))

and what is \text{sub}(\ulcorner G\urcorner , \ulcorner G\urcorner)? Well, the Gödel number of applying G to \ulcorner G\urcorner, which is… well G(\ulcorner G\urcorner) again, which means:

G(\ulcorner G\urcorner) = \neg\text{Prov}(\ulcorner G(\ulcorner G\urcorner)\urcorner)

We managed to build a formula that not just talks about other formulas (via their Gödel numbers) – we found a formula that talks about itself. And even crazier: the formula asserts its own non-provability, just like the sentence “I am not provable”, except that in actuality it’s just a mathematical statement about numbers and their properties. Which means: The formula is true if and only if it is not provable, which can be expressed as a formula:

G(\ulcorner G\urcorner)\leftrightarrow\neg\text{Prov}(\ulcorner G(\ulcorner G\urcorner)\urcorner)

\text{PA} is just an abbreviation for Peano arithmetic, and “T\vdash \varphi” just means “axiom system T proves the formula \varphi. In this case, the \text{PA}\vdash . . . expresses, that Peano arithmetic is able to proof that G(\ulcorner G\urcorner) is true if and only if it is not provable (it’s just a matter of substituting x and evaluating \text{sub}(\ulcorner G\urcorner , \ulcorner G\urcorner), after all), and there we are:

G(x) := \neg\text{Prov}(\text{sub}(x,x))\Rightarrow\text{PA}\vdash G(\ulcorner G\urcorner)\leftrightarrow\neg\text{Prov}(\ulcorner G(\ulcorner G\urcorner)\urcorner)

Both incompleteness theorems follow directly from that:

  • Gödel’s first incompleteness theorem: Every sufficiently powerful set of axioms is either incomplete or inconsistent.
    This follows, since if G(\ulcorner G\urcorner) is true (i.e. follows logically from \text{PA}), it cannot be provable. Since every true statement is provable (by the completeness of the proof calculus), that means G(\ulcorner G\urcorner) can not logically follow from \text{PA}. But if it were false (i.e. its negation follows logically from \text{PA}), then it would have to be provable, in which case \text{PA} is inconsistent (well, not quite because of nonstandard numbers, but I’ll leave those out here). So neither truth nor falsity of the formula follows from \text{PA}, and that’s what incompleteness means – so there goes the third item on our wish list.
  • Gödel’s second incompleteness theorem: No sufficiently powerful set of axioms can be proven to be consistent (except in an even more powerful system that also can not be proven to be consistent).
    This follows, because for similar reasons as above, the formula G(\ulcorner G\urcorner) is in fact equivalent to the statement, that \text{PA} is consistent – expressed (using Gödel numbers) in \text{PA} itself. Since we know that G(\ulcorner G\urcorner) can’t be proven, neither can the consistency of \text{PA} – and the second item on our wish list is, well not necessarily gone, but definitely not provable.

“Sufficiently powerful” in this context means, it must allow for everything we did with the natural numbers here; primarily we need infinitely many objects (e.g. numbers), and a way to encode finite sequences of objects as objects themselves (e.g. using prime number decomposition). Since we definitely need at least the natural numbers in a proper foundation, we’re screwed.

Now that we know, what my tattoo means – why did I have that tattooed in the first place? Well, to me, this is mathematics at its absolute best. At its center, there is a simple idea (basically: use the liar paradox to make the system implode), expressed in a new way (using first-order logic to construct a formula that negates its own provability) using a clever new technique (encoding formulas as numbers) and an incredible amount of hard work (here is Gödel’s original paper, if you want to look at it), yielding a surprising result (seriously: the whole mathematical community at the time was hoping for the opposite!) with (in this case even) profound philosophical implications about what it even means to be true, false or provable in mathematics in the first place.

It’s a piece of art constructed out of pure reasoning!

In a sense, the incompleteness theorems are to logic (and logic is to math), as Heisenberg’s uncertainty principle is to quantum mechanics (and qm is to physics). That analogy is probably not even that contrived – at the very least the timing is about right 😀

So to me, this one formal string on my arm represents everything I love about mathematics.