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
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. y precedes x or y=x) [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.
For any infinite path p in the tree 2*, if p passes through t, then p passes through an element of S.
“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)
“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)