Book Chapter
Details
Citation
Milne P (2015) Inversion principles and introduction rules. In: Wansing H (ed.) Dag Prawitz on Proofs and Meaning. first ed. Outstanding Contributions to Logic, 7. Cham, Heidelberg, New York, Dordrecht, London: Springer, pp. 189-224. http://www.springer.com/us/book/9783319110400
Abstract
Following Gentzen’s practice, borrowed from intuitionist logic, Prawitz takes the introduction rule(s) for a connective to show how to prove a formula with the connective dominant. He proposes an inversion principle to make more exact Gentzen’s talk of deriving elimination rules from introduction rules. Here I look at some recent work pairing Gentzen’s introduction rules with general elimination rules. After outlining a way to derive Gentzen’s own elimination rules from his introduction rules, I give a very different account of introduction rules in order to pair them with general elimination rules in such a way that elimination rules can be read off introduction rules, introduction rules can be read off elimination rules, and both sets of rules can be read off classical truth-tables. Extending to include quantifiers, we obtain a formulation of classical first-order logic with the subformula property.
Keywords
Introduction rules; Elimination rules; General elimination rules; Inversion principle; Sequent calculus
Status | Published |
---|---|
Title of series | Outstanding Contributions to Logic |
Number in series | 7 |
Publication date | 31/12/2015 |
URL | http://hdl.handle.net/1893/22016 |
Publisher | Springer |
Publisher URL | http://www.springer.com/us/book/9783319110400 |
Place of publication | Cham, Heidelberg, New York, Dordrecht, London |
ISSN of series | 2211-2758 |
ISBN | 978-3-319-11040-0 |
People (1)
Emeritus Professor, Philosophy