Synopses & Reviews
An innovative approach to the semantics of logic, proof-theoretic semantics seeks the meaning of propositions and logical connectives within a system of inference. Gerhard Gentzen invented proof-theoretic semantics in the early 1930s, and Dag Prawitz, the author of this study, extended its analytic proofs to systems of natural deduction. Prawitz's theories form the basis of intuitionistic type theory, and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics.
The concept of natural deduction follows a truly natural progression, establishing the relationship between a noteworthy systematization and the interpretation of logical signs. As this survey explains, the deduction's principles allow it to proceed in a direct fashion — a manner that permits every natural deduction's transformation into the equivalent of normal form theorem. A basic result in proof theory, the normal form theorem was established by Gentzen for the calculi of sequents. The proof of this result for systems of natural deduction is in many ways simpler and more illuminating than alternative methods. This study offers clear illustrations of the proof and numerous examples of its advantages.
This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.
Prawitz's theories form the basis of intuitionistic type theory, and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics. The proof-theoretical system represents a simpler and more illuminating method than alternative approaches, and this volume offers a succinct, coherent illustration of its applications to natural deduction. 1965 edition.
Table of Contents
1. Natural Deduction of Gentzen-Type
2. The Inversion Principle
3. Normal Deductions in Classical Logic
4. Normal Deductions in Intuitionistic Logic
5. Second Order Logic
6. Modal Logic
7. Some Other Concepts of Implication
Appendix A. The Calculi of Sequents
Appendix B. On a set theory by Fitch
Appendix C. Notes on some other variants of natural deduction
Index of Symbols