Natural Deduction: A Proof-Theoretical StudyAn 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. |
Other editions - View all
Common terms and phrases
2ND ORDER LOGIC A-rule application assumption discharged axioms c-rule calculi of sequents Chapter classical logic clause consequence consider contains Corollary corresponding deduction rule defined definition discharge-function E-rule edition elimination rule end-formula end-segment essentially modal existential instantiation Fitch formula occurrence formula-tree Gentzen Gentzen-type system Gentzen's system Hauptsatz hence holds I-part I-rule inference rules interpolation formula introduction rule intuitionistic and minimal intuitionistic logic inversion principle languages logical constants major premiss mathematical maximum formula maximum segment minimal logic minor modal logic modal with respect mula n-place predicate natural deduction negation normal deduction notation positive negative predicate logic predicate parameter predicate variables principal sign proof proper inference rules proper parameter provable proved pseudo-formula pure parameters quantifier quasi-deduction ramified replacing restriction result second order logic sentential connective sentential logic strictly positive subformula succedent systems of natural theorem on normal theory thread tion top-formula