The Unprovability of Consistency

Gödel’s second incompleteness theorem, roughly stated, is that if Peano Arithmetic is consistent, then it cannot prove its own consistency. The theorem has been generalized and abstracted in various ways and this has led to the notion of a provability predicate, which plays a fundamental role in much modern metamathematical research. To this notion we now turn. A formula P(v1) is called a provability predicate for S if for all sentences X and Y the following three conditions hold: Suppose now P(v1) is a Σ1-formula that expresses the set P of the system P.A. Under the assumption of ω-consistency, P(v1) represents P in P.A. Under the weaker assumption of simple consistency, all that follows is that P(v1) represents some superset of P, but that is enough to imply that if X is provable in P.A., then so is P (x̄).

Rosser Systems

Our first proof of the incompleteness of P.A. was based on the assumption that P.A. is correct. Gödel’s proof of the last chapter was based on the metamathematically weaker assumption that P.A. is ω-consistent. Rosser [1936] subsequently showed that P.A. can be proved incomplete under the still weaker metamathematical assumption that P.A. is simply consistent! Now, Rosser did not show that the Gödel sentence G of the last chapter is undecidable on the weaker assumption of simple consistency. He constructed another sentence (a more elaborate one) which he showed undecidable on the basis of simple consistency. Our first proof of the incompleteness of P.A. boils down to finding a formula that expresses the set P̃* (or alternatively one that expresses R*). Gödel’s proof, which we gave in the last chapter, boils down to representing one of the sets P* and R* in P.A. and the only way known in Gödel’s time of doing this involved the assumption of ω-consistency. [This assumption was not needed to show that the sets P* and R* are enumerable in P.A.—it was in passing from the enumerability of these sets to their representability that ω-consistency stepped in.] Now, Rosser did not achieve incompleteness by representing either of the sets P* and R*, but rather by representing some superset of R* disjoint from P*—this can be done under the weaker assumption of simple consistency—and it also serves to establish incompleteness, as we will see. The axiom schemes Ω4 and Ω5 of the system (R) will play a key role in this and the next chapter. We shall say that a system S is an extension of Ω4 and Ω5 if all formulas of Ω4 and Ω5 are provable in S. We will prove the following theorem and its corollaries. Theorem R. Every simply consistent axiomatizable extension of Ω4 and Ω5 in which all Σ1-sets are enumerable must be incomplete. Corollary 1. Every simply consistent axiomatizable extension of Ω4 and Ω5 in which all true Σ0-sentences are provable must be incomplete. Corollary 2. Every simply consistent axiomatizable extension of the system (R) is incomplete.

Definability and Diagonalization

In this chapter we establish some basic facts about Σ1-relations and functions that will be needed for the rest of this study. We also introduce the notion of fixed-points of formulas and prove a fundamental fact about them which is crucial for Gödel’s second incompleteness theorem and related results of the next chapter. A formula F(v1,...,vn) is said to define a relation R(x1,..., xn) in a system S if for all numbers a1,...,an, the two following conditions hold. (1) R(a1,... ,an) ⇒ F(ā1,... , ā n) is provable in S. (2) R̃(a1,...,an) ⇒ F(ā1,... , ā n) is refutable in S. We say that F(v1,...,vn) completely represents R(x1, . . . ,xn ) in S iff F represents R and ~ F represents the complement R of R in S—in other words, if (1) and (2) above hold with “⇒” replaced by “↔”. If F defines R in S and S is consistent, then F completely represents R in S. Proof. Assume hypothesis. We must show that the converses of (1) and (2) above must hold. Suppose F(ā1,... , ān) is provable in S. Then F(ā1,..., ān) is not refutable in S (by the assumption of consistency). Therefore by (2), R̃ (a1,...,an) cannot hold. Hence R(a1,...,an) holds. Similarly, if F(ā1,..., ān) is refutable, then it is not provable. Hence by (1), R(a1,..., an) cannot hold and hence R̃ (a1,...,an). By a recursive set or relation, we mean one such that it and its complement are both Σ1. [There are many different, but equivalent, definitions in the literature of recursive relations. We will consider some others in the sequel to this volume.] It is obvious that a formula F defines a relation R in S iff F separates R from R̃ in S. Suppose now S is a Rosser system and that R is a recursive relation. Then R and R̃ are both Σ1. Hence R is separable from R̃ in S, which means that R is definable in S. And so we have: 1. If S is a Rosser system, then all recursive relations are definable in S. 2. If S is a consistent Rosser system, then all recursive relations are completely representable in S.

