One of the foundations of pure mathematics is proof: showing mathematically, elegantly and thoroughly that a statement is true or false. You may have encountered proof by induction, contradiction, or exhaustion before at A-level. But some statements in mathematics are taken as universally true, even though we cannot prove them. These are called axioms. For example, one of Euclid's common notions: “Things which are equal to the same thing are also equal to one another” (i.e. if A=C and B=C, then A=B). For many years, mathematicians have tried to prove certain axioms, turning them into non-axiomatic statements.

But in 1931, Kurt Gödel showed that it is possible to prove that some statements are unprovable. But what does this proof actually look like?

First, we need to know about formal theories. Formal theories are sets of symbols governed by axioms and rules. These axioms and rules are called Formal Systems. Mathematics is (sometimes) considered a range of different Formal Systems.

Gödel found that if a formal system has enough rules in it to do maths, then it has one of either of these problems:

1) The formal theories make contradictions
2) The formal theories are incomplete, which means there are rules within it that we can’t prove using its other rules

Gödel used specific symbols to describe formal theories called the Gödel’s Numbering System. and then wrote "The Gödel Sentence” (represented by “G”):

The string of symbols above (“G”) essentially states, "G cannot be proven true using this formal system”.

If G can be proven true (by other rules in the formal theory), then G cannot be proven true within said formal theory, making the formal theory incomplete. This is technically Gödels First Incompleteness Theorem.

If G can be proven false (by other rules in the formal system), then G can be proven true within said formal theory, which is the opposite of the statement G itself (that G is false). This is a contradiction, and forms Gödels Second Incompleteness Theorem.

This means that certain rules in an (incomplete) formal system have no proof. Or that certain rules in a (complete) formal system contradict each other.

Before this, many mathematicians thought that there would eventually be a proof found for every axiom, if we just looked hard enough. Gödels Incompleteness Theorem proves, quite elegantly, that this is not the case, ending the search for a complete, non-contradictory formal system.

You might have actually encountered something similar in popular “paradoxes”. For example:

In another world, people can either be truth-tellers (who only tell the truth) or liars (who only tell lies). Someone in said world says “This statement is false”.

If the statement is false, then it’s false that the statement is false and the speaker is a truth-teller, but if the statement is true, then it’s true that the statement is false, and so the speaker is a liar. This form of contradiction is inescapable in a system (in this case, english language) that is advanced enough to make self-referential statements.

Extra thoughts:

I first encountered the idea of “completeness” when looking for a list of listed buildings in England. I came across a list containing the list of what I was looking for on the Wikipedia page titled “Lists of lists of lists”. You can access it here: https://en.wikipedia.org/wiki/List_of_lists_of_lists. (The specific list I was looking for, on this list, was https://en.wikipedia.org/wiki/Listed_buildings_in_England).

It states:

I wondered if the list of lists that do not contain themselves would contain itself.

Unknowingly, I was thinking about a well-established paradox in set theory called “Russell’s paradox”. The set of sets that do not contain themselves must either be incomplete or contradict itself by either not containing or containing itself.