This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included.
From reviews:
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.
Author(s): A. S. Troelstra, H. Schwichtenberg
Series: Cambridge Tracts in Theoretical Computer Science 43
Edition: 2nd
Publisher: Cambridge University Press
Year: 2000
Language: English
Pages: 430
City: Cambridge; New York
Cover......Page 1
Title Page......Page 3
Contents......Page 5
Preface (1st edition)......Page 9
Preface (2nd edition)......Page 11
1 Introduction......Page 13
1.1 Preliminaries......Page 14
1.2 Simple type theories......Page 22
1.3 Three types of formalism......Page 34
2.1 Natural deduction systems......Page 47
2.2 Ni as a term calculus......Page 57
2.3 The relation between C, I & M......Page 60
2.4 Hilbert systems......Page 63
2.5 Notes......Page 67
3 Gentzen systems......Page 72
3.1 The Gl- & G2-systems......Page 73
3.2 The Cut rule......Page 78
3.3 Equivalence of G- & N-systems......Page 80
3.4 Systems with local rules......Page 87
3.5 Absorbing the structural rules......Page 89
3.6 The one-sided systems for C......Page 97
3.7 Notes......Page 99
4.1 Cut elimination......Page 104
4.2 Applications of cutfree systems......Page 117
4.3 A more efficient calculus for Ip......Page 124
4.4 Interpolation & definable functions......Page 128
4.5 Extensions of Gl-systems......Page 138
4.6 Extensions of G3-systems......Page 142
4.7 Logic with equality......Page 146
4.8 The theory of apartness......Page 148
4.9 Notes......Page 151
5 Bounds & permutations......Page 159
5.1 Numerical bounds on cut elimination......Page 160
5.2 Size & cut elimination......Page 169
5.3 Permutation of rules for classical logic......Page 176
5.4 Permutability of rules for Gli......Page 183
5.5 Notes......Page 188
6.1 Conversions & normalization......Page 190
6.2 The structure of normal derivations......Page 196
6.3 Normality in G-systems & N-systems......Page 201
6.4 Extensions with simple rules......Page 209
6.5 E-logic & ordinary logic......Page 211
6.6 Conservativity of predicative classes......Page 215
6.7 Conservativity for Horn clauses......Page 217
6.8 Strong normalization for ––>Nm & λ_–›......Page 222
6.9 Hyperexponential bounds......Page 227
6.10 A digression : a stronger conversion......Page 229
6.11 Orevkov's result......Page 231
6.12 Notes......Page 235
7.1 Introduction to resolution......Page 242
7.2 Unification......Page 244
7.3 Linear resolution......Page 248
7.4 From Gentzen system to resolution......Page 255
7.5 Resolution for Ip......Page 258
7.6 Notes......Page 267
8 Categorical logic......Page 270
8.1 Deduction graphs......Page 271
8.2 Lambda terms & combinators......Page 276
8.3 Decidability of equality......Page 283
8.4 A coherence theorem for CCC's......Page 286
8.5 Notes......Page 293
9 Modal & linear logic......Page 295
9.1 The modal logic S4......Page 296
9.2 Embedding intuitionistic logic into S4......Page 300
9.3 Linear logic......Page 304
9.4 A system with privileged formulas......Page 312
9.5 Proofnets......Page 315
9.6 Notes......Page 325
10 Proof theory of arithmetic......Page 329
10.1 Ordinals below ε_0......Page 330
10.2 Provability of initial cases of TI......Page 333
10.3 Normalization with the omega rule......Page 337
10.4 Unprovable initial cases of TI......Page 342
10.5 TI for non-standard orderings......Page 349
10.6 Notes......Page 354
11.1 Intuitionistic second-order logic......Page 357
11.2 Ip^2 & λ2......Page 361
11.3 Strong normalization for Ni^2......Page 363
11.4 Encoding of λ2Ω into λ2......Page 369
11.5 Provably recursive functions of HA^2......Page 370
11.6 Notes......Page 376
Solutions to selected exercises......Page 379
Bibliography......Page 391
Symbols & notations......Page 416
Index......Page 420
Back cover......Page 430