Shepherdson’s Representation Theorems

We have already remarked that at the time of Gödel’s proof, the only known way of showing the set P* of Peano Arithmetic to be representable in P.A. involved the assumption of ω-consistency. Well, in 1960, A. Ehrenfeucht and S. Feferman showed that all Σ1-sets can be represented in all simply consistent axiomatizable extensions of the system (R). Hence, all Σ1-sets can be shown to be representable in P.A. under the weaker assumption that P.A. is simply consistent. Their proof combined a Rosser-type argument with a celebrated result in recursive function theory due to John Myhill which goes beyond the scope of this volume. Very shortly after, however, John Shepherdson [1961] found an extremely ingenious alternative proof that is more direct and which we study in this chapter. [In our sequel to this volume, we compare Shepherdson’s proof with the original one. The comparison is of interest in that the two methods are very different and the proofs generalize in different directions which are apparently incomparable in strength.] We recall that for each n > 1, a system S is called a Rosser system for n-ary relations if for any Σ1-relations R1(x1,..., xn) and R2(X1, ..., xn), the relation R1 — R2 is separable from R2 — R1 in S. We wish to prove the following theorem and its corollary (Th. 1 below). Theorem S1—Shepherdson’s Representation Theorem. If S is a simply consistent axiomatizable Rosser system for binary relations (n-ary relations for n = 2), then all Σ1-sets are representable in S. Theorem 1—Ehrenfeucht, Feferman. All Σ1-sets are representable in every consistent axiomatizable extension of the system (R). Shepherdson’s Lemma and Weak Separation For emphasis, we will now sometimes write “strongly separates” for “separates”. We will say that a formula F(v1) weakly separates A from B in S if F(v1) represents some superset of A disjoint from B, We showed in the last chapter (Lemma 1) that strong separation implies weak separation provided that the system S is consistent. We also say that a formula F(v1,. .. ,vn) weakly separates a relation R I (x1 , . .. ,xn) from .R2(x1,... ,xn) if F(v1, ..., vn) represents some relation R’(x1,. .. ,xn) such that R1 ⊆ R1’ and R1 is disjoint from -R2.

Gödel’s Proof Based on ω-Consistency

The proof that we have just given of the incompleteness of Peano Arithmetic was based on the underlying assumption that Peano Arithmetic is correct—i.e., that every sentence provable in P.A. is a true sentence. Gödel’s original incompleteness proof involved a much weaker assumption—that of ω-consistency to which we now turn. We consider an arbitrary axiom system S whose formulas are those of Peano Arithmetic, whose axioms include all those of Groups I and II (or alternatively, any set of axioms for first-order logic with identity such that all logically valid formulas are provable from them), and whose inference rules are modus ponens and generalization. (It is also possible to axiomatize first-order logic in such a way that modus ponens is the only inference rule—cf. Quine [1940].) In place of the axioms of Groups III and IV, however, we can take a completely arbitrary set of axioms. Such a system S is an example of what is termed a first-order theory, and we will consider several such theories other than Peano Arithmetic. (For the more general notion of a first-order theory, the key difference is that we do not necessarily start with + and × as the undefined function symbols, nor do we necessarily take ≤ as the undefined predicate symbol. Arbitrary function symbols and predicate symbols can be taken, however, as the undefined function and predicate symbols—cf. Tarski [1953] for details. However, the only theories (or “systems”, as we will call them) that we will have occasion to consider are those whose formulas are those of P.A.) S is called simply consistent (or just “consistent” for short) if no sentence is both provable and refutable in S.

