Customer Reviews

Proof Theory

5 star:		(2)
4 star:		(0)
3 star:		(0)
2 star:		(0)
1 star:		(0)

 

 

Takeuti was undoubtedly one of the greatest logicians of the twentieth century and this book is indispensable reading for anyone who wishes fully to appreciate his contributions. The first three chapters are also quite a good introduction to proof theory in general. On the whole, although the second and third chapters do contain a fair number of theorems first proved by Takeuti himself, the book can pretty much be divided into two halves: the first three chapters present standard results of proof theory while the fourth, fifth and sixth are devoted almost entirely to Takeuti's own work.

The first chapter introduces Gentzen's sequent calculi LJ and LK and proves Gentzen's cut-elimination theorem as well as completeness theorems for both LJ and LK.

The centrepiece of the second chapter is Gentzen's second (1938) proof of the eliminability of essential cuts from a derivation of the empty sequent in PA. Takeuti's presentation of the proof is very helpful and makes some things clearer than Gentzen's own presentation. This proof also constitutes the starting point for Takeuti's own cut-elimination proofs. On the other hand, Takeuti omits the helpful heuristic discussion which accompanies Gentzen's presentation of the proof, so someone wishing to get to know the proof really well would do best to read both Gentzen's and Takeuti's versions. In any case, a thorough knowledge of this proof is essential before you go on to the higher-level stuff.

The third chapter is good as an introduction to general second-order logic and simple type theory, culminating in the proof of cut-eliminability via completeness for simple type theory, which was produced by Takahashi and Prawitz simultaneously, in the late 1960's.

I skipped the very long fourth chapter, so cannot really comment on its contents. The purpose of the chapter is, by considering infinitary logic, to enable familiar theorems of model theory to be re-stated as theorems of proof theory.

With the fifth chapter, we come to the material which Takeuti is mainly famous for: the cut-elimination proof for the Pi-1-1 sub-systems of second order logic and arithmetic. It is notoriously difficult to see the strategic thinking behind this proof and for this reason Takeuti's methods never caught on much outside Japan.

The difficulty of perceiving the ideas behind these proofs is not helped by the absence from the book of almost any heuristic discussion. I would, in fact, not advise anyone wanting to understand this proof to begin with the present book. There is a sequence of articles by Takeuti called "On the Fundamental Conjecture of GLC" numbered I through to VI, which appeared mainly in the Journal of the Mathematical Society of Japan in the 1950's and it is very helpful to read these articles in chronological order as, in doing so, you see Takeuti gradually extending his techniques so as to deal with stronger and stronger calculi.

There are a number of articles by other authors which are also helpful here. Firstly, Toshiyasu Arai in his article in a volume entitled "Sets and Proofs" (Cambridge University Press; 1999) has presented a simplified version of the ideas behind "On the Fundamental Conjecture of GLC I" and shown how the substitution rule, which plays a crucial (but not easy to understand) role in Takeuti's later cut-elimination proofs, grew out of these ideas. Arai sketches a proof of the consistency of the system BI using the well-ordering of the system O(2,1) of ordinal diagrams. He presents the same proof more fully, and generalizes it, in "A Sub-System of Classical Analysis Proper to Takeuti's Reduction Method".

Finite trees are quasi-well-ordered by embeddability relation and, as Takeuti's ordinal diagrams look like labelled finite trees in which this quasi-ordering is extended to a total one, it is plausible to conjecture that a careful study of trees will throw light on ordinal diagrams. The articles by Smorynski and Simpson in "Harvey Friedman's Research on the Foundations of Mathematics" are good introductions to trees. Jervell's article "How to Well Order Finite Trees", available on his web page, explicitly relates finite trees to ordinal diagrams. An interesting feature of the second edition of Takeuti's book (p.344f.) is that he exploits the close relationship between ordinal diagrams and labelled finite trees to show that the well-ordering of the system O(n,1) of ordinal diagrams, for every natural number n, follows from Friedman's extension of Kruskal's theorem; this yields a very neat proof of the independence of the said theorem from Pi-1-1 analysis.

Despite the above aids, I cannot say that I myself have fully succeeded in understanding Takeuti's ideas, but that is no reason to give up hope.

Non-Japanese authors discussing Takeuti's work almost invariably complain about the "imperspicuity" of his proofs. They are certainly complicated, but this may be compensated by the fact that he proves metamathematical results about provability in sub-systems of second-order logic and arithmetic by considering these systems directly, rather than by proving their equivalence to other theories, which then get embedded in others, which finally get analysed directly. Suppose you have a sub-system of the second-order sequent calculus, not too strong of course, and want to know how much transfinite induction is needed in order to prove the eliminability of the cuts. Takeuti tells you. European logicians like Pohlers, Buchholz and Rathjen do not seem to discuss such questions explicitly, at any rate, though I may be missing something due to not being sufficiently familiar with their work.

In the second edition, a great deal of material has been added about applications of proof theory to other areas of logic and even to areas of maths outside of logic. In the light of all this, you have to conclude that only sheer ignorance can motivate people to complain (as they do) that proof theory is a subject with no applications.

If anyone wishes to get in touch with any comments about this review, my real name is given above.

I found this book at a used-book fair and for only $3, I struck gold. This book, although a bit old and the fact that it deals with very difficult topics, is not bad to read. Many other books leave you in the dust from page one, but Takeuti's Proof Theory isn't one of them. The pace is good and pretty much everything explained clearly. But this doesn't mean you can just look at it and understand, it's tough content, but made as accessible as I've ever seen it.