[The other "MidWest Book Review" seems to miss the main point of the book and doesn't do justice to it.]
This book is not original research, but is still a great book because it opened my eyes to some very important maths about logic that I've overlooked. As the title says, it's about truth and proof. It surprised me that the "strength" of proof systems is somehow related to transfinite numbers.
Chapter 1: Aleph_0 is the cardinality of the integers. 2^Aleph_0 is the cardinality of the continuum (ie, the real line). By Cantor's diagonal argument we know there is no 1-1 correspondence between the integers and the reals.
Chapter 2: Cantor's theory of infinite ordinals. We can count from 1,2,3,... to infinity, and BEYOND that, is the first transfinite ordinal, that Cantor denotes as omega. Then we can carry on counting with omega + 1, omega + 2, omega +3, ..., to omega * 2. This process goes on to omega * 3, omega * 4, ..., and to omega^2, omega^3, ..., omega^omega, omega^omega^omega, ..., and eventually to omega raised to omega an infinite number of times, but it still doesn't end. The next ordinal is epsilon_0, and these countable ordinals go "inconceivably far beyond" epsilon_0. This results in Aleph_1, the first UNCOUNTABLE ordinal, and it still doesn't end!
The continuum hypothesis asks whether 2^Aleph_0 = Aleph_1. It is still unsolved, but Cohen believes that it is highly unlikely to be true. Godel proved that CH is consistent with standard Zermelo-Frankel set theory. Cohen (the inventor of "forcing") proved that it cannot be proved in ZF.
All this is explained very clearly in the book; my summary is lousy. John Stillwell's writing style is very engaging, he knows the subject thoroughly and is able to explain every detail with exceptional clarity.
Chapter 3: About Emil Post's efforts to search for a formulation of all formal systems. He saw that unprovability is a simple consequence of the diagonal argument; this predated Godel's incompleteness theorems, but he didn't publish because the Church-Turing thesis was not yet established at that time (so he wasn't sure if his normal form is universal; Later it turned out to be, of course, Turing-equivalent).
Chapter 4: An introduction to logic and deduction, via Gentzen's sequent calculus. I mainly skimmed this chapter. Cut elimination is introduced here.
Chapter 5: This chapter is very crucial. It starts with the Peano axioms for arithmetic (PA). We can assign a countable ordinal to each vertex of the proof tree. Thus, a proof system's "strength" can be measured by what kind of induction it allows. Gentzen 1943 proved that induction up to any ordinal less than epsilon_0 can be proved in PA. However, there exists "real" theorems whose proof lies beyond epsilon_0 induction. Some examples are given next...
Chapter 6: "Natural Unprovable Theorems". Eg: the Paris-Harrington theorem in Ramsey theory and the Tao-Green theorem in number theory.
Chapter 7: About "Axioms of Infinity" that can be added to ZF so it can deal with infinities. [I haven't read this chapter yet, maybe later. Hope this review helps you so far!]