A Sequent System without Improper Derivations


  • Katsumi Sasaki Nanzan University, Faculty of Science and Technology, 18 Yamazato-Cho, Showa-Ku, Nagoya, 466, Japan




Sequent system, improper derivation, natural deduction


In the natural deduction system for classical propositional logic given by G. Gentzen, there are some inference rules with assumptions discharged by the rule. D. Prawitz calls such inference rules improper, and others proper. Improper inference rules are more complicated and are often harder to understand than the proper ones.

In the present paper, we distinguish between proper and improper derivations by using sequent systems. Specifically, we introduce a sequent system \(\vdash_{\bf Sc}\) for classical propositional logic with only structural rules, and prove that \(\vdash_{\bf Sc}\) does not allow improper derivations in general. For instance, the sequent \(\Rightarrow p \to q\) cannot be derived from the sequent \(p \Rightarrow q\) in \(\vdash_{\bf Sc}\). In order to prove the failure of improper derivations, we modify the usual notion of truth valuation, and using the modified valuation, we prove the completeness of \(\vdash_{\bf Sc}\). We also consider whether an improper derivation can be described generally by using \(\vdash_{\bf Sc}\).


W. Breckenridge, O. Magidor, Arbitrary reference, Philosophical Studies: An International Journal for Philosophy in the Analytic Tradition, vol. 158(3) (2012), pp. 377–400, DOI: https://doi.org/10.1007/s11098-010-9676-z
Google Scholar DOI: https://doi.org/10.1007/s11098-010-9676-z

A. Chagrov, M. Zakharyaschev, Modal logic, Oxford Logic Guides, Oxford University Press, New York (1997).
Google Scholar

K. Fine, Reasoning with arbitrary objects, Aristotelian Society Series, Basil Blackwell, Oxford (1986).
Google Scholar

G. Gentzen, Untersuchungen über das logisch Schließen, Mathematische Zeitschrift, vol. 39 (1934–35), pp. 176–210, 405–431, DOI: https://doi.org/10.1007/BF01201353
Google Scholar DOI: https://doi.org/10.1007/BF01201363

P. Hertz, Über Axiomensysteme für beliebige Satzsysteme, Mathematische Annalen, vol. 101 (1929), pp. 457–514.
Google Scholar DOI: https://doi.org/10.1007/BF01454856

A. Indrzejczak, A Survey of Nonstandard Sequent Calculi, Studia Logica, vol. 102 (2014), pp. 1295–1322, DOI: https://doi.org/10.1007/s11225-014-9567-y
Google Scholar DOI: https://doi.org/10.1007/s11225-014-9567-y

D. Prawitz, Natural Deduction: A Proof-Theoretical Study, Almqvist & Wiksell, Stockholm (1965).
Google Scholar

K. Robering, Ackermann’s Implication for Typefree Logic, Journal of Logic and Computation, vol. 11(1) (2001), pp. 5–23, DOI: https://doi.org/10.1093/logcom/11.1.5
Google Scholar DOI: https://doi.org/10.1093/logcom/11.1.5

P. Schroeder-Heister, Resolution and the Origins of Structural Reasoning: Early Proof-Theoretic Ideas of Hertz and Gentzen, The Bulletin of Symbolic Logic, vol. 8(2) (2002), pp. 246–265, DOI: https://doi.org/10.2178/bsl/1182353872
Google Scholar DOI: https://doi.org/10.2178/bsl/1182353872

R. Suszko, W sprawie logiki bez aksjomatów, Kwartalnik Filozoficzny, vol. 17 (1948), pp. 199–205.
Google Scholar

R. Suszko, Formalna teoria wartości logicznych, Studia Logica, vol. 6 (1957), pp. 145–320, DOI: https://doi.org/10.1007/BF02547932
Google Scholar DOI: https://doi.org/10.1007/BF02547932




How to Cite

Sasaki, K. (2021). A Sequent System without Improper Derivations. Bulletin of the Section of Logic, 51(1), 91–108. https://doi.org/10.18778/0138-0680.2021.21



Research Article