Tautology Elimination, Cut Elimination, and S5

• Authors: Indrzejczak Andrzej
• Languages of publication: EN

Abstracts

EN

Tautology elimination rule was successfully applied in automated deduction and recently considered in the framework of sequent calculi where it is provably equivalent to cut rule. In this paper we focus on the advantages of proving admissibility of tautology elimination rule instead of cut for sequent calculi. It seems that one may find simpler proofs of admissibility for tautology elimination than for cut admissibility. Moreover, one may prove its admissibility for some calculi where constructive proofs of cut admissibility fail. As an illustration we present a cut-free sequent calculus for S5 based on tableau system of Fitting and prove admissibility of tautology elimination rule for it.

Keywords

EN

sequent calculus; tautology elimination; cut elimination; modal logic S5

• Publisher: Uniwersytet Mikołaja Kopernika (Nicolaus Copernicus University in Toruń)
• Journal: Logic and Logical Philosophy
• Year: 2017
• Volume: 26
• Issue: 4
• Pages: 461–471

Dates

published

2017-12-15

Contributors

author

Indrzejczak Andrzej

• Department of Logic, University of Łódź, Lindleya 3/5, 90–131 Łódź, Poland

References

• Brighton, J., “Cut elimination for GLS using the terminability of its regress process”, Journal of Philosophical Logic 5, 2 (2016): 147–153. DOI: 10.1007/s10992-015-9368-4
• Bednarska, K., and A. Indrzejczak, “Hypersequent calculi for S5: The methods of cut elimination”, Logic and Logical Philosophy 24, 3 (2015): 277–311. DOI: 10.12775/LLP.2015.018
• Davis, M., and H. Putnam, “A computing procedure for quantification theory”, Journal of the Assoc. Comput. Mach. 7, 3 (1960): 201–215. DOI: 10.1145/321033.321034
• Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Reidel, Dordrecht 1983. DOI: 10.1007/978-94-017-2794-5
• Fitting, M., “Simple propositional S5 tableau system”, Annals of Pure and Applied Logic 96, 1–3 (1999): 101–115. DOI: 10.1016/S0168-0072(98)00034-7
• Gallier, J.H., Logic for Computer Science, Harper and Row, New York 1986.
• Gao, F., and G. Tourlakis, “A short and readable proof of cut elimination for two first-order modal logics”, Bulletin of the Section of Logic 44, 3–4 (2015): 131–148. DOI: 10.18778/0138-0680.44.3.4.03
• Indrzejczak, A., “Simple decision procedure for S5 in standard cut-free sequent calculus”, Bulletin of the Section of Logic 45, 2 (2016): 125–140. DOI: 10.18778/0138-0680.45.2.05
• Lyaletski, A.V., “A note on the cut rule”, in Abstracts of the International Conference “Maltsev Meeting”, vol. 137, Novosibirsk 2011.
• Negri, S., and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge 2001. DOI: 10.1017/CBO9780511527340
• Ohnishi, M., K. Matsumoto, “Gentzen method in modal calculi I”, Osaka Mathematical Journal 9 (1957): 113–130.

Identifiers

DOI

10.12775/LLP.2017.005