Rule-Generation Theorem and its Applications

Andrzej Indrzejczak

Bulletin of the Section of Logic (2018)

  • Volume: 47, Issue: 4
  • ISSN: 0138-0680

Abstract

top
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.

How to cite

top

Andrzej Indrzejczak. "Rule-Generation Theorem and its Applications." Bulletin of the Section of Logic 47.4 (2018): null. <http://eudml.org/doc/295506>.

@article{AndrzejIndrzejczak2018,
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.},
author = {Andrzej Indrzejczak},
journal = {Bulletin of the Section of Logic},
keywords = {sequent calculus; cut elimination; proof theory; extralogical rules},
language = {eng},
number = {4},
pages = {null},
title = {Rule-Generation Theorem and its Applications},
url = {http://eudml.org/doc/295506},
volume = {47},
year = {2018},
}

TY - JOUR
AU - Andrzej Indrzejczak
TI - Rule-Generation Theorem and its Applications
JO - Bulletin of the Section of Logic
PY - 2018
VL - 47
IS - 4
SP - null
AB - 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.
LA - eng
KW - sequent calculus; cut elimination; proof theory; extralogical rules
UR - http://eudml.org/doc/295506
ER -

References

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

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.