CSLI Publications logo
new books
knuth books
for authors
CSLI Publications
>Normalization, Cut-Elimination and the Theory of Proofs cover

Normalization, Cut-Elimination and the Theory of Proofs

A. M. Ungar

Gentzen's cut-elimination theorem is widely used as a tool for mathematical investigations. It is sometimes claimed however that the theorem and its proof have an 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 fro 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 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.

A. M. Ungar teaches philosophy at the State University of New York at Albany.


  • Introduction 1
  • 1 Background 11
  • 2 Comparing NJ with LJ 32
  • 3 Natural Deduction Revisited 46
  • 4 The Problem of Substitution 55
  • 5 A Multiple-Conclusion Calculus 77
  • 6 Reduction Procedures 102
  • 7 Correspondence Results 126
  • 8 Interpretations of Derivations 153
  • Appendices
    • A A Strong Cut-Elimination Theorem for LJ 186
    • B A Formulation of the Classical Sequent Calculus 200
  • Proofs and Categories 220
  • List of Works Cited 229
  • Index 234


ISBN (Paperback): 9780937073827 (0937073822)
ISBN (Cloth): 9780937073834 (0937073830)
Subject: Mathematics; Logic--Proofs

Add to Cart
View Cart

Check Out

Distributed by the
University of
Chicago Press

pubs @ csli.stanford.edu