Abstract
We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view.
Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible.
We shall present such a proof of the uniform interpolation theorem for normal modal logics K and T. It provides an explicit algorithm constructing the interpolants.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Blackburn, P., M. de Rijke, and Y. Venema, Modal Logic, Cambridge University Press, 2001.
Boolos, G., The Logic of Provability, Cambridge University Press, New York and Cambridge, 1993.
Bull, R. A., ‘On modal logic with propositional quantifiers’, The Journal of Symbolic Logic 34:257–263, 1969.
Buss, S. R. (ed.), Handbook of Proof Theory, Elsevier, Amsterdam, 1998.
Chagrov, A., and M. Zakharyaschev, Modal Logic, Oxford University Press, 1998.
Heuerding, A., Sequent Calculi for Proof Search in Some Modal Logics, Thesis, University of Bern, 1998.
Heuerding, A., M. Seyfried, and H. Zimmermann, ‘Efficient loop-check for backward proof search in some non-classical propositional logics’, in P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi (eds.), 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNCS 1071, Springer, 1996, pp. 210–225.
Fine, K., ‘Propositional quantifiers in modal logic’, Theoria 36:336–346, 1970.
Ghilardi, S., and M. Zawadowski, ‘Undefinability of Propositional Quantifiers in the Modal System S4’, Studia Logica 55:259–271, 1995.
Ghilardi, S., and M. Zawadowski, ‘A sheaf representation and duality for finitely presented Heyting algebras’, The Journal of Symbolic Logic 60:911–939, 1995.
Kremer, P., ‘On the complexity of propositional quantification in intuitionistic logic’, The Journal of Symbolic Logic 62:529–544, 1997.
Kremer, P., ‘Quantifying over propositions in relevance logics: Non-axiomatizibility of 8 and 9’, The Journal of Symbolic Logic 58:334–349, 1993. Uniform Interpolation and Propositional Quantifiers in Modal Logics
Ladner, R., ‘The computational complexity of provability in systems of modal propositional logic’, SIAM Journal of Computation Vol. 6, No. 3:467–480, 1977.
Negri, S., and J. von Plato, Structural Proof Theory, Cambridge University Press, 2001.
Pitts, A., ‘On an interpretation of second order quantification in first order intuitionistic propositional logic’, The Journal of Symbolic Logic 57:33–52, 1992.
Sambin, G., and S. Valentini, ‘The modal logic of provability. The sequential approach’, Journal of Philosophical Logic 11: 311–342, 1982.
Shavrukov, V. Yu., Subalgebras of diagonalizable algebras of theories containing arithmetic, Dissertationes Mathematicae CCCXXIII, Polska Akademia Nauk, Mathematical Institute, Warszawa, 1993.
Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, Cambridge UniversityPress, 1996.
Visser, A., Bisimulations, ‘Model Descriptions and Propositional Quantifiers’, Logic Group Preprint Series No. 161, Utrecht, 1996.
Wansing, H., ‘Sequent systems for modal logics’, in D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, Vol. 8, Kluwer Academic Publishers, 2002, pp. 61–145.
Author information
Authors and Affiliations
Corresponding author
Additional information
Presented by Heinrich Wansing
Rights and permissions
About this article
Cite this article
Bílková, M. Uniform Interpolation and Propositional Quantifiers in Modal Logics. Stud Logica 85, 1–31 (2007). https://doi.org/10.1007/s11225-007-9021-5
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-007-9021-5