This chapter is entirely devoted to the proof of the compactness theorem. Section 13.1 outlines the proof, which reduces to establishing two main lemmas. These are then taken up in sections 13.2 through 13.4 to complete the proof, from which the Löwenheim—Skolem theorem also emerges as a corollary. The optional section 13.5 discusses what happens if nonenumerable languages are admitted: compactness still holds, but the Löwenheim—Skolem theorem in its usual ‘downward’ form fails, while an alternative ‘upward’ theorem holds.

In the preceding several chapters we have introduced the intuitive notion of effective computability, and studied three rigorously defined technical notions of computability: Turing computability, abacus computability, and recursive computability, noting along the way that any function that is computable in any of these technical senses is computable in the intuitive sense. We have also proved that all recursive functions are abacus computable and that all abacus-computable functions are Turing computable. In this chapter we close the circle by showing that all Turing-computable functions are recursive, so that all three notions of computability are equivalent. It immediately follows that Turing's thesis, claiming that all effectively computable functions are Turing computable, is equivalent to Church's thesis, claiming that all effectively computable functions are recursive. The equivalence of these two theses, originally advanced independently of each other, does not amount to a rigorous proof of either, but is surely important evidence in favor of both. The proof of the recursiveness of Turing-computable functions occupies section 8.1. Some consequences of the proof of equivalence of the three notions of computability are pointed out in section 8.2, the most important being the existence of a universal Turing machine, a Turing machine capable of simulating the behavior of any other Turing machine desired. The optional section 8.3 rounds out the theory of computability by collecting basic facts about recursively enumerable sets, sets of natural numbers that can be enumerated by a recursive function. Perhaps the most basic fact about them is that they coincide with the semirecursive sets introduced in the preceding chapter, and hence, if Church's (or equivalently, Turing's) thesis is correct, coincide with the (positively) effectively semidecidable sets.

In this chapter we begin to bring together our work on logic from the past few chapters with our work on computability from earlier chapters (specifically, our work on recursive functions from Chapters 6 and 7). In section 15.1 we show how we can ‘talk about’ such syntactic notions as those of sentence and deduction in terms of recursive functions, and draw among others the conclusion that, once code numbers are assigned to sentences in a reasonable way, the set of valid sentences is semirecursive. Some proofs are deferred to sections 15.2 and 15.3. The proofs consist entirely of showing that certain effectively computable functions are recursive. Thus what is being done in the two sections mentioned is to present still more evidence, beyond that accumulated in earlier chapters, in favor of Church's thesis that all effectively computable functions are recursive. Readers who feel they have seen enough evidence for Church's thesis for the moment may regard these sections as optional.

Showing that a function is Turing computable directly, by giving a table or flow chart for a Turing machine computing the function, is rather laborious, and in the preceding chapters we did not get beyond showing that addition and multiplication and a few other functions are Turing computable. In this chapter we provide a less direct way of showing functions to be Turing computable. In section 5.1 we introduce an ostensibly more flexible kind of idealized machine, an abacus machine, or simply an abacus. In section 5.2 we show that despite the ostensible greater flexibility of these machines, in fact anything that can be computed on an abacus can be computed on a Turing machine. In section 5.3 we use the flexibility of these machines to show that a large class of functions, including not only addition and multiplication, but exponentiation and many other functions, are computable on a abacus. In the next chapter functions of this class will be called recursive, so what will have been proved by the end of this chapter is that all recursive functions are Turing computable.

According to Gödel's second incompleteness theorem, the sentence expressing that a theory likePis consistent is undecidable byP, supposingPis consistent. The full proof of this result is beyond the scope of a book on the level of the present one, but the overall structure of the proof and main ingredients that go into the proof will be indicated in this short chapter. In place of problems there are some historical notes at the end.

Ramsey's theorem is a combinatorial result about finite sets with a proof that has interesting logical features. To prove this result about finite sets, we are first going to prove, in section 26.1, an analogous result about infinite sets, and are then going to derive, in section 26.2, the finite result from the infinite result. The derivation will be an application of the compactness theorem. Nothing in the proof of Ramsey's theorem to be presented requires familiarity with logic beyond the statement of the compactness theorem, but at the end of the chapter we indicate how Ramsey theory provides an example of a sentence undecidable in P that is more natural mathematically than any we have encountered so far.

This chapter connects our work on computability with questions of logic. Section 11.1 presupposes familiarity with the notions of logic from Chapter 9 and 10 and of Turing computability from Chapters 3–4, including the fact that the halting problem is not solvable by any Turing machine, and describes an effective procedure for producing, given any Turing machine M and input n, a set of sentences Γ and a sentence D such that M given input n will eventually halt if and only if Γ implies D. It follows that if there were an effective procedure for deciding when a finite set of sentences implies another sentence, then the halting problem would be solvable; whereas, by Turing's thesis, the latter problem is not solvable, since it is not solvable by a Turing machine. The upshot is, one gets an argument, based on Turing's thesis for (the Turing—Büchi proof of) Church's theorem, that the decision problem for implication is not effectively solvable. Section 11.2 presents a similar argument—the Gödel-style proof of Church's theorem—this time using not Turing machines and Turing's thesis, but primitive recursive and recursive functions and Church's thesis, as in Chapters 6–7. The constructions of the two sections, which are independent of each other, are both instructive; but an entirely different proof, not dependent on Turing's or Church's thesis, will be given in a later chapter, and in that sense the present chapter is optional. (After the present chapter we return to pure logic for the space of several chapters, to resume to the application of computability theory to logic with Chapter 15.)

