Rule-Generation Theorem and its Applications

Andrzej Indrzejczak

doi:10.18778/0138-0680.47.4.03

Authors

Andrzej Indrzejczak University of Łódź, Department of Logic

DOI:

https://doi.org/10.18778/0138-0680.47.4.03

Keywords:

sequent calculus, cut elimination, proof theory, extralogical rules

Abstract

In several applications of sequent calculi going beyond pure logic, an introduction of suitably defined rules seems to be more profitable than addition of extra axiomatic sequents. A program of formalization of mathematical theories via rules of special sort was developed successfully by Negri and von Plato. In this paper a general theorem on possible ways of transforming axiomatic sequents into rules in sequent calculi is proved. We discuss its possible applications and provide some case studies for illustration.

References

K. Bimbo, Proof Theory, CRC Press 2015.
Google Scholar

T. Braüner, Hybrid Logic and its Proof-Theory, Roskilde 2009.
Google Scholar

S. R. Buss, An Introduction to Proof Theory [in:] S. Buss (ed.) Handbook of Proof Theory, Elsevier 1998.
Google Scholar

A. Ciabattoni, N. Galatos and K. Terui, From axioms to analytic rules in nonclassical logics, [in:] LICS (2002), pp. 229–240, IEEE Computer Society, 2008.
Google Scholar

A. Ciabattoni, G. Metcalfe and F. Montagna, Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions, Fuzzy Sets and Systems 161(3) (2010), pp. 369–389.
Google Scholar

A. Ciabattoni and R. Ramanayake, Structural extensions of display calculi: a general recipe, WoLLIC 2013, LNCS pp. 81–95, Springer 2013.
Google Scholar

H. B. Curry, Foundations of Mathematical Logic, McGraw-Hill, New York 1963.
Google Scholar

M. Fitting, Proof Methods for Modal and Intuitionistic Logics , Reidel, Dordrecht 1983.
Google Scholar

G. Gentzen, Untersuchungen über das Logische Schlieẞen, Mathematische Zeitschrift 39 (1934), pp. 176–210 and pp. 405–431.
Google Scholar

G. Gentzen, Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie, Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, New Series 4, Leipzig, pp. 19–44, 1938.
Google Scholar

A. Indrzejczak, Natural Deduction, Hybrid Systems and Modal Logics, Springer 2010.
Google Scholar

A. Indrzejczak, Sequent Calculi in Classical Logic [in Polish], Lodz University Publications 2013.
Google Scholar

A. Indrzejczak, Eliminability of Cut in Hypersequent Calculi for some Modal Logics of Linear Frames, Information Processing Letters 115/2 (2015), pp. 75–81.
Google Scholar

A. Indrzejczak, Simple Cut Elimination Proof for Hybrid Logic, Logic and Logical Philosophy 25/2 (2016), pp. 129–141.
Google Scholar

A. Indrzejczak, Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus, Bulletin of the Section of Logic 45(2) (2016), pp. 95–102.
Google Scholar

A. Indrzejczak, Fregean Description Theory in Proof-Theoretical Setting, Logic and Logical Philosophy, Vol. 28, No 1 (2019), pp. 137–155.
Google Scholar

A. Indrzejczak, Cut-Free Modal Theory of Definite Descriptions, [in:] G. Bezhanishvili et al. (eds.) Advances in Modal Logic 12, pp. 387–406, College Publications 2018.
Google Scholar

M. Kracht, Power and weakness of the modal display calculus, [in:] H. Wansing (ed.) Proof Theory of Modal Logic, pp. 93–121, Kluwer 1996.
Google Scholar

H. Kurokawa, Hypersequent Calculi for Modal Logics Extending S4, [in:] New Frontiers in Artificial Intelligence, pp. 51–68, Springer 2014.
Google Scholar

B. Lellmann, Axioms vs hypersequent rules with context restrictions, [in:] Proceedings of IJCAR , pp. 307–321, Springer 2014.
Google Scholar

B. Lellmann, Hypersequent rules with restricted contexts for propositional modal logics, Theoretical Computer Science, Vol. 656, part A (2016), pp. 76–105.
Google Scholar

B. Lellmann and D. Pattinson, Correspondence between modal Hilbert axioms and sequent rules with an application to S5, [in:] TABLEAUX 2013, pp. 219–233, Springer 2013.
Google Scholar

M. Manzano, Model Theory, Oxford University Press, Oxford 1999.
Google Scholar

G. Metcalfe, N. Olivetti and D. Gabbay, Proof Theory for Fuzzy Logics, Springer 2008.
Google Scholar

T. Nagashima, An extension of the Craig-Schütte interpolation theorem, Annals of the Japan Association for the Philosophy of Science 3 (1966), pp. 12–18.
Google Scholar

S. Negri and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge 2001.
Google Scholar

S. Negri and J. von Plato, Proof Analysis, Cambridge University Press, Cambridge 2011.
Google Scholar

M. Ohnishi and K. Matsumoto, Gentzen Method in Modal Calculi I, Osaka Mathematical Journal 9 (1957), pp. 113–130.
Google Scholar

F. Paoli, Substructural Logics: A Primer, Kluwer, Dordrecht 2002.
Google Scholar

F. Poggiolesi, Gentzen Calculi for Modal Propositional Logic, Springer 2011.
Google Scholar

P. Schroeder-Heister, Open Problems in Proof-theoretic Semantics, [in:] T. Piecha, P. Schroeder-Heister (eds.) Advances in Proof-theoretic Semantics, pp. 253–283, Springer 2016.
Google Scholar

G. Takeuti, Proof Theory, North-Holland, Amsterdam 1987.
Google Scholar

A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Oxford University Press, Oxford 1996.
Google Scholar

H. Wansing, Displaying Modal Logics, Kluwer Academic Publishers, Dordrecht 1999.
Google Scholar

H. Wansing, Sequent Systems for Modal Logics, [in:] D. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic, vol. IV, pp. 89–133, Reidel Publishing Company, Dordrecht 2002.
Google Scholar