Hostname: page-component-7b7567c8c-wxvwp Total loading time: 0 Render date: 2026-11-15T05:34:13.216Z Has data issue: false hasContentIssue false
  • English
  • Français

Interpolation for first order S5

Published online by Cambridge University Press:  12 March 2014

Melvin Fitting
Melvin Fitting*
Affiliation:
Department of Mathematics and Computer Science, Lehman College (CUNY), Bronx, NY 10468., USA, E-mail: fitting@lehman.cuny.edu, URL: comet.lehman.cuny.edu/fitting
Get accessRights & Permissions [Opens in a new window]

Abstract

An interpolation theorem holds for many standard modal logics, but first order S5 is a prominent example of a logic for which it fails. In this paper it is shown that a first order S5 interpolation theorem can be proved provided the logic is extended to contain propositional quantifiers. A proper statement of the result involves some subtleties, but this is the essence of it.

Information

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 67 , Issue 2 , June 2002, pp. 621 - 634
Copyright
Copyright © Association for Symbolic Logic 2002

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable

References

REFERENCES

[1]Ackermann, W., Solvable cases of the decision problem, North-Holland, Amsterdam, 1954.Google Scholar
[2]Areces, Carlos, Blackburn, Patrick, and Marx, Maarten, Hybrid logics: Characterization, interpolation and complexity, this Journal, vol. 66 (2001), pp. 977–1010.Google Scholar
[3]Bull, R. A., On modal logic with propositional quantifiers, this Journal, vol. 34 (1969), no. 2, pp. 257–263.Google Scholar
[4]Fine, Kit, Propositional quantifiers in modal logic, Theoria, vol. 36 (1970), pp. 336–346.CrossRefGoogle Scholar
[5]Fine, Kit, Failures of the interpolation lemma in quantified modal logic, this Journal, vol. 44 (1979), pp. 201–206.Google Scholar
[6]Fitting, Melvin C., Tableau methods of proof for modal logics, Notre Dame Journal of Formal Logic, vol. 13 (1972), pp. 237–247.CrossRefGoogle Scholar
[7]Fitting, Melvin C., Proof methods for modal and intuitionistic logics, D. Reidel Publishing Co., Dordrecht, 1983.CrossRefGoogle Scholar
[8]Fitting, Melvin C., First-order logic and automated theorem proving, Springer-Verlag, 1996. first edition. 1990.CrossRefGoogle Scholar
[9]Fitting, Melvin C. and Mendelsohn, R., First-order modal logic, Kluwer, 1998, paperback. 1999.CrossRefGoogle Scholar
[10]Goldblatt, Robert, Mathematics of modality, CSLI Lecture Notes, no. 43, CSLI, Stanford, CA. 1993.Google Scholar
[11]Kaplan, David, S5 with quantifiable propositional variables, this Journal, vol. 35 (1970), no. 2, p. 355.Google Scholar
[12]Prawitz, Dag, Hauptsatz for higher order logic, this Journal, vol. 33 (1968), pp. 452–457.Google Scholar
[13]Russell, Bertrand, The principles of mathematics, Allen and Unwin, London, 1903.Google Scholar
[14]Smullyan, R. M., First-order logic, Springer-Verlag, Berlin, 1968, revised edition, Dover Press, New York, 1994.CrossRefGoogle Scholar
[15]Stockmeyer, L. J., The complexity of decision problems in automata theory and logic, Technical Report MAC TR-133, MIT, Cambridge, MA. 1974.Google Scholar
[16]Takahashi, Moto-o, A proof of cut-elimination theorem in simple type theory, Journal of the Mathematical Society of Japan, vol. 19 (1967), pp. 399–410.CrossRefGoogle Scholar
[17]Thomason, S. K., Semantic analysis of tense logic, this Journal, vol. 37 (1972), pp. 150–158.Google Scholar