Abstract
An explicit concatenation rule (EC) is proposed, obtained by generalizations and formalization of one of the most intuitive principle of abstract reasoning, which governs the composition of abstract derivations from the left and from the right at the same time, via the mediation of control clauses that occur in the position of the major premise. The sets of control clauses necessary to express various different calculi of natural deduction—standard natural deduction, natural deduction with general elimination rules, “bioriented” natural deduction and their variants—are considered, with a specific focus on a control clause for co-identity, a cut-like inference expressing the principle of linear substitution and on the effect of its addition to these calculi.
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.
Collections \(\Gamma,\Delta \) are always considered to be multisets, that is, the multiplicity of formula occurrences is always accounted for, but not the order of those occurrences.
- 2.
About natural deduction, we refer to Prawitz (1965) explication of how to obtain deduction rules from inference rules by considering them as rules operating on pairs \(\langle \Gamma,A\rangle\).
- 3.
It is for this reason that inference rules have to be taken to a different level of abstraction when talking about abstract derivations. Otherwise, the fundamental fact that cut is a rule of one calculus but not of the other could not be represented.
- 4.
Historically, the inference rule “syllogism”, introduced by Paul Hertz in 1923, is the first formulation of multicut, see Hertz (1923). Apart from an additional side effect that contracts multiple occurrences of formulae in the antecedents of the major premise and the conclusion, it looks exactly as the rule that is presented here. Thus, multicut precedes the formulation of the cut rule. In fact, Gentzen introduced the cut rule in Gentzen (1932) and demonstrated how syllogism can be decomposed into a sequence of cuts. Moreover, see also Paul Bernays’ definition of “Syllogismus” in Bernays (1965).
- 5.
An attempt of defining a most general rule of “composition” is already to be found in Gentzen (1936), where a chain rule is defined that, together with a specific set of basic logical sequents, allows one to reproduce almost all of the inference rules of the original system of natural deduction (in sequent style). See also the forthcoming Moriconi (2014).
- 6.
We are indebted to Peter Schroeder-Heister for suggesting this extremely succinct and elegant notation.
- 7.
Such a notion is indeed present in the refutationistic calculus defined in Tranchini (2010).
- 8.
Note that the Kleene star is not a logical symbol, but results from the omission of multiset parentheses for antecedent and succedent and also for effects. Indeed, if those were not omitted, \(\langle A^{{\ast}}\vert B\rangle\) would have to be written \(\langle \{A\}^{{\ast}}\vert \{B\}\rangle\).
- 9.
With “bioriented” natural deduction, we shall here refer to the calculus of bidirectional natural deduction proposed by Peter Schroeder-Heister in Schroeder-Heister (2009). The calculus of natural deduction with general elimination rules, instead, was first defined as such by Jan von Plato in von Plato (2001).
- 10.
A dual phenomenon could be observed on the left-hand side, provided the fulfillment of the condition that antecedents of abstract derivations never be empty, but this obviously does not hold in any of the control bases defined in the present work.
- 11.
Without going into details of a formal definition, we chose to give the inferences a leftmost, topmost order.
References
Arndt, Michael and Laura Tesconi. 2014. The role of cut as a principle of explicit composition. In Second Pisa Colloquium in Logic, Language and Epistemology, ed. E. Moriconi and L. Tesconi. ETS.
Bernays, Paul. 1965. Betrachtungen zum Sequenzen-Kalkul. In Contributions to logic and methodology in honor of J.M. Bochenski, ed. A.-T. Tymieniecka. Amsterdam: North-Holland.
Gentzen, Gerhard. 1932. Über die Existenz unhabängiger Axiomensysteme zu unendlichen Satzsysteme. Mathematische Annalen 107:329–350.
Gentzen, Gerhard. 1936. Die Widerspruchsfreiheit der reine Zahlentheorie. Mathematische Annalen 112:493–565.
Hertz, Paul. 1923. Über Axiomensysteme für beliebige Satzsysteme. II. Sätze höheren Grades. Mathematische Annalen 89:76–102.
Moriconi, Enrico. 2014, In preparation. Early structural reasoning. Gentzen 1932.
Prawitz, Dag. 1965. Natural deduction. A proof-theoretic study. Stockholm: Almqvist & Wiksell.
Schroeder-Heister, Peter. 2009. Sequent calculi and bidirectional natural deduction: On the proper basis of proof-theoretic semantics. In The Logica Yearbook 2008, ed. M. Peliš. London: College Publications.
Tranchini, Luca. 2010. Refutation: a proof-theoretic account. In First Pisa Colloquium in Logic, Language and Epistemology, ed. C. Marletti. Pisa: ETS.
von Plato, Jan. 2001. Natural deduction with general elimination rules. Archive for Mathematical Logic 40:541–567.
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
Arndt, M., Tesconi, L. (2015). A Cut-Like Inference in a Framework of Explicit Composition for Various Calculi of Natural Deduction. In: Lolli, G., Panza, M., Venturi, G. (eds) From Logic to Practice. Boston Studies in the Philosophy and History of Science, vol 308. Springer, Cham. https://doi.org/10.1007/978-3-319-10434-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-10434-8_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10433-1
Online ISBN: 978-3-319-10434-8
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)