Gentzen's cut-elimination theorem is widely used as a tool for meta-mathematical investigations. It is sometimes claimed however that the theorem and its proof have interest which is independent of these applications and derives from the information they supply about the structure of proofs in general. Ungar investigates this claim in the context of first order logic. Ungar gives an account of Gentzen's theorem for various formalisms and discusses the difficulties involved in treating these different versions uniformly, as instances of a single theorem which is not tied to a particular system of rules. By extending the theorem to a natural deduction calculus whose derivations are allowed to have more than one conclusion, Ungar argues that the different versions of the theorem are more or less natural specializations of a single result whose significance can be understood in terms of the proofs represented by formal derivations. A concluding discussion focuses on the relationship between proofs and formal derivations, and the role proofs may play as part of a general theory of evidence.
Author(s): A. M. Ungar
Series: Center for the Study of Language and Information - CSLI Lecture Notes 28
Edition: 1
Publisher: CSLI Publications
Year: 1992
Language: English
Pages: 236
Normalization, Cut-Elimination, and the Theory of Proofs......Page 3
Copyright......Page 4
Contents......Page 5
Introduction......Page 7
1. Background......Page 17
2. Comparing NJ with LJ......Page 38
3. Natural Deduction Revisited......Page 52
4. The Problem of Substitution......Page 61
5. A Multiple-Conclusion Calculus......Page 83
6. Reduction Procedures......Page 108
7. Correspondence Results......Page 132
8. Interpretations of Derivations......Page 159
Appendix A. A Strong Cut-Elimination Theorem for LJ......Page 192
Appendix B. A Formulation of the Classical Sequent Calculus......Page 206
Appendix C. Proofs and Categories......Page 226
List of Works Cited......Page 235
Index......Page 240
CSLI Publications......Page 243
