Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science, Series Number 43)

The book is, indeed, about "basic proof theory", as claimed. Yet, I was disappointed at it's narrow focus, and was unable to glean much of anything that I didn't already know or suspect. Frankly, reading it is a bit of a slog (I'm about 1/3rd-1/2 way in; I'm taking the proverbial 1/2 hour per page, but the resulting narrative is not very gripping.) I suppose it covers the material it promises to cover; it just didn't meet my hopes & expectations.I'd hoped to improve my understanding; I'd hoped to have something I could wave in the face of students and say "here, read this and be enlightened!" I'd hoped to gain insights into the relationship to grammars, parsing, term rewriting, confluence. Insights into homotopy type theory. A bridge to model theory. Algorithms for generating proofs. Perhaps a more categorical view: lets say, algorithms generating proofs based on monoidal categories and acts. Perhaps some early peaks at non-classical logics, such as linear logic, which famously has the no-cloning/no-erasing theorems that alter how proofs can be written. Perhaps insights into ultrafilters and the like. I was hoping to find some insight that perhaps could be applied to proofs in probabilistic logics. Perhaps all of my dreams and hopes were far beyond the narrow boundaries of what is to be considered to be "proof theory" in modern mathematical academia. In which case, my bad. Still, in actual day-to-day practice of actually creating software systems that can actually generate proofs -- offdah, this book offered no insights. Again, perhaps I'm on the wrong foot, here, but if you, like me, are coming at this from the computer science perspective, there is nothing to be gleaned here.

This is a very bread-and-butter introduction to proof theory. Apart from digressions, it is not until we are five-sixths of the way through the book that we begin to meet formal systems in which any actual mathematics can be formalized (chapter 10). The first nine chapters are devoted to studying, in great detail, a plethora of purely logical systems. Anyone who thought, under the influence of Hilbert, perhaps, that proof theory was about proving the consistency of classical mathematics will probably be seriously disappointed with this book.This is the main flaw in the book. Computer scientists (of whom I am not one) might like it; but beginners looking for an explanation of the relevance of proof theory to either mathematics or philosophy will probably not find what they are looking for, at least through the first five-sixths of the book.Why is proof theory interesting? I could be missing something, but I just do not see that the authors have anything much to say about this question - rather a serious fault in an introductory textbook, surely? The book is very clear and the style is pleasant; but a great many hairs are split and a beginner cannot be expected to see that there is anything much to be gained from doing so.Despite these faults, for readers who *already* possess a moderately advanced knowledge of proof theory and want a really thorough, in-depth treatment of the very basics of the subject, this book is very useful. A thing I particularly liked is the emphasis given to considerations about the lengths of proofs (sections 5.1 and 6.7). Some textbooks on proof theory either do not treat pure logic at all (Pohlers) or do treat it but without giving any information about what cut-elimination in pure logic does to the length of a proof (Schuette). The latter strategy is perverse. Considerations about lengths of proofs are undeniably important when the proofs in question are infinitely long; yet students of the subject should be allowed to see that the considerations that apply here are just generalizations of the same considerations as they apply to finitely long proofs. You will understand the advanced stuff better if you know the basics as well.People doing research in proof theory might also welcome the fact that the authors discuss quite a wide variety of logical systems, thus giving the reader a chance to weigh up the merits and disadvantages of each.Anyone wanting a first introduction to proof theory will probably find the one by Pohlers a lot more exciting than this one. Of the older books, the one by Girard is the one that bears the closest resemblance to this book: in fact, this book covers much of the same ground as the earlier chapters of Girard's, but is easier to follow. On the other hand, because Girard goes much further into the subject, he allows you better to see the relevance of the basics to the more advanced material.

Ottimo Handbook introduttivo in teoria della dimostrazione. Estremamente completo per chi desidera cominciare a studiare la materia. Negli ultimi capitoli vengono anche toccati problemi più particolari (calcoli per le logiche modali, embedding,...)