by Scott Soames
Apart from this continuing line of philosophical inquiry, what were the most important and clear-cut achievements growing out of the Frege-Russell attempt to ground mathematics? Their most important advance was the invention of powerful new systems of logic that are vital to deductive reasoning in all scientific domains. Another was the impetus they provided for the development of set theory as the dominant foundational system for unifying mathematics. In the next two chapters I will explain how the contributions of Frege and Russell started us on the road to the formal notion of computation that sparked the digital age (and the development of contemporary cognitive science) and also laid the foundations of the still young science of linguistic meaning and the use of language to encode information about the world.
CHAPTER 6
LOGIC, COMPUTATION, AND THE BIRTH OF THE DIGITAL AGE
The fundamentals of modern logic; results about logical systems; how to logically demonstrate the limits of logic: the strategy behind Gödel’s first incompleteness theorem; Gödel’s original method; lower and higher-order logics; Gödel’s second incompleteness theorem; proof, effective computability, and Turing machines as mathematical prototypes of real computers.
Invented by Frege in 1879 and put to philosophical use by Frege and Russell over the next four decades, modern symbolic logic emerged as an independent scientific discipline between 1929 and 1939, primarily through the unprecedented advances of four philosophically minded mathematical logicians—Kurt Gödel (1906–1978), Alfred Tarski (1901–1983), Alonzo Church (1903–1995), and Alan Turing (1912–1954). It was then that the now standard understanding of what logic is, what it is capable of achieving, and what is demonstrably beyond its limits were put in place. It was also then that the link between logic and computability, and ultimately digital computability, was forged, leading to the electronic processing of information that has transformed the age in which we live.
The transformation began with Frege’s new system, the predicate calculus, which vastly expanded the expressive power of logical systems. This was accompanied by proof procedures that are effectively decidable in the sense that whether something offered as a proof really is a proof can always be uncontroversially decided by a purely mechanical procedure. In the decades following Frege, the form of guaranteed truth preservation known as logical consequence—which proofs are intended to verify—was defined in a way that allows mathematical investigation of proof procedures to determine whether (i) B is a logical consequence of A, whenever there is a proof of B from A, and whether (ii) there is a proof of B from A, whenever B is a logical consequence of A. These investigations established versions of the predicate calculus for which there are proof procedures satisfying both (i) and (ii), as well as versions, with greater expressive power, for which only (i) can be satisfied. Next, taking an arithmetical theory to include all logical consequences of an effectively decidable set of axioms, Gödel showed that it is impossible to construct a proof procedure that allows one to prove all and only the truths of elementary arithmetic; in fact, every such system that doesn’t prove contradictions leaves infinitely many arithmetical truths unproven.
It was then that the connection between logic and computability became clear. Whenever membership in a set (or sequence) of natural numbers can be effectively decided, there is a formula (sometimes very complex) of the language, LA, of elementary arithmetic that is true of all and only the members of that set. There are also axiomatic theories T of arithmetic such that for every decidable set S of natural numbers (or sequences of such), there is a formula F of LA and theorem Tyes of T that says of F that it is true of a particular number n (or sequence of numbers), whenever n (or the sequence) really is a member of S; there is also a theorem Tno of T, that says of F that it isn’t true of n (or a sequence), whenever n (or the sequence) isn’t a member of S. Given this, one can use systematic searches for theorems as effective decision procedures for membership in any decidable set of natural numbers (or sequences of such). Since Gödel also showed how to use natural numbers to code things that aren’t natural numbers, this result can be extended to decision procedures for any decidable set, as well as for any intuitively computable function.
Having come this far, we were now only one step away from the digital age. That step was taken by Turing, who articulated a new mathematical framework for formalizing the idea of computable function. Although the functions counted as Turing computable were the same as those counted computable by Gödel and Church, the means Turing used to compute them had far-reaching implications. What he gave us were logico-mathematical instructions for operating on sequences of 1’s and 0’s. Since the operations were digital, the 0’s and 1’s could be taken to model the two positions, open and closed, of an electric circuit, which meant that his instructions could be seen as encoding internal states of imagined machines. Despite the intervention of World War II, it was not long before these abstract models were turned into real machines.
What follows will add enough detail to this sketch to allow those who wish to get an idea of the main lines of argument, while leaving aside the most daunting technical refinements, of which there are many. Since the results achieved were among the greatest intellectual advances of the twentieth century, even the simplified story told here may include some elements that those new to the subject may find challenging. The goal is to provide interested readers with enough to deepen their knowledge. Asterisks (*) identify sections that deal with somewhat more technical material; those whose interests lie elsewhere can skip these without losing the thread.
FUNDAMENTALS OF MODERN LOGIC
The most important logical notions are truth, proof, and guaranteed truth preservation. If A is a logical consequence of B, then if A turns out to be true, its truth will guarantee that of B. In such a case, we may try to construct a proof of B from A—a sequence of obvious steps each of which is a logical consequence of earlier steps. While we may hope that there is a proof of B from A whenever B is a logical consequence of A, what we demand is that whenever there is a proof, B is, in fact, a logical consequence of A. Some logical systems justify our hope, because all logical consequences of a set of sentences are provable from that set. But, as indicated above, in other cases the expressive power of the system makes this impossible.
Making these ideas precise requires understanding the sense in which, when B is a logical consequence of A, A’s truth guarantees B’s truth. The intuitive idea is that if B is a logical consequence of A, it is impossible for A to be true without B being true. In addition, this impossibility mustn’t depend on the special subject matter of A or B—e.g., on the essences of objects and properties designated by terms in A and B. Rather, the necessary connection must be due to the structures, or forms, of the sentences A and B alone. Finally, if one doesn’t know B, but does know A, it should be possible to come to know B without appealing to information not contained in A or B, provided one can derive B from A by obvious steps, each of which is a logical consequence of earlier steps.
Although these ideas have always guided the construction of logical systems, Frege’s invention of the modern predicate calculus brought them to a higher level. His system was the result of combining the truth-functional logic of the propositional calculus—familiar from the Stoics onward—with a new analysis of sentences containing ‘all’ and ‘some’, used to make general claims. The key to Frege’s achievement was his decision to trade the subject/predicate distinction of Aristotelian logic for a clarified and expanded version of the function/argument distinction from mathematics. This allowed him to assign functions—from (sequences of) objects to truth or falsity—to each of the infinitely many formulas of his logical language. When ‘all’ and ‘some’ were attached to a formula F, the resulting sentence was taken to be true if and only if the function designated by F assigned truth to all or some objects. In this way, infinitely many patterns of logically valid arguments were generated.1
A system of logic, in Frege’s modern sense, always st
arts with a precisely specified language consisting of (i) an exhaustive inventory of names, simple predicate symbols, function signs, and the like, (ii) an unambiguous rule for combining them to form simple (atomic) sentences, and (iii) further rules for forming complex sentences out of simple ones. The result is a set of well-formed sentences and formulas leaving no room for doubt about whether a string of symbols is, or is not, a member of the set.
To this, one adds a proof procedure, which, in Frege’s case, was a set of axioms drawn from the language, plus a fixed number of rules of inference. As explained in chapter 5, a proof in the system is a finite sequence of lines, each of which is an axiom or a formula obtainable from earlier lines by the inference rules. Whether or not something counts as a proof must, in principle, be decidable merely by inspecting the formula on each line, and determining (i) whether it is an axiom, and (ii) whether, if it isn’t, it bears the required structural relation to earlier lines in order for it to be obtainable from those lines by the rules of inference. For this reason, the axioms themselves must be an effectively decidable set—that is, there must be a purely mechanical procedure capable of deciding, in every case, whether a formula is one of the axioms. Similarly, rules of inference must be stated so that whether or not a formula is obtainable from earlier ones is effectively decidable in the same sense. When these requirements are met, the question of whether or not something counts as a proof can always be resolved—thereby forestalling the need to prove that something is a proof.
Frege’s method of interpreting formulas and sentences of his logical language, which was also set out in chapter 5, gives us an assignment of truth conditions to each sentence of the language. What were there called models are interpretations of the language that arise from selecting a domain D of objects and assigning objects in D as referents of names, assigning sets of objects in D (or of pairs, triples, etc. of those objects) as referents of predicates, and assigning n-place functions (e.g., the addition function) defined on objects in D (when D includes the natural numbers) as referents of n-place function signs (e.g., ‘+’).
This allows us to define truth in a model, from which we define logical consequence. A sentence B is a logical consequence of a set S of sentences of the language if and only if B is true in every model (interpretation) of the language in which A is. One can now see the sense in which, when B is a logical consequence of a sentence or set S of sentences, the truth of S guarantees the truth of B. The truth of S is sufficient for the truth of B, no matter how the vocabulary—the names, predicates, and function signs—are interpreted, and no matter which, or how many, objects are under discussion. Because the guarantee is determined by the forms of the sentences themselves, it is independent of their subject matter. Thus, it is impossible for the claims S is used to make to be true without the claim B is used to make also being true. Finally, suppose one understands the sentences in S and knows the truths they express, while understanding B, but not knowing whether the claim it expresses is true. One can, in principle, come to know that claim by reasoning alone, without appealing to further information, if one can derive B from S via a proof each line of which is a logical consequence (in the sense we have defined) of earlier lines.
These ideas are central to understanding the tradition of modern logic initiated by Frege. It should be noted, however, that the concept truth in a model, in terms of which the modern concept logical consequence is now defined, wasn’t explicit in Frege, and would not become so until those concepts were introduced by Tarski in two classic papers, “The Concept of Truth in Formalized Languages,” published in 1935, and “On the Concept of Logical Consequence,” published in 1936.2 The importance of these papers was in making fully precise what had tacitly been understood for some time.3
THE SCOPE AND LIMITS OF LOGICAL SYSTEMS
Tarski’s formalizations validated the idea that one could construct mathematical metatheories to investigate the logical properties of Frege-style systems of logic, and of broader theories incorporating them as parts. In particular, one can prove metatheorems about the relationship between the syntactically defined provable sentences of a given logical system and its semantically defined logical truths. One can also prove metatheorems about the relationship between the provable sentences of specific theories of arithmetic (which include both logical and strictly arithmetical axioms) and the logical consequences of those axioms. Some of these turned out to be surprising.
In 1930, Gödel proved an important metatheorem of the first kind.4 He showed that it is possible to construct a sound proof procedure (which allows one to derive B from A only when B is a logical consequence of A) for the Fregean predicate calculus that is also complete in the sense that it always allows one to derive B from A, whenever B is a logical consequence of A. In such a system, the sentences of the logical language that are derivable from A are all and only the logical consequences of A. So, if B is a logical consequence of A, one can always find a proof of B if one looks long enough.
This result applies only to the first-order predicate calculus. A logical language is first-order if its only sentences that make general claims are those containing all and some in which these expressions (called ‘quantifiers’) combine with individual variables (x, y, z) that range over individual objects and that occupy the same position in formulas as proper names for those objects—e.g., For all x (if x is a man, then x is mortal). By contrast, a second-order language also has sentences that make general claims in which all and some combine with predicate and/or function variables, which range over (i) arbitrary sets of individual objects (or sequences of such) and/or (ii) functions, and which (iii) occupy the same position in formulas as predicate constants or function signs—e.g., For all P (if Socrates is P, then Socrates is P). Although Frege’s original logical system allowed both first- and second-order quantification, the first-order fragment of it was complete in the sense of Gödel’s 1930 theorem, which the latter proved 50 years after Frege presented his system. What Frege didn’t know then was that for second-order systems, no complete proof procedure is possible, which, as we will see, is a corollary of another one of Gödel’s revolutionary metatheorems.5
THE STRATEGY BEHIND GÖDEL’S FIRST INCOMPLETENESS THEOREM
Gödel’s completeness proof for the first-order predicate calculus was first presented in his 1929 doctoral dissertation. Also in 1929, he was named, along with 13 other founding members of the Vienna Circle, in its founding document, “The Scientific Conception of the World,” announcing logical empiricism as a new school of philosophy centered on logic and the philosophy of science.6 In 1931, he proved two revolutionary theorems. One has come to be called the Gödel-Tarski theorem that arithmetical truth is not arithmetically definable.7 This theorem is interesting because we know in advance that every effectively decidable set S or relation R of natural numbers is arithmetically definable—i.e., for every effectively decidable set S (or relation R) there is an arithmetical formula that is true of a natural number n (or a sequence of natural numbers n … m) if and only if n is a member of S (or n … m stand in relation R to one another). We also know that some sets of natural numbers are definable in arithmetic even though membership in those sets is not effectively decidable. The theorem tells us that the set of arithmetical truths isn’t one of them.
The theorem uses “Gödel numbering” to assign numbers to expressions of the language of arithmetic, LA. The Gödel number of an expression is its numerical code. Using these codes allows us to treat formulas of LA (which are officially about the natural numbers 0, 1, 2, 3, …) as making claims about LA itself—e.g., claims that certain of its sentences are, or are not, provable. The indefinability theorem states that there is no formula of LA that is true of the set of numbers that code the true sentences of LA. In certain systems of Gödel numbering, the numerical code of a compound expression is the number denoted by the Arabic numeral that results from writing, one after another (in left-to-right order), the Arabic numerals that code the individual sy
mbols that make up the expression. There is a decision procedure for determining the numerical code of any expression of LA, and for determining, given a natural number, the expression, if any, that it codes.
The Gödel-Tarski theorem is an application of the liar and heterologicality paradoxes. We begin by calling a formula with exactly one free variable a predicate.8 We then stipulate that a predicate/formula of a language L is heterological if and only if it is not true of itself. For example, the ordinary English predicate ‘x is a human being’ isn’t true of itself because the sentence The predicate ‘x is a human being’ is a human being isn’t true; thus it is heterological. By contrast, the predicate ‘x is a predicate’ is autological, rather than heterological, because the sentence The predicate ‘x is a predicate’ is a predicate is true. What about the predicate ‘x is heterological’? Whether or not it is a heterological predicate of ordinary English depends on whether or not it is a predicate of ordinary English at all, and hence on whether or not the sentence The predicate ‘x is heterological’ is heterological is a sentence of ordinary English. If it is, then it must either be true or not true. Since, by definition, it is true if and only if it’s not true, it can’t be either one. Thus, we must conclude that ‘x is heterological’ isn’t a predicate of ordinary English. Instead, it is a predicate of a technical extension of ordinary English that we can use to talk about ordinary English. In general, a language can contain a predicate ‘heterological’ defined for languages of which ‘heterological’ isn’t a part, but including it in the range of predicates for which it is defined leads to absurdities.