Arithmetic Without the Exponential

§1. By an arithmetic term or formula, we mean a term or formula in which the exponential symbol E does not appear, and by an arithmetic relation (or set), we mean a relation (set) expressible by an arithmetic formula. By the axiom system P.A. (Peano Arithmetic), we mean the system P.E. with axiom schemes N10 and N11 deleted, and in the remaining axiom schemes, terms and formulas are understood to be arithmetic terms and formulas. The system P.A. is the more usual object of modern study (indeed, the system P.E. is rarely considered in the literature). We chose to give the incompleteness proof for P.E. first since it is the simpler. In this chapter, we will prove the incompleteness of P.A. and establish several other results that will be needed in later chapters. The incompleteness of P.A. will easily follow from the incompleteness of P.E., once we show that the relation xy = z is not only Arithmetic but arithmetic (definable from plus and times alone). We will first have to show that certain other relations are arithmetic, and as we are at it, we will show stronger results about these relations that will be needed, not for the incompleteness proof of this chapter, but for several chapters that follow—we will sooner or later need to show that certain key relations are not only arithmetic, but belong to a much narrower class of relations, the Σ1-relations, which we will shortly define. These relations are the same as those known as recursively enumerable. Before defining the Σ1-relations, we turn to a still narrower class, the Σ0-relations, that will play a key role in our later development of recursive function theory. §2. We now define the classes of Σ0-formulas and Σ0-relations and then the Σ1-formulas and relations. By an atomic Σ0-formula, we shall mean a formula of one of the four forms c1 + c2 = c3, c1 · c2 =c3, c1 = c2 or c1 ≤ c2, where each of c1, c2 or c3 is either a variable or a numeral (but some may be variables and others numerals).

The Incompleteness of Peano Arithmetic with Exponentiation

