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.
CITATION STYLE
Milne, P. (2015). Inversion Principles and Introduction Rules. In Outstanding Contributions to Logic (Vol. 7, pp. 189–224). Springer. https://doi.org/10.1007/978-3-319-11041-7_8
Mendeley helps you to discover research relevant for your work.