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.
I thank audiences at the Universities of Tübingen and St. Andrews for comments on some of the material presented here.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Strictly, the negation rule in play is weaker than reductio ad absurdum. It’s the weak principle which, added to positive logic, yields what Allen Hazen calls subminimal logic: from \(\lnot \psi \) and a proof of \(\psi \) with \(\phi \) as assumption, infer \(\lnot \phi \) and discharge the assumption \(\phi \) (Hazen 1995).
- 2.
The restriction to one or two premisses is clearly inessential. What is surprising, though, is the lack of mention of subformulae possibly occurring as assumptions discharged in the application of the rule. As this characterisation stands, it would seem to preclude Gentzen’s rule for \(\supset \)-introduction (conditional proof). Prawitz gives a much more general form at (Prawitz 1978, p. 35) which corrects this oversight.
- 3.
On the last, cf. Zucker and Tragesser (1978).
- 4.
- 5.
Francez and Dyckhoff (2012, Sect. 3.1) give the same formulation as ‘another formulation of the idea behind the inversion-principle’. In her (2002, pp. 571–572), Negri says, ‘Whatever follows from the grounds for deriving a formula must follow from that formula’. I thank Jan von Plato (personal communication) for bringing (Negri 2002) to my attention.
- 6.
In his (2010), Read doesn’t discuss \(\supset \) explicitly but we can extrapolate from his discussion of negation and the general case. The derivation here is exactly in accord with how he arrives at the standard general elimination rule.
- 7.
Read (2010) emphasises the role of structural rules in proving the equivalence of different forms of elimination rules.
- 8.
If \(\curlywedge \) isn’t a logical constant then, strictly speaking, Gentzen’s rules for negation are not impure in the sense of Dummett (1991, p. 257), for then only one logical constant figures in them.
- 9.
One may reasonably object that the standard \(\vee \)-elimination rule does not provide the minimal conditions that have \(\phi \vee \psi \) allow for its own introduction; the restricted \(\vee \)-introduction rule of quantum logic also does that. But the pursuit of minimality is not an end in itself and since the standard rule allows for the levelling of local peaks, (i) we have no proof-theoretic motivation to restrict the elimination rule and (ii) the standard rule accords with the use of proof by cases in mathematics (and elsewhere).
- 10.
This is how Gentzen puts the restriction. He does not say, as we would nowadays expect, that \(a\) does not occur in any assumption on which \(\phi (a)\) depends.
- 11.
I do not claim that this is the most general form possible. It is, I suggest, the most straightforward general form matching Prawitz’s characterisation and consonant with the refashioning employed in general elimination rules.
- 12.
- 13.
Negri (2002, pp. 573, 574) has the single elimination rule for the multiplicative conjunction of linear logic and the pair of elimination rules for the additive conjunction.
- 14.
The term ‘general introduction rule’ has been used already by Negri and von Plato. My general introduction rules are similar in form but not identical to those of Negri and von Plato’s (2001, p. 217) natural deduction system NG for intuitionist propositional logic, and again similar in style but not identical to the rules of Negri (2002). For example, Negri and von Plato adopt what I call immediately below an inessential reformulation of Gentzen’s \(\supset \)-introduction rule, a rule which does not comply with my conception of general introduction rules.
- 15.
- 16.
Merging is a special case of the operation on rules called splicing in Milne (Milne 2012).
- 17.
The rules here are obtained by the splicing technique when \(\looparrowright (\phi ,\psi ,\chi )\) is identified either with \( (\phi \supset \psi ) ~ \& ~ (\lnot \phi \supset \chi )\) or with \( (\phi ~ \& ~ \psi ) \vee (\lnot \phi ~ \& ~ \chi )\) — see Milne (2012). Compare the rules given here for ‘if ...then ...else ...’ with those in Francez and Dyckhoff (2012) which mention negation explicitly.
- 18.
The procedure here and in the previous section is close to the two procedures outlined in Kurbis (2008), but Kurbis’s method for deriving elimination from introduction rule applies only to constants with a single introduction rule and, likewise, his method for deriving introduction rules from elimination rule applies only to constants with a single elimination rule.
Negri (2002, pp. 571, 575) uses a ‘dual inversion principle’ to obtain her general introduction rules from general elimination rules. The dual inversion principle states, ‘Whatever follows from a formula follows from the sufficient grounds for deriving the formula’. Cf. (Negri (2001), p. 217).
- 19.
- 20.
Cf. Schroeder-Heister (2004, pp. 36–37)
- 21.
Strictly, because he is being very careful regarding structural rules, Read has two occurrences of \(\bullet \) “above the line” in the elimination rule.
- 22.
In fact, it is Heinrich Wansing’s *tonk (Wansing 2006, p. 657). Read takes \(\bullet \) to show that (ge-)harmony does not entail consistency, let alone conservativeness—see (Read 2000, pp. 141–142, Read 2010, pp. 570–573); Schroeder-Heister (2004, p. 37) takes it to show failure of cut/transitivity of deduction (thus preserving consistency).
- 23.
- 24.
They are the rules obtained via the classically valid equivalence of \(\forall x \phi \) and \(\lnot \exists x\lnot \phi \) from the rules for negation and the existential quantifier by splicing (Milne 2012).
- 25.
That we obtain a sequent calculus with only elimination rules from a direct transcription of our system of natural deduction rules is in marked contrast with the standard case (on which see Prawitz 1971, p. 243).
- 26.
Ruy de Queiroz (2008) decries the verificationist tendency in proof-theoretic semantics and seeks to oppose it by finding in Wittgenstein early and late a focus on the consequences of assertions, thus playing up the significance of elimination rules.
- 27.
Pavel Tichý maintained that, despite what Gentzen said, natural deduction only makes sense when viewed in the same way as sequent calculus: as a calculus of logically true statements concerning entailments (Tichy 1988, Chap. 13).
- 28.
The manipulation of general introduction and general elimination rules by splicing shows that the Gentzen and Quine approaches are more closely related than may first appear (Milne 2012, Sect. 6).
References
Belnap, N., Jr. (1962). Tonk, plonk and plink. Analysis, 22, 130–134 (Reprinted in Philosophical Logic by P. F. Strawson (ed.) (1967). Oxford University Press, Oxford, 132–137).
Dummett, M. A. E. (2000). Elements of intuitionism (2nd ed.). Oxford: Oxford University Press (1st ed. 1977).
Dummett, M. A. E. (1991). The logical basis of metaphysics. London: Duckworth.
Dyckhoff, R. (2009). Generalised elimination rules and harmony, talk given at St Andrews. Retrieved May 26, 2009, http://www.cs.st-andrews.ac.uk/rd/talks/2009/GE.pdf
Francez, N., & Dyckhoff, R. (2012). A note on harmony. Journal of Philosophical Logic, 41, 613–628.
Gentzen, G. (1934–1935). Untersuchungen über das logische schließen. Mathematische Zeitschrift, 39, 176–210, 405–431. (English translation by Manfred Szabo as ‘Investigations into Logical Deduction’, American Philosophical Quarterly, 1, 1964, 288–306, 2, 1965, 204–218, also in Szabo, M.E. (ed.) (1969). The Collected Papers of Gerhard Gentzen (pp. 68–131). North-Holland, Amsterdam).
Gentzen, G. (1936). Die Widerspruchfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112, 493–565. (English translation by Manfred Szabo as The Consistency of Elementary Number Theory in Szabo, M. E. (ed.) (1969). The Collected Papers of Gerhard Gentzen (pp. 132–201). North-Holland, Amsterdam).
Hazen, A. (1995). Is even minimal negation constructive? Analysis, 55, 105–107.
Heyting, A. (1930). Die formalen Regeln der intuitionistischen logik und mathematik. In P. Mancosu (ed.). Sitzungsberichte der Preußischen Akademie der Wissenschaften, Physikalisch-mathematische Klasse (pp. 42–65). (English translation, (1998) ‘The formal rules of intuitionist logic’, In P. Mancosu (ed.). From Brouwer to Hilbert: the debate in the foundations of mathematics in the 1920s (pp. 311–328). Oxford: Oxford University Press).
Kurbis, N. (2008). Stable harmony. In M. Peliš (Ed.), The logica yearbook 2007 (pp. 87–96). Institue of Philosophy, Czech Academy of Sciences, Prague: Filosofia.
von Kutschera, F. (1968). Die vollständigkeit des operatorensystems \(\lbrace \) \(\lnot \), \(\wedge \), \(\vee \), \(\rightarrow \) \(\rbrace \) für die intuitionistische aussagenlogik im rahmen der gentzensemantik. Archiv für Math Logik Grundlagenforschung, 11, 3–16.
Lemmon, E. (1965). A further note on natural deduction. Mind, 74, 594–597.
Milne, P. (2007). Existence, freedom, identity, and the logic of abstractionist realism. Mind, 116, 23–53.
Milne, P. (2008). A formulation of first-order classical logic in natural deduction with the subformula property. In M. Peliš (Ed.), The logica yearbook 2007 (pp. 97–110). Institue of Philosophy, Czech Academy of Sciences, Prague: Filosofia.
Milne, P. (2010). Subformula and separation properties in natural deduction via small Kripke models. Review of Symbolic Logic, 3, 175–227.
Milne, P. (2012). Inferring, splicing, and the Stoic analysis of argument. In O. T. Hjortland & C. Dutilh Novaes (Ed.), Insolubles and consequences: Essays in honour of Stephen Read (pp. 135–154). College Publications: London.
Mondadori, M. (1988). On the notion of classical proof. In C. Cellucci & G. Sambin (Eds.), Atti del congresso temi e prospettive della logica e della filosofial della scienza contemporanee, Cesana 7–10 gennaio 1987 (Vol. 1, pp. 211–214). Bologna: Cooperativa Libraria Universitaria Editrice Bologna.
Moriconi, E., & Tesconi, L. (2008). On inversion principles. History and Philosophy of Logic, 29, 103–113.
Negri, S., & von Plato, J. (2001). Structural proof theory. Cambridge: Cambridge University Press (with an appendix by Arne Ranta).
Negri, S. (2002). Varieties of linear calculi. Jounral of Philosophical Logic, 31, 569–590.
von Plato, J. (2001). Natural deduction with general elimination rules. Archive for Mathematical Logic, 40, 541–567.
von Plato, J. (2008). Gentzen’s proof of normalization for natural deduction. Bulletin of Symbolic Logic, 14, 240–257.
Prawitz, D. (1965). Natural deduction: A proof-theoretical study. Stockholm: Almqvist & Wiksell (reprinted with new preface, Mineola, NY: Dover Publications, 2006).
Prawitz, D. (1971). Ideas and results in proof theory. In J. E. Fenstad (Ed.), Proceedings of the Second Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics (Vol. 63). Amsterdam: North-Holland.
Prawitz, D. (1978). Proofs and the meaning and completeness of the logical constants. In J. Hintikka, I. Niiniluoto, & E. Saarinen (Eds.), Essays on Mathematical and Philosophical Logic: Proceedings of the Fourth Scandinavian Logic Symposium and of the First Soviet-Finnish Logic Conference, Jyväskylä, Finland, June 29-July 6, 1976, Synthese Library (Vol. 122, pp. 25–40). Dordrecht: Reidel.
Prawitz, D. (1967). A note on existential instantiation. Journal of Symbolic Logic, 32, 81–82.
Prawitz, D. (2006). Meaning approached via proofs. Synthese, 148, 507–524.
de Queiroz, R. J. (2008). On reduction rules, meaning-as-use, and proof-theoretic semantics. Studia Logica, 90, 211–247.
Read, S. (2000). Harmony and autonomy in classical logic. Journal of Philosophical Logic, 29, 123–154.
Read, S. (2004). Identity and harmony. Analysis, 64, 113–119.
Read, S. (2010). General-elimination harmony and the meaning of the logical constants. Journal of Philosophical Logic, 39, 557–576.
Sandqvist, T. (2012). The subformula property in natural deduction established constructively. Review of Symbolic Logic, 5, 710–719.
Schroeder-Heister, P. (1984). A natural extension of natural deduction. Journal of Symbolic Logic, 49, 1284–1300.
Schroeder-Heister, P. (1984). Generalized rules for quantifiers and the completeness of the intuitionistic operators & \(\vee \), \(\rightarrow \), \(\curlywedge \), \(\forall \), \(\exists \). In M. Richter., E. Börger., W. Oberschelp., B. Schinzel., W. Thomas (Eds.), Computation and Proof Theory. Proceedings of the Logic Colloquium held in Aachen, July 18–23, 1983, Part II, Lecture Notes in Mathematics (pp. 399–426, vol 1104). Berlin, Heidelberg, New York, Tokyo: Springer.
Schroeder-Heister, P. (2004). On the notion of assumption in logical systems. In: R. Bluhm & C. Nimtz (Eds.). Selected Papers Contributed to the Sections of GAP5, Fifth International Congress of the Society for Analytical Philosophy (pp. 27–48), Bielefeld. Paderborn: Mentis Verlag. Retrieved 22–26 Sept 2003, from http://www.gap5.de/proceedings/.
Schroeder-Heister, P. (2014). Generalized elimination inferences, higher-level rules, and the implications-as-rules interpretation of the sequent calculus. In L. C. Pereira, & E. H. Haeusler, & V. de Paiva (Eds.), Advances in natural deduction: A Celebration of Dag Prawitz’s Work (pp. 1–29). Dordrecht, Heidelberg, New York, London.
Suppes, P. (1957). Introduction to logic. New York: Van Nostrand Rienhold.
Tennant, N. (1978). Natural logic (1st ed.). Edinburgh: Edinburgh University Press (Reprinted in paperback with corrections, 1991).
Tennant, N. (1992). Autologic. Edinburgh: Edinburgh University Press.
Tichý, P. (1988). The foundations of Frege’s logic. Berlin, New York: Walter de Gruyter.
Wansing, H. (2006). Connectives stranger than tonk. Journal of Philosophical Logic, 35, 653–660.
Zucker, J. I., & Tragesser, R. S. (1978). The adequacy problem for inferential logic. Journal of Philosophical Logic, 7, 501–516.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Milne, P. (2015). Inversion Principles and Introduction Rules. In: Wansing, H. (eds) Dag Prawitz on Proofs and Meaning. Outstanding Contributions to Logic, vol 7. Springer, Cham. https://doi.org/10.1007/978-3-319-11041-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-11041-7_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11040-0
Online ISBN: 978-3-319-11041-7
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)