We shall now turn to a formal axiom system which we call Peano Arithmetic with Exponentiation and which we abbreviate “P.E.”. We take certain correct formulas which we call axioms and provide two inference rules that enable us to prove new correct formulas from correct formulas already proved. The axioms will be infinite in number, but each axiom will be of one of nineteen easily recognizable forms; these forms are called axiom schemes. It will be convenient to classify these nineteen axiom schemes into four groups (cf. discussion that follows the display of the schemes). The axioms of Groups I and II are the so-called logical axioms and constitute a neat formalization of first-order logic with identity due to Kalish and Montague [1965], which is based on an earlier system due to Tarski [1965]. The axioms of Groups III and IV are the so-called arithmetic axioms. In displaying these axiom schemes, F, G and H are any formulas, vi and vj are any variables, and t is any term. For example, the first scheme L1 means that for any formulas F and G, the formula (F ⊃ (G ⊃ F)) is to be taken as an axiom; axiom scheme L4 means that for any variable Vi and any formulas F and G, the formula . . . (∀vi (F ⊃ G) ⊃ (∀vi (F ⊃ ∀vi G) . . . is to be taken as an axiom.

Self-Referential Systems

Self-Referential Systems This chapter is largely a review of the essential ideas behind the proofs of Gödel, Rosser and Löb—only presented in a more abstract setting. We believe that it will tie up these ideas in a helpful and instructive manner. We shall first present these ideas in the form of logic puzzles (much in the manner of Smtdlyan [1987]). Then we shall state the results more generally in terms of abstract systems that we call provability systems. These are closely related to certain axiom systems of modal logic, which we briefly discuss at the end of the chapter. In the puzzles to which we now turn, belief will play the rôle of provability. Instead of considering a mathematical system and the sentences provable in it, we consider a logician (sometimes call a reasoner) and the propositions believed by the reasoner. Apart from the heuristic value, these “epistemic” incompleteness theorems appear to be of some interest to those working in artificial intelligence. We shall pay a visit to the Island of Knights and Knaves, in which knights make only true statements and knaves make only false ones. Each inhabitant is either a knight or a knave. No inhabitant can claim that he is not a knight (since a knight would never make such a false claim and a knave would never make such a true claim). A logician visits this island one day and meets a native. All we are told about the logician is that he is completely accurate in his beliefs—he never believes anything false. The native then makes a certain statement X. It then follows that the logician can never believe that the native is a knight nor can he ever believe that the native is a knave.

Some General Remarks on Provability and Truth

We have given three different incompleteness proofs of Peano Arithmetic— the first used Tarski’s truth-set, the second (Gödel’s original proof) was based on the assumption of ω-consistency, and the third (Rosser’s proof) was based on the assumption of simple consistency. The three proofs yield different generalizations—namely 1. Every axiomatizable subsystem of N is incomplete. 2. Every axiomatizable ω-consistent system in which all true Σ0-sentences are provable is incomplete. 3. Every axiomatizable simply consistent extension of (R) is incomplete. The first of the three proofs is by far the simplest and we are surprised that it has not appeared in more textbooks. Of course, it can be criticized on the grounds that it is not formalizable in arithmetic (since the truth set is not expressible in arithmetic), but this should be taken with some reservations in light of Askanas’ theorem, which we will discuss a bit later. It is not too surprising that Peano Arithmetic is incomplete because the scheme of mathematical induction does not really express the full force of mathematical induction. The true principle of mathematical induction is that for any set A of natural numbers, if A contains 0 and A is closed under the successor function (such a set A is sometimes called an inductive set), then A contains all natural numbers. Now, there are non-denumerably many sets of natural numbers but only denumerably many formulas in the language LA and, hence, there are only denumerably many expressible sets of LA- Therefore, the formal axiom scheme of induction for P.A. guarantees only that for every expressible set A, if A is inductive, then A contains all natural numbers. To express the principle of mathematical induction fully, we need second order arithmetic in which we take set and relational variables and quantify over sets and relations of natural numbers.

Tarski’s Theorem for Arithmetic

In the last chapter, we dealt with mathematical languages in considerable generality. We shall now turn to some particular mathematical languages. One of our goals is to reach Gödel’s incompleteness theorem for the particular system known as Peano Arithmetic. We shall give several proofs of this important result; the simplest one is based partly on Tarski’s theorem, to which we first turn. The first concrete language that we will study is the language of first order arithmetic based on addition, multiplication and exponentiation. [We also take as primitive the successor function and the less than or equal to relation, but these are inessential.] We shall formulate the language using only a finite alphabet (mainly for purposes of a convenient Gödel numbering); specifically we use the following 13 symbols. . . . 0’ ( ) f, υ ∽ ⊃ ∀ = ≤ # . . . The expressions 0, 0′, 0″, 0‴, · · · are called numerals and will serve as formal names of the respective natural numbers 0, 1, 2, 3, · · ·. The accent symbol (also called the prime) is serving as a name of the successor function. We also need names for the operations of addition, multiplication and exponentiation; we use the expressions f′, f″, f‴ as respective names of these three functions. We abbreviate f′ by the familiar “+”; we abbreviate f’’ by the familiar dot and f‴ by the symbol “E”. The symbols ~ and ⊃ are the familiar symbols from prepositional logic, standing for negation and material implication, respectively. [For any reader not familiar with the use of the horseshoe symbol, for any propositions p and q, the propositions p ⊃ q is intended to mean nothing more nor less than that either p is false, or p and q are both true.] The symbol ∀ is the universal quantifier and means “for all.” We will be quantifying only over natural numbers not over sets or relations on the natural numbers. [Technically, we are working in first-order arithmetic, not second-order arithmetic.] The symbol “=” is used, as usual, to denote the identity relation, and “≤” is used, as usual, to denote the “less than or equal to” relation.