1) Computing machines are essentially formal systems.

The Background to Gödel's Proof

Context
 
By the turn of the 20th century a crisis had developed in the foundations of mathematics. The discovery of fundamental paradoxes led to concern about the basic concepts of math and logic. In response to those concerns, mathematicians tried to develop more secure foundational systems.

One such system, the Principia Mathematica of Bertrand Russell and Alfred North Whitehead, was widely received and provided a framework to subsequent work on the foundations of arithmetic geometry, analysis and algebra. Concurrently with Russell and Whitehead, David Hilbert worked on foundational systems in Germany. Hilbert's central idea was that the consistency of mathematics can be shown by a system of metamathematics—a system of mathematics about mathematics.

The work of Kurt Gödel was situated in this context. He set out to apply the recently developed methods to his own areas of interest, and shortly thereafter discover the proof for his famous incompleteness theorem is.

Method

Gödel developed a numbering system that allowed him to include formal mathematical proofs into numeric expressions. The numeric expressions—or Gödel numerals—can be recognised and manipulated within the Principia system in the same way that any numerals could be. Gödel numerals allowed the Principia—and formal systems generally—to look at themselves and to say things about themselves. Through this method, Gödel wanted to find out whether the formal system of Principia Mathematica could prove itself consistent.

He discovered that no such proof exists. There is no way from the Principia to prove itself consistent. Gödel went further and used his method to prove that no complete formalisation of arithmetic exists at all (Gödel's first theorem). As a corollary, he returned to the consistency question and showed that no consistent formal system of arithmetic could be proved consistent using only its own methods of proof (Gödel's second theorem).

Earlier precedents
 
Gödel wasn't the first to suspect that his completeness and consistency results held. Earlier, Finsler (1926) presented an idea similar to Gödel's but without showing how to formalise the argument. Because he did not deal with aspecific formal system, Finsler could not present any actual proof of his claim. The American mathematician Emil Post had also proved a result equivalent to Gödel's, but his work wasn't published.

Suggested reading

Readable discussions of Gödel's theorem includes Hofstadter (1978, and Nagel and Newman (1958). Smullyan (1987) teaches Gödel's theorem to a series of puzzles. An introduction with applications to computers is Harrell (1887). For historical context, see Rucker (1987), Davies (1965), Dawson (1984a, 1984b), and van Heijenoort (1967). This last volume reprints Gödel's original paper.

The Steps of Gödel's Proof

1) The Principia Mathematica gave Gödel a way to translate natural language statements into a formal system of proof. With this formal system in hand, Gödel was able to prove that all such systems strong enough to produce arithmetic are inherently limited. Illustration of the proof begins with an English version of what will become the notorious Gödel sentence: "G says it is not provable that G."

2) In step two, the sentence is roughly translated into the formal system of Principia Mathematica. The formalisation shown here is not well formed (i.e. it is not grammatically correct), and consequently the system of proof used in Principia Mathematica cannot be applied to it. To make the sentence truly self-referential and well formed we must first develop a way to make well formed sentences that refer to themselves.

3) To that end, each symbol in the formal system is replaced with a code number.

4) Those numbers are then used as exponents in a series of prime numbers that will be multiplied together into one large Gödel number. This step ensures that every Gödel number corresponds to one and only one formula in the formal system of Principia Mathematica.

5) This number is then represented symbolically in this case by a long string of S's followed by zero (where the number of S'sis equal to the Gödel number). The symbolic numeral representation is necessary that the Gödel number can be dealt with formally in the Principia Mathematica.

6) This numeral representation for Gödel numbers allows us to use Principia Mathematica to "talk about itself". In particular, we can plug the Gödel numeral for G back into the formula itself. This genrates a well-formed Gödel sentence that makes reference to itself, and that can be assessed using the proof system of Principia Mathematica.

7) Now we are in a position to show that the Gödel sentence is neither provable or disprovable using the system of Principia Mathematica. To see how the paradox works see "Self-referential paradoxes" on this map.

8) However, the Gödel sentence can be recognised to be a true from outside of the system. This is the aspect of the proof that later interpreters would focus on in the context of machine intelligence.

Various authors, notably John Lucas and Roger Penrose, extended Gödelian insight to computers. They pointed out that because computers are a kind of formal system, the same limitations discovered by Gödel in Principia Mathematica and other formal systems might apply to computers as well.

Note: A variety of simplifications have been used in order to illustrate in a readable way the general idea behind Gödel's extremely complex proof: 

• Gödel does not begin with a non-well formed formula and then fix it as we've done—this is just rhetorically useful way to present the proof.

• The Gödel sentence does not make reference to itself in the simple ways suggested by the its informal versions. The numeral for G—and the sentence G itself—correspond precisely in that there is a one-to-one coding between them, but they do not have the same “meaning.” They are “extensionally equivalent” but not “intensionally equivalent.”

Formal Systems: An Overview

David Hilbert laid many of the foundations for what are now known as formal systems. His formalist program aimed to develop axioms that would yield the desired truths of math and geometry, without reliance on intuition. These axioms would be true regardless of whether they were interpreted in terms of points, lines, planes, or in terms of "law, love, and chimney sweeps".

Formal systems allow mathematical results to be described and assessed with increased precision, and are particularly useful with theories that deal with more than three dimensions.

In a formal system, the whole process of proof is reduced to the manipulation of symbols according to rules that complicitly determine the conclusions that can be drawn from a set of axioms. Intuitions about the "meaning" of the symbols play no role in the workings of the formal system. Such meanings are only introduced with the interpretation of the system.

Below is an example of a simple formal system designed for application to the logic of truth. Note that in addition to the standard interpretation in terms of truth, there are also other interpretations that satisfy the formal system (for more explanation see "The Lowenheim-Skolem Theorem" Map 3 Box 107).

This formal system is not complete with respect to the logic of truth; that is it does not yield all valid formulas of the logic of truth. But recall that it does not even make sense to ask whether the system iteslf is complete or correct; the system in itself is just an orderly set of patterns of symbols with rules to govern their recombination.

For more on formal systems, see Map 4 and the "Can functional states generate consciousness?" argument on Map 6.

Follow the links below for Robert Horn's original information boxes on:

1) The background to Godel's proof

2) The steps of Godel's proof

3) Self-referential paradoxes

4) Formal Systems: An Overview

5) Alternate versions of Godel's theorem