It is a common belief that to do mathematics, it is enough to simply manipulate symbols according to strict rules. But an important discovery of mathematical logic demonstrates that mechanical manipulation is not enough to deduce all of mathematics, and eventually humans will be required to add new rules or assumptions.

Mathematicians come up with ideas by noticing patterns. Then they verify these patterns by proving mathematical theorems. Ever since the ancient Greek mathematician Euclid wrote his famous treatise, The Elements, mathematicians have proved theorems by starting with certain assumed, self-evident facts, called axioms, and applying precise rules of reasoning. In the early twentieth century, this effort was revitalised by the great mathematician, David Hilbert, with the concept of a formal system. This is a system where mathematical statements are encoded as sequences of symbols, called strings. A system provides strict rules for creating new strings from old strings, and these rules do not refer to the meaning of those strings, only to the arrangement of symbols which comprise them. It is possible to create a formal system with multiple interpretations or none at all. Our interpretation of the system does not affect which strings can be produced. The following quote by Hilbert demonstrates the concept: “One must be able to say at all times – instead of points, straight lines, and planes – tables, chairs, and beer mugs.”

Mathematicians are only interested in formal systems with certain properties. Most importantly, the system has to be interpretable in a way that no statement can be proven both true and false. The technical term for this property is consistency. Another important property is completeness: that any sensibly composed string can be proven or disproven. Hence, if a system is incomplete, there exists a statement whose truth or falsity is undecidable within the system.

Since the nineteenth century, mathematics has been founded on a theory of sets, or collections of objects. Sets are defined by a rule which determines whether something is in the set or not – for example “the set of whole numbers which are even” is a set defined by a rule. Intuitively, you might want to create axioms of set theory which say that any object is either in a set or not in it, and that sets can be defined by any reasonable rule. These seem pretty self-evident, like axioms should be. Unfortunately, this leads to a contradiction, meaning the system is not consistent. From these axioms, Russell’s paradox follows: suppose X is a set that contains all sets that do not contain themselves. Does X contain itself? If so, then by definition it must not, and vice versa – a contradiction in either case.

At the time Russell’s paradox was discovered, most mathematicians believed that it was possible to establish a consistent and complete formal system that could be used as a foundation for mathematics. To avoid the kind of self-referential contradiction seen in Russell’s Paradox, Bertrand Russell and Alfred Whitehead created a complicated formal system in their work Principia Mathematica in 1910, which tried to avoid self-reference, but their efforts were proven futile by Kurt Gödel in 1931. In his paper, On Formally Undecidable Propositions of Principia Mathematica and Related Systems, Gödel proved that any formal system powerful enough to describe number theory, i.e. the properties of whole numbers, was either incomplete or inconsistent. This result is known as Gödel’s first incompleteness theorem.

Due to its technical nature, only the gist of the proof will be given. First, symbols in the formal system can be encoded as sequences of digits, meaning that strings become very large numbers. Then you pick some arbitrary string, aka number. The proposition that that string is provable can then be written as a number-theoretical statement. This way we can use number theory to talk about whether a statement of number theory is provable. Then, by a technical trick, the statement “This statement is not provable in the system” can be encoded. If this statement can be proven or disproven, it leads to a contradiction similar to Russell’s paradox, meaning the system is inconsistent. If it can’t be proven or disproven, then the system is, by definition, incomplete.

This result surprised many mathematicians and philosophers as it revealed some of the limitations of formal systems. Subsequent results by Gödel and others revealed further limitations. Therefore, we cannot create a perfect formal system where all mathematical patterns can be proven as theorems. There will be an eternal struggle to add new axioms and avoid contradictions, so that mathematicians will be able to formalise and prove their intuitions.