by Scott Soames
The Gödel-Tarski theorem of the arithmetical indefinability of arithmetical truth is an application of this result to the language, LA, of arithmetic. In proving it we take the predicates of LA to be formulas in which a single variable ‘x’ occurs free (not bound by any quantifier). If P is such a predicate, a self-ascription of P is a sentence we get by substituting the numeral that names the code (i.e., the Gödel number) of P for all free occurrences ‘x’ in P. Now consider the relation that holds between numbers n and m if and only if m is the code of a predicate P and n is the code of a self-ascription of P. Since this relation is effectively decidable, there is a formula Self-Ascription x, y of LA that is true of numbers n and m if and only if m is the code of a predicate P, and n is the code of its self-ascription, i.e., of the sentence that predicates P of its own code. Finally, suppose there is a formula T(x) of LA that is true of all and only the codes of true sentences of LA. Then, the formula For some x (Self-Ascription x, y & ~ T(x)) is a heterologicality predicate of LA; it is true of m if and only if m is the code of a predicate of LA that isn’t true of its own code. Let h* be the numeral that denotes the Gödel number of this heterologicality predicate. Then For some x (Self-Ascription x, h* & ~T(x)) is a sentence of LA that says that some self-ascription of the heterologicality predicate isn’t true. Since this very sentence is the self-ascription of the heterologicality predicate, it says of itself that it isn’t true. In other words, it is a liar sentence that says I’m not true, and so is true if and only if it is not true. Thus, the supposition that there is a predicate of LA that is true of all and only the codes of its true sentences leads to the result that LA contains a sentence that is true if it is not true, and not true if it is true. Assuming that it must be one or the other, but not both, we conclude that there is no such sentence. Thus, the supposition that led to this result—namely that arithmetical truth is arithmetically definable—is false. This is the Gödel-Tarski proof that arithmetical truth is not arithmetically definable.
This theorem is an application of Gödel’s first incompleteness theorem, which states that for every consistent proof procedure of first-order arithmetic, there are pairs of sentences S and ~ S that it can’t prove. Since a proof is a finite sequence of formulas, we can assign a Gödel number to each proof. Now consider the proof relation that holds between numbers n and m if and only if n is the code of a proof of a sentence with code m. This relation is effectively decidable, since we can always decide, for any m and n, whether m is the code of a sentence S and n is the code of a sequence of formulas the last member of which is S, and given any such sequence, we can always determine whether each formula is an axiom or a consequence of earlier formulas via one of the rules of inference.
Since the proof relation is decidable, there is a formula, Proof (x, y), of LA that is true of numbers n and m if and only if n is the numerical code of a proof of the sentence that m codes. Next consider the formula For some y Proof (y, x)—or Prov x (for short)—which is true of the codes of provable sentences. Since this set is definable in LA, but, as we have just seen, the set of arithmetical truths isn’t definable in LA, the set of truths isn’t the same as the set of provable sentences. So, if all provable sentences are true, some truths can’t be proved in the system. This is the simplest version of Gödel’s first incompleteness theorem.
GÖDEL’S ORIGINAL METHOD*
Gödel’s own method of proving this result was a little different. The key predicate in his proof was G1, the self-ascription of which was G2.
G1. For some x (x is a Self-Ascription of y & ~ for some z Proof (z, x))
G2. For some x (x is a Self-Ascription of [k] & ~ for some z Proof (z, x))
G1 is true of all and only codes of predicates the self-ascriptions of which are not provable; in short, G is true of predicates that aren’t provable of themselves. Let k be the code of G1 and ‘[k]’ be the numeral denoting k. G2 says that a self-ascription of G1 is not provable. Since G2 is the self-ascription of G1, G2 says that G2 isn’t provable. Thus, it is either true and unprovable, or false and provable. Assuming no falsehoods are provable, it must be true and not provable.
When we present Gödel’s result this way, we prove—reasoning informally in a technical extension of ordinary English we use to speak about the language LA—that a sentence of LA saying of itself that it isn’t provable (using a consistent proof theory T) isn’t a theorem of T (i.e., isn’t provable in T). Are there any theorems of T that themselves assert what we just asserted? Gödel showed that there are. He showed there are theorems of T—G if and only if ~ Prov G (where G denotes the Gödel number of G)—that assert that G is true if and only if G is unprovable in T. From this it follows that G isn’t a theorem of T, for if it were, some natural number n would be the Gödel number of a proof of G in T, in which case Proof (n*, G) would be a theorem of T (where n* is the numeral denoting n), thereby guaranteeing that For some x Proof (x, G)—i.e., Prove G—was also a theorem of T. This is impossible, since if G were a theorem, it would mean that both Prov G and its negation ~ Prov G were both theorems. Thus, the simple logical consistency of T ensures that G isn’t a theorem of T.
Given this, we also know that ~Proof n, G is a theorem of T for all natural numbers n. It might seem to follow directly that ~G isn’t a theorem, and hence that T is incomplete. But, due to certain complications, it doesn’t follow unless one uses a notion of consistency slightly stronger than logical consistency, which Gödel did in 1931. Barkley Rosser, who was a student of Alonzo Church, showed in Rosser (1937) that simple logical consistency is enough by focusing on a slightly different class of unprovable sentences.9
THE DIFFERENCE BETWEEN THE FIRST- AND SECOND-ORDER PREDICATE CALCULUS*
At this point, it is worth saying a word about the difference between arithmetical theories formulated in first-order logic and those formulated in second-order logic. Recall, first-order logic has statements For all x … x … that make general claims about all individual objects in the domain of the model (interpretation) of the language of the theory—in this case the language, LA, of arithmetic. In addition to these, second-order logic also has statements For all P … P … that make claims about all sets of objects in the domain.10 If that domain is the set of natural numbers, then sentences of the first-order predicate calculus can make statements about all of them, while sentences of the second-order predicate calculus can also make statements about all sets of natural numbers. A key difference between first- and second-order theories of arithmetic is that the most interesting first-order theories include the first-order axiom schema of mathematical induction, while the most interesting second-order theories include the second-order axiom of mathematical induction.
The former is expressed
[(F(0) & for all x (F(x) → F(S(x)))) → for all x F(x)]
To include this axiom schema in a theory is to take its infinitely many instances as axioms of the theory. Each instance is formed by (i) replacing ‘Fx’ with a 1-place predicate of LA—i.e., with a formula of LA in which only the variable ‘x’ has free occurrences; (ii) replacing ‘F(0)’ with the result of replacing free occurrences of ‘x’ in that formula with occurrences of ‘0’; and (iii) treating ‘S(x)’ as designating the successor of the number ‘x’ designates. So understood, an instance of the schema (i.e., one of the infinitely many axioms the schema introduces) is true if and only if the predicate that replaces ‘Fx’ is true of everything in the domain, whenever it is true of zero and also true of the successor of anything it is true of. When the domain consists simply of the natural numbers, each of these axioms tells us that if zero is a member of the set of numbers of which the predicate is true, and if, whenever a number is in that set, its successor is too, then all natural numbers are in the set. By contrast, the second-order axiom of induction is expressed
For all P [(P(0) & for all x (P(x) → P (S(x)))) → for all x P(x)]
It is true if and only if any set of natural numbers that contains zero, and also contains the s
uccessor of anything it contains, contains every natural number.
The schema and the single axiom are different because there are vastly more sets of natural numbers than there are predicates of the first-order language of arithmetic. Hence, there are vastly more sets of natural numbers than there are sets of natural numbers designated by those predicates. Because of this, the set of logical consequences of second-order theories of arithmetic include many more statements about the natural numbers than the set of logical consequences of the corresponding first-order theories do. In fact, it is easy to show that all true first-order sentences of LA are logical consequences of certain arithmetical theories incorporating the second-order axiom schema of mathematical induction. This means that consistent second-order theories of arithmetic are complete in the sense in which Gödel’s first incompleteness theorem shows that no consistent first-order theory can be.11
But this doesn’t subvert the earlier theorem. Although all first-order truths of arithmetic are logical consequences of a certain second-order arithmetical theory, second-order logic is not complete in the sense in which first-order logic was proved complete by Gödel. In first-order logic, every logical truth is provable from a consistent set of logical axioms and rules of inference. Similarly, every logical consequence B of a first-order sentence A (or of a decidable set A* of first-order sentences) is provable from A (or from a finite subset of A*). By contrast, second-order logic is not complete in this sense. For any consistent system of proof for second-order logic, there will be second-order logical truths that are not provable in the system, and there will be logical consequences of second-order sentences that are not provable from those sentences in the system. So, although the relevant second-order arithmetic is a complete formal theory that, for each first-order arithmetical sentence S, has S or ⎡~S⎤ as a logical consequence, the fact that no proof procedure in second-order logic is complete—in the sense in which some first-order proof procedures are complete—means that there is no effective positive test for first-order arithmetical truth. Thus, the central lesson of Gödel’s first incompleteness proof is untouched.
GÖDEL’S SECOND INCOMPLETENESS THEOREM*
Gödel’s second incompleteness theorem extended his incompleteness result by showing that strong, logically consistent, first-order theories of arithmetic like Peano Arithmetic can’t prove their own consistency—i.e., although they don’t prove contradictions, they can’t prove theorems that say, relative to a system of Gödel numbering, that they don’t prove contradictions.12 Put simply, the idea is this. We know from Gödel’s first incompleteness theorem that if a sufficiently powerful arithmetical theory, e.g., Peano Arithmetic (PA), is consistent, then G isn’t provable in PA, but G ↔ ~Prov G is provable in PA. (In effect, G “asserts” its own unprovability.)
This is expressed in PA by the fact that ConPA → ~Prov G and G ↔ ~Prov G are both theorems of PA, where ConPA “says,” relative to the Gödel numbering, that PA is consistent—in the sense that we can establish, when reasoning about the system, that ConPA is a theorem of PA only if the set of theorems of PA is logically consistent. If ConPA were also provable in PA (and hence a theorem), then ~Prov G and G ↔ ~Prov G would both be theorems. Hence, G would be a theorem of PA, as would Proof (n*, G) (where n* is the numeral denoting a proof in PA of G). This would then guarantee that For some x Proof (x, G))—i.e., Prov G—is also a theorem. But then the theorems of PA would be inconsistent, since its theorems would include both Prov G and ~Prov G. Since we know that Peano Arithmetic is consistent, this means that ConPA isn’t provable in Peano Arithmetic. In short, consistent first-order theories of arithmetic can’t prove their own consistency (even though they are, in fact, consistent).13
PROOF AND EFFECTIVE COMPUTABILITY
One of the important lessons of Gödel’s results is that there is an intimate connection between effective computability and proof in a formal system. Proof in these systems is an effectively decidable notion, and systematic searches for proofs can be used as decision procedures for determining membership in decidable sets of natural numbers. This close relationship between computability and logic was studied by the mathematician and philosopher Alonzo Church and his students Barkley Rosser, Stephen Kleene, and Alan Turing in the 1930s. In 1934, Gödel introduced a mathematical formalization of the notion of an effectively computable function; in 1936 Church proved his own formalization to be equivalent to Gödel’s.14 He also used Gödel’s first incompleteness theorem, to prove that there is no effective procedure capable of always deciding whether or not a sentence of first-order logic is, or isn’t, a logical truth (or a logical consequence of other first-order sentences).15
His proof is based on a Gödel-sentence G that “says,” relative to the coding of sentences by Gödel numbers, that G is unprovable. G is the self-ascription of the predicate of LA that is true of all and only the Gödel numbers of predicates of LA that are not provable of themselves. Since Proof encodes a decidable relation, whenever two numbers stand in that relation some theorem of our arithmetical theory says they do, and whenever they don’t stand in that relation some theorem says they don’t. With this in mind, consider the 1-place predicate For some x, Proof x,y. Although it is true of all and only numbers that encode provable sentences, this doesn’t guarantee that whenever a sentence isn’t provable some theorem of PA says it isn’t. If it did, then, as Gödel showed, the fact that G is unprovable in PA would guarantee that the negation of [For some x, Proof x,G] was provable, from which it would follow that G was provable after all. This means that when a sentence isn’t a logical consequence of the axioms of the theory, the theory won’t always tell us that it isn’t.
This proves Church’s undecidability theorem. For suppose first-order logical consequence were effectively decidable. Then the set of logical consequences of the axioms of our theory would decidable. By the completeness of first-order logic, the logical consequences of our theory are its theorems. So, if logical consequence were decidable, some theorem of our theory would tell us the G is unprovable in the theory. Since we have shown that no theorem of the theory tells us this, we know that first-order logic is undecidable.16
Church’s future student Alan Turing independently proved the same result by a different method using a new mathematical model of the intuitive notion of a computable function.17 In his review of Turing’s work, Church called the model, which was provably equivalent to his own and Gödel’s formalizations, a Turing machine.18 In reality, a Turing “machine” is a kind of abstract mathematical program that a merely imagined machine could run. The imagined machine operates on an infinite tape divided into squares, each of which is either blank or imprinted with a single dot. It moves along the tape one square at a time, checking to see whether or not the square it is on is blank. It can also print a dot on a previously blank square or erase a dot on a square that had one. It has a finite number of internal states; its instructions tell it what to do—move left, move right, erase a dot, or print a dot—based on the state it is in at a given time.19
There are several key features of Turing machines. First, they are digital, operating on 0’s and 1’s (blank squares and squares with a dot) that model the two positions, open and closed, of an electrical circuit. Second, their instructions, which determine their operation at every moment, can be encoded by sentences of the first-order predicate calculus. Third, they are universal—i.e., Turing machines are capable of computing every function that can be shown to be computable by any means whatsoever. Fourth, there is no decision procedure for deciding in every case whether an arbitrary Turing machine will eventually halt (and provide an interpretable output) after having been started on an arbitrary input.
However, there would be such a procedure, if there were a decision procedure for determining whether any arbitrary sentence of first-order logic was a logical consequence of an arbitrary set of other first-order sentences. For each Turing machine T there is a set IT of sentences of the logic encoding its instructions, and
for each input to T there is a sentence S that describes that input. There is also a sentence H of the logic that is true if and only if T ever halts. H will be a logical consequence of IT plus S, if and only if T ever halts. So, if we could always decide whether one thing was a logical consequence of something else, the halting problem for Turing machines would be solvable. Since we know it isn’t solvable, there must be no decision procedure for deciding first-order logical consequence. That was Turing’s version of Church’s undecidability theorem.
Since Church’s result narrowly preceded Turing’s, the interest in Turing’s proof lay not in what it proved, but in the brilliant model of computability he used to prove it. In addition to being conceptually transparent, it was technologically feasible, and so able to provide the mathematical basis for electronic computing, which began not long after his discovery. This, in short, is how the turn to logic and language initiated by Frege, Russell, Tarski, Gödel, Church, and Turing ushered in the modern digital age that has contributed so much to the world we now inhabit.
In addition to leading to stunning technological advances, digital computers also helped to launch what we now call cognitive science, which combines psychology, artificial intelligence, and computation theory. It soon became clear that digital computers could imitate, duplicate, or actually perform a range of demanding intellectual tasks that skilled human beings perform intelligently. This gave rise to questions: What is the range of such tasks? Are there limits to it? Assuming, as seems natural, that computers could, in principle, at least imitate intelligent human performance, what, if anything, should stop us from recognizing them as intelligent thinkers? Turing himself introduced fascinating philosophical speculation on these matters in “Computing Machinery and Intelligence,” published in 1950. Whatever one might think of speculation along these lines, it now seems clear that studying the cognitive architectures of human beings and computing machines are complementary enterprises, each capable of positively influencing the other.
