Russell’s discovery of a hidden contradiction in Frege’s attempt to formalize set theory, with the help of his simple comprehension scheme, caused some mathematicians to wonder how one could make sure that no other contradictions existed. Hilbert’s program, called formalism, was to concentrate on the formal language of mathematics and to study its syntax. In particular, the consistency of mathematics, which may be taken, for instance, to be the metamathematical assertion that the mathematical statement 0 = 1 is not provable, ought to be a metatheorem—that is, provable within the syntax of mathematics. This formalization project made sense only if the syntax of mathematics was consistent, for otherwise every syntactical statement would be provable, including that which asserts the consistency of mathematics.
Unfortunately, a consequence of Gödel’s incompleteness theorem is that the consistency of mathematics can be proved only in a language which is stronger than the language of mathematics itself. Yet, formalism is not dead—in fact, most pure mathematicians are tacit formalists—but the naive attempt to prove the consistency of mathematics in a weaker system had to be abandoned.
While no one, except an extremist intuitionist, will deny the importance of the language of mathematics, most mathematicians are also philosophical realists who believe that the words of this language denote entities in the real world. Following the Swiss mathematician Paul Bernays (1888–1977), this position is also called Platonism, since Plato believed that mathematical entities really exist.
Gödel
Implicit in Hilbert’s program had been the hope that the syntactic notion of provability would capture the semantic notion of truth. Gödel came up with the surprising discovery that this was not the case for type theory and related languages adequate for arithmetic, as long as the following assumptions are insisted upon:
- The set of true statements of mathematics is ω-complete in the following sense: given any formula ϕ(x), containing a free variable x of type N, the universal statement ∀x ∊ Nϕ(x) will be true if ϕ(n) is true for each numeral n—that is, for n = 0, n = S0, n = SS0, and so on.
- The language is consistent.
Actually, Gödel also made a somewhat stronger assumption, which, as the American mathematician J. Barkley Rosser later showed, could be replaced by assuming consistency. Gödel’s ingenious argument was based on the observation that syntactical statements about the language of mathematics can be translated into statements of arithmetic, hence into the language of mathematics. It was partly inspired by an argument that supposedly goes back to the ancient Greeks and which went something like this: Epimenides says that all Cretans are liars; Epimenides is a Cretan; hence Epimenides is a liar. Under the assumptions 1 and 2, Gödel constructed a mathematical statement g that is true but not provable. If it is assumed that all theorems are true, it follows that neither g nor ¬g is a theorem.
No mathematician doubts assumption 1; by looking at a purported proof of a theorem, suitably formalized, it is possible for a mathematician, or even a computer, to tell whether it is a proof. By listing all proofs in, say, alphabetic order, an effective enumeration of all theorems is obtained. Classical mathematicians also accept assumption 2 and therefore reluctantly agree with Gödel that, contrary to Hilbert’s expectation, there are true mathematical statements which are not provable.
However, moderate intuitionists could draw a different conclusion, because they are not committed to assumption 2. To them, the truth of the universal statement ∀x ∊ Nϕ(x) can be known only if the truth of ϕ(n) is known, for each natural number n, in a uniform way. This would not be the case, for example, if the proof of ϕ(n) increases in difficulty, hence in length, with n. Moderate intuitionists might therefore identify truth with provability and not be bothered by the fact that neither g nor ¬g is true, as they would not believe in the principle of the excluded third in the first place.
Intuitionists have always believed that, for a statement to be true, its truth must be knowable. Moreover, moderate intuitionists might concede to formalists that to say that a statement is known to be true is to say that it has been proved. Still, some intuitionists do not accept the above argument. Claiming that mathematics is language-independent, intuitionists would state that in Gödel’s metamathematical proof of his incompleteness theorem, citing ω-completeness to establish the truth of a universal statement yields a uniform proof of the latter after all.
Gödel considered himself to be a Platonist, inasmuch as he believed in a notion of absolute truth. He took it for granted, as do many mathematicians, that the set of true statements is ω-complete. Other logicians are more skeptical and want to replace the notion of truth by that of truth in a model. In fact, Gödel himself, in his completeness theorem, had shown that for a mathematical statement to be provable it is necessary and sufficient that it be true in every model. His incompleteness theorem now showed that truth in every ω-complete model is not sufficient for provability. This point will be returned to later, as the notion of model for type theory is most easily formulated with the help of category theory, although this is not the way Gödel himself proceeded. See below Gödel and category theory.
Recursive definitions
Peano had observed that addition of natural numbers can be defined recursively thus: x + 0 = x, x + Sy = S(x + y). Other numerical functions ℕk → ℕ that can be defined with the help of such a recursion scheme (and with the help of 0, S, and substitution) are called primitive recursive. Gödel used this concept to make precise what he meant by “effectively enumerable.” A set of natural numbers is said to be recursively enumerable if it consists of all f(n) with n ∊ ℕ, where f ∶ ℕ → ℕ is a primitive recursive function.
This notion can easily be extended to subsets of ℕk and, by a simple trick called arithmetization, to sets of strings of words in a language. Thus Gödel was able to assert that the set of theorems of mathematics is recursively enumerable, and, more recently, the American linguist Noam Chomsky (born 1928) could say that the set of grammatical sentences of a natural language, such as English, is recursively enumerable.
It is not difficult to show that all primitive recursive functions can be calculated. For example, to calculate x + y when x = 3 and y = 2, making use of Peano’s recursive definition of x + y and of the definitions 1 = S0, 2 = S1, and so on, one proceeds as follows:
3 + 2 = S2 + S1 = S(S2 + 1) = S(S2 + S0)
= SS(S2 + 0) = SSS2 = SS3 = S4 = 5.
But primitive recursive functions are not the only numerical functions that can be calculated. More general are the recursive functions, where f ∶ ℕ → ℕ is said to be recursive if its graph is recursively enumerable—that is, if there exist primitive recursive functions u, v ∶ ℕ → ℕ such that, for all natural numbers x and y, y = f(x) if and only if, for some z ∊ ℕ, x = u(z) and y = v(z).
All recursive functions can be calculated with pencil and paper or, even more primitively, by moving pebbles (calculi in Latin) from one location to another, using some finite set of instructions, nowadays called a program. Conversely, only recursive functions can be so calculated, or computed by a theoretical machine introduced by the English mathematician Alan Turing (1912–54), or by a modern computer, for that matter. The Church-Turing thesis asserts that the informal notion of calculability is completely captured by the formal notion of recursive functions and hence, in theory, replicable by a machine.
Gödel’s incompleteness theorem had proved that any useful formal mathematical system will contain undecidable propositions—propositions which can be neither proved nor disproved. Church and Turing, while seeking an algorithmic (mechanical) test for deciding theoremhood and thus potentially deleting nontheorems, proved independently, in 1936, that such an algorithmic method was impossible for the first-order predicate logic (see logic, history of: 20th-century logic). The Church-Turing theorem of undecidability, combined with the related result of the Polish-born American mathematician Alfred Tarski (1902–83) on undecidability of truth, eliminated the possibility of a purely mechanical device replacing mathematicians.
Computers and proof
While many mathematicians use computers only as word processors and for the purpose of communication, computer-assisted computations can be useful for discovering potential theorems. For example, the prime number theorem was first suggested as the result of extensive hand calculations on the prime numbers up to 3,000,000 by the Swiss mathematician Leonhard Euler (1707–83), a process that would have been greatly facilitated by the availability of a modern computer. Computers may also be helpful in completing proofs when there are a large number of cases to be considered. The renowned computer-aided proof of the four-colour mapping theorem by the American mathematicians Kenneth Appel (born 1932) and Wolfgang Haken (born 1928) even goes beyond this, as the computer helped to determine which cases were to be considered in the next step of the proof. Yet, in principle, computers cannot be asked to discover proofs, except in very restricted areas of mathematics—such as elementary Euclidean geometry—where the set of theorems happens to be recursive, as was proved by Tarski.
As the result of earlier investigations by Turing, Church, the American mathematician Haskell Brooks Curry (1900–82), and others, computer science has itself become a branch of mathematics. Thus, in theoretical computer science, the objects of study are not just theorems but also their proofs, as well as calculations, programs, and algorithms. Theoretical computer science turns out to have a close connection to category theory. Although this lies beyond the scope of this article, an indication will be given below.
