I recently read a book on Gödel’s Incompleteness Theorem. I’ll try to explain it if you’re not familiar with it, and then think about the implications for artificial intelligence.

Mathematicians require rigourous logical proofs for their hypotheses — unlike in the physical sciences, where theories are developed by observation and experiment.

However, you can’t prove everything; you have to start somewhere. Maths is based on a set of initial assumptions, called **axioms**, such as “parallel lines never meet”. The axioms of arithmetic for natural numbers might go something like this:

- Zero is a number.
- Every number has an immediate successor.
- There is no number whose successor is zero…

…and so on.

A mathematical system — such as elementary logic, presented in the book — consists of a set of axioms together with a fixed set of **rules of inference**, which describe how to derive further theorems within the system as a consequence of the axioms. For example, one rule of inference in elementary logic is the Rule of Detachment: if you can derive the formulas *“A”* and *“if A, then B”* from the axioms, then the formula *“B”* is proved also.

Mathematical proofs are sequences of statements starting from initial axioms (or alternatively, from statements already proved). Each following statement is derived from the previous one by the application of one of the rules of inference, such that each one is proved, until we arrive at the final concluding statement.

For elementary logic, we can prove the system both consistent and complete from within the system itself. **Consistent** means that there are no contradictions; given a statement *“S”*, you can’t prove both *“S”* and *“not S”*. **Complete** means that every statement is decidable; it’s possible to determine the truth or falsity of every formula that can be expressed in the formal language of the system — which is done by deriving the formula or its negation (*“not S”*).

So, an axiomatic system consists of:

- a formal syntax for writing formulas
- some initial axioms, formulas that are assumed to be true
- a set of rules of inference, for deriving new statements.

For most more complicated mathematical systems, we can’t prove them to be consistent and/or complete from within the system. We can use higher, more complex systems to prove them consistent — but this just brings the same problem to another level.

Mathematicians in the 1900s were worried about consistency: they thought that the maths they used might contain contradictions or paradoxes (such as Russell’s paradox). Hilbert wanted to find an axiomatic system as a foundation from which the rest of mathematics could be derived. It needed to be sufficiently complex to represent all mathematical truths, questions, statements… so that geometry could be reduced to algebra, and algebra to arithmetic. By proving this system consistent, all of mathematical reasoning could then be shown to be consistent and free from contradiction.

By mapping each formula within the system to a unique number, Gödel essentially constructed the mathematical equivalent of the statement:

This statement is not provable.

…and showed that this statement must be undecidable within the system.

He therefore famously proved that any finite consistent axiomatic system has undecidable statements: statements that we know to be true, but that can’t be proved within the system. This applies to systems complex enough to include whole numbers. He also showed that you can’t prove the consistency of such a system from within the system.

Godel’s proof destroys Hilbert’s dream; any axiomatic system will always contain statements whose truth or falsity cannot be derived within the system. You can add an extra axiom to solve the problem — but there are still other statements that are still undecidable. You can use a higher, more complex system to decide the statement — but again, this just brings the same problem to another level.

It means that mathematics (and, probably, all science and knowledge) will never be finished — there will always be new problems to solve, with new methods of solving to discover.

The book summarises this in *VIII Concluding Remarks, p98*:

It follows that an axiomatic approach to number theory, for example, cannot exhaust the domain of arithmetical truth. It follows, also, that what we understand by the process of mathematical proof does not coincide with the exploitation of a formalized axiomatic method… as Gödel’s own arguments show, no antecedent limits can be placed on the inventiveness of mathematicians in devising new rules of proof.

For me, I’m not sure about “new *rules* of proof” in that last part — new methods of proof might make more sense. But I suppose the point is that the mathematician is free to use the existing rules of inference in new ways; extend the rules of the system; or indeed create an entirely new system, in order to solve his or her problem.

*Maybe sometime I’ll write a post about what I think this all means for my quest to build artificial intelligence.*