Rule-Generation Theorem and its Applications

• Autorzy: Andrzej Indrzejczak
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

sequent calculus; cut elimination; proof theory; extralogical rules

• Wydawca: Wydawnictwo Uniwersytetu Łódzkiego
• Czasopismo: Bulletin of the Section of Logic
• Rocznik: 2018
• Tom: 47
• Numer: 4

Daty

wydano

2018-12-30

Twórcy

autor

Andrzej Indrzejczak

• University of Łódź, Department of Logic

Bibliografia

• K. Bimbo, Proof Theory, CRC Press 2015.
• T. Braüner, Hybrid Logic and its Proof-Theory, Roskilde 2009.
• S. R. Buss, An Introduction to Proof Theory [in:] S. Buss (ed.) Handbook of Proof Theory, Elsevier 1998.
• 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.
• 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.
• A. Ciabattoni and R. Ramanayake, Structural extensions of display calculi: a general recipe, WoLLIC 2013, LNCS pp. 81–95, Springer 2013.
• H. B. Curry, Foundations of Mathematical Logic, McGraw-Hill, New York 1963.
• M. Fitting, Proof Methods for Modal and Intuitionistic Logics , Reidel, Dordrecht 1983.
• G. Gentzen, Untersuchungen über das Logische Schlieẞen, Mathematische Zeitschrift 39 (1934), pp. 176–210 and pp. 405–431.
• 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.
• A. Indrzejczak, Natural Deduction, Hybrid Systems and Modal Logics, Springer 2010.
• A. Indrzejczak, Sequent Calculi in Classical Logic [in Polish], Lodz University Publications 2013.
• A. Indrzejczak, Eliminability of Cut in Hypersequent Calculi for some Modal Logics of Linear Frames, Information Processing Letters 115/2 (2015), pp. 75–81.
• A. Indrzejczak, Simple Cut Elimination Proof for Hybrid Logic, Logic and Logical Philosophy 25/2 (2016), pp. 129–141.
• 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.
• A. Indrzejczak, Fregean Description Theory in Proof-Theoretical Setting, Logic and Logical Philosophy, Vol. 28, No 1 (2019), pp. 137–155.
• 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.
• M. Kracht, Power and weakness of the modal display calculus, [in:] H. Wansing (ed.) Proof Theory of Modal Logic, pp. 93–121, Kluwer 1996.
• H. Kurokawa, Hypersequent Calculi for Modal Logics Extending S4, [in:] New Frontiers in Artificial Intelligence, pp. 51–68, Springer 2014.
• B. Lellmann, Axioms vs hypersequent rules with context restrictions, [in:] Proceedings of IJCAR , pp. 307–321, Springer 2014.
• B. Lellmann, Hypersequent rules with restricted contexts for propositional modal logics, Theoretical Computer Science, Vol. 656, part A (2016), pp. 76–105.
• 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.
• M. Manzano, Model Theory, Oxford University Press, Oxford 1999.
• G. Metcalfe, N. Olivetti and D. Gabbay, Proof Theory for Fuzzy Logics, Springer 2008.
• 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.
• S. Negri and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge 2001.
• S. Negri and J. von Plato, Proof Analysis, Cambridge University Press, Cambridge 2011.
• M. Ohnishi and K. Matsumoto, Gentzen Method in Modal Calculi I, Osaka Mathematical Journal 9 (1957), pp. 113–130.
• F. Paoli, Substructural Logics: A Primer, Kluwer, Dordrecht 2002.
• F. Poggiolesi, Gentzen Calculi for Modal Propositional Logic, Springer 2011.
• 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.
• G. Takeuti, Proof Theory, North-Holland, Amsterdam 1987.
• A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Oxford University Press, Oxford 1996.
• H. Wansing, Displaying Modal Logics, Kluwer Academic Publishers, Dordrecht 1999.
• 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.

Identyfikatory

DOI

10.18778/0138-0680.47.4.03