This chapter and the next contain a summary of material, mainly definitions, needed for later chapters, of a kind that can be found expounded more fully and at a more relaxed pace in introductory-level logic textbooks. Section 9.1 gives an overview of the two groups of notions from logical theory that will be of most concern: notions pertaining to formulas and sentences, and notions pertaining to truth under an interpretation. The former group of notions, called syntactic, will be further studied in section 9.2, and the latter group, called semantic, in the next chapter.

A function is effectively computable if there are definite, explicit rules by following which one could in principle compute its value for any given arguments. This notion will be further explained below, but even after further explanation it remains an intuitive notion. In this chapter we pursue the analysis of computability by introducing a rigorously defined notion of a Turing-computable function. It will be obvious from the definition that Turing-computable functions are effectively computable. The hypothesis that, conversely, every effectively computable function is Turing computable is known as Turing's thesis. This thesis is not obvious, nor can it be rigorously proved (since the notion of effective computability is an intuitive and not a rigorously defined one), but an enormous amount of evidence has been accumulated for it. A small part of that evidence will be presented in this chapter, with more in chapters to come. We first introduce the notion of Turing machine, give examples, and then present the official definition of what it is for a function to be computable by a Turing machine, or Turing computable.

We have given in earlier chapters several different proofs of Church's theorem to the effect that first-order logic is undecidable: there is no effective procedure that applied to any first-order sentence will in a finite amount of time tell us whether or not it is valid. This negative result leaves room on the one hand for contrasting positive results, and on the other hand for sharper negative results. The most striking of the former is the Löwenheim—Behmann theorem, to the effect that the logic of monadic (one-place) predicates is decidable, even when the two-place logical predicate of identity is admitted. The most striking of the latter is the Church—Herbrand theorem that the logic of a single dyadic (two-place) predicate is undecidable. These theorems are presented in sections 21.2 and 21.3 after some general discussion of solvable and unsolvable cases of the decision problem for logic in section 21.1. While the proof of Church's theorem requires the use of considerable computability theory (the theory of recursive functions, or of Turing machines), that is not so for the proof of the Löwenheim—Behmann theorem or for the proof that Church's theorem implies the Church—Herbrand theorem. The former uses only material developed by Chapter 11. The latter uses also the elimination of function symbols and identity from section 19.4, but nothing more than this. The proofs of these two results, positive and negative, are independent of each other.

Introductory textbooks in logic devote much space to developing one or another kind of proof procedure, enabling one to recognize that a sentence D is implied by a set of sentences Γ, with different textbooks favoring different procedures. In this chapter we introduce the kind of proof procedure, called a Gentzen system or sequent calculus, that is used in more advanced work, where in contrast to introductory textbooks the emphasis is on general theoretical results about the existence of proofs, rather than practice in constructing specific proofs. The details of any particular procedure, ours included, are less important than some features shared by all procedures, notably the features that whenever there is a proof of D from Γ, D is a consequence of Γ, and conversely, whenever D is a consequence of Γ, there is a proof of D from Γ. These features are called soundness and completeness, respectively. (Another feature is that definite, explicit rules can be given for determining in any given case whether a purported proof or deduction really is one or not; but we defer detailed consideration of this feature to the next chapter.) Section 14.1 introduces our version or variant of sequent calculus. Section 14.2 presents proofs of soundness and completeness. The former is easy; the latter is not so easy, but all the hard work for it has been done in the previous chapter. Section 14.3, which is optional, comments briefly on the relationship of our formal notion to other such formal notions, as might be found in introductory textbooks or elsewhere, and of any formal notion to the unformalized notion of a deduction of a conclusion from a set of premisses, or proof a theorem from a set of axioms.

Suppose that, in addition to allowing quantifications over the elements of a domain, as in ordinary first-order logic, we allow also quantification over relations and functions on the domain. The result is called second-order logic. Almost all the major theorems we have established for first-order logic fail spectacularly for second-order logic, as is shown in the present short chapter. This chapter and those to follow generally presuppose the material in section 17.1. (They are also generally independent of each other, and the results of the present chapter will not be presupposed by later ones.)

Modal logic extends ‘classical’ logic by adding new logical operators □ and ⋄ for ‘necessity’ and ‘possibility’. Section 27.1 is an exposition of the rudiments of (sentential) modal logic. Section 27.2 indicates how a particular system of modal logic GL is related to the kinds of questions about provability in P we considered in Chapters 17 and 18. This connection motivates the closer examination of GL then undertaken in section 27.3.

The intuitive notion of an effectively computable function is the notion of a function for which there are definite, explicit rules, following which one could in principle compute its value for any given arguments. This chapter studies an extensive class of effectively computable functions, the recursively computable, or simply recursive, functions. According to Church's thesis, these are in fact all the effectively computable functions. Evidence for Church's thesis will be developed in this chapter by accumulating examples of effectively computable functions that turn out to be recursive. The subclass of primitive recursive functions is introduced in section 6.1, and the full class of recursive functions in section 6.2. The next chapter contains further examples. The discussion of recursive computability in this chapter and the next is entirely independent of the discussion of Turing and abacus computability in the preceding three chapters, but in the chapter after next the three notions of computability will be proved equivalent to each other.