So I'm back from Scotland. From my experience, the public transit is pretty bad there. The good thing is, this gave me plenty of time to read Richard Kaye's recent book, The Mathematics of Logic (Cambridge University Press 2007). It's fun to read it. Below is the first draft of a review. All comments and suggestions are welcome.----------------------------------------------
Kaye’s book is devoted to a topic discussed in many existing textbooks: the Completeness theorems for classical logics. Nevertheless, it is far from a standard presentation of a few basic notions and proofs of a bunch of classical results in metalogic. Instead of giving such a presentation, Kaye focuses on extracting interesting mathematical content of Completeness Theorems and showing some of their more sophisticated applications.
*
To give the reader a sample of mathematically interesting aspects of metalogical results, Kaye starts his book with introducing the notion of a tree, explains and proves König’s Lemma, which says that every infinite binary tree contains an infinite path. (Possibly binary) trees often arise quite naturally in certain proof-theoretic considerations, and they serve as a good example of the distinction between “definition from perfect information” (or semantics) and “definition from imprerfect information” (or proof theory). König’s lemma is logically interesting, because it connects the notion of a tree being infinite defined from perfect information (its containing inifinitely many nodes) with the notion of a tree being infinite defined from imperfect information (its containing an infinite path). In a sense, the Completeness Theorem for first-order logic constitutes a generalization of König’s lemma.
Kaye then moves on to extending the lemma to infinite trees whose vertices have finite valency and to certain applications of the lemma.
- It is used in a proof of the claim that that X=[0,1] is sequentially compact (every sequence of its elements has a subsequence converging to some element in X).
- It helps to prove that every infinite planary graph can be colored if and only if every finite subgraph of this planary graph can be colored (which, together with Appel’s and Haken’s theorem that every finite planar graph is 4-colorable, implies that every infitite planar graph can be 4-colored).
- Most interestingly, Kaye briefly discusses an application of König’s lemma in computability theory. For any non-deterministic computation, if we take a computation tree of all its possible computations, and we know that independently of any specific choices in the computation, it will eventually halt (=every path of the computation tree is finite), it follows by König’s lemma that the whole computation tree is finite, which means that this non-deterministic computation can be simulated in a finite time by a deterministic one.
The first chapter also discusses the role of this lemma in the proofs, introducing the idea of reverse mathematics.
*
The second chapter introduces the notion of a poset, some basic notions related to posets and countability, and explains how trees can be viewed as posets (say you take a binary tree to be a set of finite sequences of 0s and 1s closed under taking initial segments, then the relation of being an initial segment is a partial order). It also contains a very clear discussion of one of the key lemmas used in the book: Zorn’s lemma. Take a poset (a set with a transitive and irreflexive relation <) X. It has the Zorn property if for every chain Y in X (a linearly ordered subset of X), Y has an upper bound in X (an x in X, not necessarily in Y, such that for any y in Y, either y precedes x or y=x) First, Kaye analyzes the proof that every countable poset X with the Zorn property has a maximal element (an x such that for no y in X, x strictly precedes y) without using the Axiom of Choice (for any set of non-empty sets there is a function that picks an object from each of those non-empty sets). Second, he proves the full Zorn’s lemma (every poset with Zorn property has a maximal element) using the Axiom of Choice and shows how the proof in the other direction can be given (that the Axiom of Choice can be proven using Zorn’s lemma). Zorn’s lemma is then used to prove yet another generalization of König’s lemma: any infinite finitely branching tree has an infinite path.
*
Chapter three contains an explanation of what a formal system is, from a tree-theoretic perspective. Start with the set of all finite sequences of 0s and 1s. It is a binary tree, call it 2*. Consider now a game that starts with a subset S of 2* and uses the following rules:
- [Given strings rule] You may write down any string s from S.
- [Lengthening rule] Once a string has been written down, you can also write down one or both of the strings s0 or s1.
- [Shortening rule] For any string s, once you have written down s0 and s1, then you may write down s.
The objective of the game is to obtain another string t in 2*. Now, the question is: can we obtain t from S (in a finite number of steps) that way? If yes, a list of strings that can be written down in the game, each of which is written according to one of the rules such that the last string is t may be called a formal proof or derivation of t from S.
Using this slightly unusual example of a formal system, Kaye introduces a few useful notions (e.g. consistency, computability, and partial computability of Post-style formal systems) and produces a few examples of proof-theoretic facts about this system. Next, he introduces the notion of semantics. He contrasts derivability of t from S in his system with t being a semantic consequence of S, defined by:
- For any infinite path p in the tree 2*, if p passes through t, then p passes through an element of S.
Proving that these two notions coincide gives us first Soundness and Completeness Theorems (soundness: whatever is derivable from a set is its consequence; completeness: whatever is a consequence of a set is derivable from it). A crucial role in the completeness proof is played by the Zorn’s lemma. For in the proof we assume that t is not derivable from S and show that in such a case t is not a consequence of S. To do that we have to find an infinite path in 2*-S that contains t. This is done by taking the set X of all supersets S’ of S which do not derive t. This set is a poset ordered by the subset relation. It has the Zorn property (because every union of a chain of this poset is its upper bound). By Zorn’s lemma, this means that that X has a maximal element U. The proof ends by showing that 2*-U (i.e. the complement of this maximal element) is a path we’ve been looking for.
*
Chapter four describes a formal proof system for posets. Kaye gives a few fairly detailed examples of proofs in that system, thus getting the reader used to dealing with similar proofs in classical logic. Next, he defines truth in a poset for formulas of the language under discussion, and understands consequence as truth-preservation in all posets. Proofs of Soundness and Completeness theorems for that system are given. The completeness proof is didactically nicely chosen, for it illustrates the idea that to prove completeness it is enough to prove that consistent sets are satisfiable, and yet it doesn’t involve any complicated model construction on the scale needed for completeness proofs for classical logic (most importantly, neither the Axiom of Choice, nor Lindenbaum’s nor Zorn’s lemmas are used). The system is then used as an example of a few proof-theoretic and semantical facts.
Zorn’s lemma is used, however, in this chapter, to prove that any partial order can be linearized. The proof uses also the Completeness Theorem. A comparison to a proof of the same claim without the completeness theorem illustrates the idea that even proofs of what we consider purely mathematical facts can be much simpler if they employ completeness theorems. Kaye then discusses some applications of the ideas introduced in this chapter to the question of orderability of fields and abelian and non-abelian groups.
*
Chapter five discusses Boolean algebras. The author introduces the notions of a lattice, a distributive lattice and a boolean algebra, discussing properties of those structures. The chapter contains also an interesting historical remark. It turns out that Boole himself wasn’t working with boolean algebras. A fairly common opinion is that he rather worked with boolean rings (commutative rings with 1 and for which x2=x for all x in the ring). In fact, however, as Kaye points out, a careful lecture of Boole’s works indicates rather that his algebras were commutative rings with 1 in which there are no additive or multiplicative nilpotent elements.
*
Chapters six and seven contain a presentation of propositional logic in terms of algebraic semantics. First, in chapter six, the class of boolean terms is defined (these are, pretty much, well-formed formulas). A Post-style proof system is described, whose explanation is supported with a selection of examples. Decidability of provability for propositional logic is proved. In chapter seven Kaye defines valuations of boolean terms in boolean algebras, and proves soundness, completeness and compactness of the proof system under discussion with respect to the class of all boolean algebras (these results with respect to binary boolean algebras are corollaries). Quite interesting is additional material contained in chapter seven, where the complexity of the satisfiability problem for propositional logic and the relation between P and NP problems are discussed.
*
Chapter eight is devoted to applications of Soundness and Completeness theorems to algebraic theories of boolean algebras. Kaye defines some additional notions (esp. filters and ideals). He explains how the Soundness Theorem can be expressed in terms of filters of free algebras. He also uses the Completeness Theorem to prove Boolean Prime Ideal Theorem (every proper filter in a boolean algebra can be extended to an ultrafilter). This theorem, subsequently, is used to prove Tychonov’s Theorem (an arbitrary product of compact topological spaces is compact). Another theorem proven in that chapter is Stone Representation Theorem.
*
In chapter nine Kaye describes a (Post-style) proof system for first-order logic. The explanation is clear and concise, enriched with a nice selection of examples. Somewhat briefly, semantics for first-order languages is introduced and Soundness Theorem is proved.
In fact, Kaye does something slightly surprising. He proves the Soundness Theorem by giving a three-liner:
“Formally, the proof is by induction on the (finite) length of the derivation. We simply need to inspect each proof role to check that it preserves the property… [that if a set proves a formula, the set also semantically entails this formula].” (p. 134)
“I am not going ot prove the Soundness Theorem in any more detail here. A full proof would involve a more formal definition of what it really means for an L-sentence […] to be true in an L-structure […] This can be done […] but is unenlightening for the beginner and only becomes really useful in much advanced work. Instead, I shall appear to the reader’s common sense and mathematical experience that the rules just given look like they should be correct and are in fact particular proof rules that he/she is accustomed to using anyway.” (p. 134)
However trivial the Soundness Theorem for first-order logic may be, one might think, a book that’s all about soundness and completeness and their applications might contain a more detailed treatment of the proof. Also, it seems slightly awkward that Kaye on one hand assumes that the reader is a beginner who wouldn’t profit from inspecting the proof in more detail, and, on the other hand, relies on the reader’s common sense and mathematical experience in deciding that the soundness theorem can be seen to be obviously true (come to think of it, this isn’t a real contradiction, though).
Kaye also explains in this chapter how second-order logic is different from first-order logic and points out that it’s devoid of a complete proof system. He does seem to be quite dismissive about categoricity and the role played by second-order logic in obtaining it, saying that:
“The real problem comes when one tries to put right the most conspicuous omission in the account of second-order logic: the lack of any system for proof. There is no such system, and in fact it is a consequence of Gödel’s famous theorem on the incompleteness of arithmetic that there cannot be such a second-order system for natural numbers that is any better than simply writing down all the true sentences and using them as a set of axioms. (This is not what we want: we want a way of discovering new true statements!)” (p. 138)
This treatment, however, is understandable, given that the book is about mathematical applications of the Completeness Theorems, which does not apply to second-order logic.
*
Chapter ten contains proofs of Completeness and Compactness Theorems. The proof uses Henkinisation. We start by introducing a constant for each open formula with one free variable. This gives us the first Henkinisation of the language. Then we iterate the process, thus obtaining the complete Henkinisation of our language. Now, take any consistent set of the original language and extend it with all the Henkin axioms (which say that if anything satisfies an open formula with one free variable, so does the object denoted by the Henkin constant for that formula). This set will also be consistent. Then, Zorn’s lemma gives us the existence of a maximal consistent set of formulas containing our original set together with Henkin axioms. We now need to show that this consistent set is satisfiable. This is done by taking the model to consist of the set of closed terms of the Henkinised language factored out by the equivalence relation between terms s and t such that s=t belongs to our maximal consistent set. Reference of terms, predicates and functions in the model mirrors their behavior in the maximal consistent set under consideration. By induction we prove that this model models a formula iff this formula belongs to the maximal consistent set under consideration. This gives us the claim that every consistent set is satisfiable. By contraposition and trivial facts about semantical consequence and provability we get completeness.
The Compactness Theorem is a fairly simple consequence of Soundess and Completeness theorems: if every finite subset of a set of formulas is satisfiable, every finite subset of that set is consistent. But this means that the whole set is also consistent (if it weren’t, a proof of the contradiction would employ only a finite number fo premises, and all those would belong to a finite subset of that set). By Completeness, this means that the whole set is also satisfiable.
The first mathematical example of an application of the Completeness Theorem for first-order logic is a proof of the fact that cyclic groups aren’t first-order definable (i.e that there is no set of first-order sentences true for precisely the cyclic groups).
Another interesting application of the Compactness Theorem is discussed in relation to topology. We can consider the set of all theories of all models as a topological space. For each sentence of a language consider an open set of those theories which contain that sentence. Compactness Theorem comes handy when we want to prove that this topological space is compact: if a collection of its open subsets covers it, there is a finite subcollection of this collection that covers the same topological space.
Yet another interesting example in topology is the Omitting Types Theorem. First, the Compactness Theorem is used to prove Baire’s Theorem about Hausdorff topological spaces, and then Baire’s Theorem is used to prove the Omitting Types Theorem.
*
In Chapter 11 Kaye develops some model-theoretic notions and proves a few handy model-theoretic facts. He introduces the notion of countability and proves a few standard claims about it. Then he turns to languages with countable alphabets. He proves that there are countably many finite strings over such alphabets and that the complete Henkinisation of such language also will be countable. This gives a countable version of the Completeness Theorem: every consistent set of sentences of a countable first-order language has a countable model.
Next, Kaye introduces the notion of a cardinal number and explains a few basic facts of cardinal arithmetic. He proves in general that for any first-order language with an infinite alphabet the cardinality of the set of finite strings over that alphablet is equal to the cardinality of the alphabet (this applies to uncountable languages as well). Similarly: the cardinality of the complete Henkinisation of a language equals to the cardinality of that language. This gives us a completeness theorem for arbitrary cardinalities: for any consistent set of first-order sentences of a language of a certain cardinality there is a model that models this set of cardinality at most equal to the cardinality of that language. Another useful theorem is that any consistent set of sentences of a first-order language is such that if that language is of an infinite cardinality, the set has models for each of the cardinalities equal or greater to the cardinality of that language (the last two theorems, in a sense, provide us with a variant of the Löwenheim-Skolem Theorem). The author discusses negation-completeness and categoricity and proves that every set of formulas that’s k-kategorical for some infinite cardinal k is such that, if it has no finite models, it is negation-complete. An application of this result is an argument for the negation-completeness of an axiom system for F-vector spaces over a field F. Another interesting proof is that of Morley’s theorem: any set of sentences that has no finite models and is k-categorical for some cardinality k greater than the cardinality of that language is l-categorical for any cardinal l greater than the cardinality of the language.
Among the applications of these developments we find the fact that the theory of dense linear orders is aleph-zero categorical and hence negation-complete. Another examples are: Schröder-Bernstein Theorem (Tarski’s proof that uses Fixed Point Lemma is used).
Chapter twelve is concerned with non-standard analysis. The basic idea is that the Completeness and Compactness Theorems can be used (as discovered by Robinson) in a construction of the hyperreal number line and in relating reals and hyperreals.
*
The author’s intention is to present “the material usually treated in a first course in logic, but in a way that should appeal to a suspicious mathematician wanting to see some genuine mathematical applications” without the “off-putting and didactically unneccessary logical precision insisted on by some of the authors of the standard undergraduate textbooks.” (p. vii) In this task he succeeds. General understanding of how the Completeness Theorem works and why it holds can be achieved without getting into those ``off-putting’’ details – indeed, if a university course is intended to discuss applications of the Completeness Theorem, it cannot devote the whole semester to proving it.
There are some trade-offs resulting from selecting such a task. Even the less-advanced sections of the book require a more mathematically sophisticated reader than usual presentations of the same material in standard logic textbooks. Kaye assumes that the reader is used to proofs by induction, and that they are ready to go into more set theory than is usually needed for the proofs of metalogical facts. The latter can be seen from the fact that throughout the book he uses Zorn’s lemma, even though in completeness proofs it is usually sufficient to take (a variant of) Lindenbaum’s lemma. This decision has its pros and cons. On one hand, the reader has to have a more general understanding of posets and related notions. On the other hand, this gives some unity to a wide selection of proofs: instead of proving variants of Lindenbaum’s lemma for each of the systems, one just takes Zorn’s lemma and proves that certain chains have the Zorn property. In other words, I wouldn’t recommend this book as a first logic textbook, but this is hardly an objection.
The author does a good job explaining the completeness theorems and indicating their mathematically interesting application (although, one wonders why Kaye didn’t bring up non-standard models of Peano Arithmetic in this context). Chapters are divided into basic and more advanced sections. Even though some parts of the book are not really directed to a philosophically-minded reader, most of the material presented, even in the advanced sections (perhaps excluding some applications of the Completeness Theorem and chapter 12) is a must for any philosopher who wants to work with philosophy of logic or philosophy of mathematics.
Comments