Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-29T00:32:20.975Z Has data issue: false hasContentIssue false
  • English
  • Français

Derivation rules as anti-axioms in modal logic

Published online by Cambridge University Press:  12 March 2014

Yde Venema
Yde Venema*
Affiliation:
Faculteit der Wijsbegeerte, Rijksuniversiteit Utrecht, 3584 CS Utrecht, The Netherlands, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We discuss a ‘negative’ way of defining frame classes in (multi)modal logic, and address the question of whether these classes can be axiomatized by derivation rules, the ‘non-ξ rules’, styled after Gabbay's Irreflexivity Rule. The main result of this paper is a metatheorem on completeness, of the following kind: If ⋀ is a derivation system having a set of axioms that are special Sahlqvist formulas and ⋀+ is the extension of ⋀ with a set of non-ξ rules, then ⋀+ is strongly sound and complete with respect to the class of frames determined by the axioms and the rules.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 58 , Issue 3 , September 1993 , pp. 1003 - 1034
Copyright
Copyright © Association for Symbolic Logic 1993

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

References

REFERENCES

[1]Andréka, H., Németi, I. and Sain, I., On the strength of temporal proofs, Theoretical Computer Science, vol. 80 (1991), pp. 125–151.CrossRefGoogle Scholar
[2]van Benthem, J. F. A. K., Correspondence theory, Handbook of philosophical logic, vol. II (Gabbay, D. M. and Guenthner, F., editors), Reidel, Dordrecht, 1984, pp. 167–247.CrossRefGoogle Scholar
[3]van Benthem, J. F. A. K., Modal logic and classical logic, Bibliopolis, Naples, 1985.Google Scholar
[4]van Benthem, J. F. A. K., Language in action, North-Holland, Amsterdam, 1991.Google Scholar
[5]Blackburn, P., Nominal Tense Logic, Ph.D. Dissertation, University of Edinburgh, Edinburgh, 1989.Google Scholar
[6]Burgess, J. P., Decidability for branching time, Studio Logica, vol. 39 (1980), pp. 203–218.CrossRefGoogle Scholar
[7]Crossley, J. (editor), Algebra and Logic, Lecture Notes in Mathematics, vol. 450, Springer-Verlag, Berlin, 1975.CrossRefGoogle Scholar
[8]Gabbay, D. M., An irreflexivity lemma with applications to axiomatizations of conditions on linear frames, Aspects of philosophical logic (Monnich, V., editor), Reidel, Dordrecht, 1981, pp. 67–89.CrossRefGoogle Scholar
[9]Gabbay, D. M. and Guenthner, F. (editors), Handbook of philosophical logic, vol. II, Reidel, Dordrecht, 1984.CrossRefGoogle Scholar
[10]Gabbay, D. M. (in collaboration with Hodkinson, I. and Reynolds, M.), Temporal logic: mathematical foundations and computational aspects, Oxford University Press, Oxford, 1992.Google Scholar
[11]Gabbay, D. M. and Hodkinson, I. M., An axiomatization of the temporal logic with since and until over the real numbers, Journal of Logic and Computation, vol. 1 (1990), pp. 229–259.CrossRefGoogle Scholar
[12]Gargov, G. and Goranko, V., Modal logic with names, Colloquium on modal logic 1991 (de Rijke, M., editor), Dutch Network for Language, Logic and Information, Amsterdam, 1991, pp. 81–103.Google Scholar
[13]Gargov, G., Passy, S., and Tinchev, T., Modal environment for Boolean speculations, Mathematical logic and its applications (Skordev, D., editor), Plenum Press, New York, 1987, pp. 253–263.CrossRefGoogle Scholar
[14]Goldblatt, R., Metamathematics of modal logic, Reports on Mathematical Logic, vol. 6 (1976), pp. 41–77; Reports on Mathematical Logic, vol. 7 (1976), pp. 21–52.Google Scholar
[15]Goldblatt, R., Varieties of complex algebras, Annals of Pure and Applied Logic, vol. 44 (1989), pp. 173–242.CrossRefGoogle Scholar
[16]Goldblatt, R. and Thomason, S., Axiomatic classes in propositional modal logic, Algebra and logic (Crossley, J., editor), Lecture Notes in Mathematics, vol. 450, Springer-Verlag, Berlin, 1975, pp. 163–173.CrossRefGoogle Scholar
[17]Goranko, V., Applications of quasi-structural rules to axiomatizations in modal logic, Logic colloquium ’91, abstracts of the 9th international congress of logic, methodology and philosophy of sciences, Uppsala, 1991, vol. I: logic, p. 119. (Abstract)Google Scholar
[18]Jónsson, B. and Tarski, Alfred, Boolean algebras with operators, American Journal of Mathematics, vol. 73 (1951), pp. 891–939; American Journal of Mathematics, vol. 74 (1952), pp. 127–162.CrossRefGoogle Scholar
[19]Kanger, S. (editor), Proceedings of the third Scandinavian logic symposium, Uppsala 1973, North-Holland, Amsterdam, 1975.Google Scholar
[20]Koymans, R., Specifying message passing and time-critical systems with temporal logic, Ph.D. Dissertation, Eindhoven University of Technology, Eindhoven, 1989.CrossRefGoogle Scholar
[21]Kracht, M., How completeness and correspondence theory got married, Colloquium on modal logic 1991 (de Rijke, M., editor), Dutch Network for Language, Logic and Information, Amsterdam, 1991, pp. 161–185.Google Scholar
[22]Kuhn, S., The domino relation: flattening a two-dimensional logic, Journal of Philosophical Logic, vol. 18 (1989), pp. 173–195.CrossRefGoogle Scholar
[23]Logic colloquium ’91, abstracts of the 9th international congress of logic, methodology and philosophy of sciences, Uppsala, 1991, vol. I: logic.Google Scholar
[24]Mönnich, U. (editor), Aspects of philosophical logic, Reidel, Dordrecht, 1981.CrossRefGoogle Scholar
[25]Németi, I., Algebraizations of quantifier logics: an introductory overview, Studia Logica, vol. 50 (1991), pp. 485–570.CrossRefGoogle Scholar
[26]Passy, S. and Tinchev, T., PDL with data constants, Information Processing Letters, vol. 20 (1985), pp. 35–41.CrossRefGoogle Scholar
[27]Reynolds, M., Complete axiomatization for until and since over the reals—IRR rule not needed, Studia Logica, vol. 51 (1992), pp. 165–194.CrossRefGoogle Scholar
[28]De Rijke, M., The modal logic of inequality, this Journal, vol. 57 (1992), pp. 566–584.Google Scholar
[29]De Rijke, M. (editor), Colloquium on modal logic 1991, Dutch Network for Language, Logic and Information, Amsterdam, 1991.Google Scholar
[30]Roorda, D., Resource logics: proof-theoretical investigations, Ph.D. Dissertation, University of Amsterdam, Amsterdam, 1991.Google Scholar
[31]Sahlqvist, H., Completeness and correspondence in the first and second order semantics for modal logic, Proceedings of the third Scandinavian logic symposium, Uppsala 1973 (Kanger, S., editor), North-Holland, Amsterdam, 1975, pp. 110–143.CrossRefGoogle Scholar
[32]Sain, I., Successor axioms increase the program verification powers of the “sometime + nexttime” logic, preprint no. 23 (1983), Mathematical Institute of the Hungarian Academy of Sciences, Budapest.Google Scholar
[33]Sain, I., Is “some-other-time” sometimes better than “sometime” for proving partial correctness of programs?, Studia Logica, vol. 47 (1988), pp. 279–301.CrossRefGoogle Scholar
[34]Sain, I., Temporal logics need their clocks, Theoretical Computer Science, vol. 95 (1992), pp. 75–96.CrossRefGoogle Scholar
[35]Sambin, G. and Vaccaro, V., A new proof of Sahlqvist's theorem on modal definability and completeness, this Journal, vol. 54 (1989), pp. 992–999.Google Scholar
[36]Skordev, D. (editor), Mathematical logic and its applications, Plenum Press, New York, 1987.CrossRefGoogle Scholar
[37]Venema, Y., Expressiveness and completeness of an interval tense logic, Notre Dame Journal of Formal Logic, vol. 31 (1990), pp. 529–547.CrossRefGoogle Scholar
[38]Venema, Y., Two-dimensional modal logics for relation algebras and temporal logic of intervals, ITLI-prepublication series LP-89-03, University of Amsterdam, Amsterdam, 1989.Google Scholar
[39]Venema, Y., A modal logic for chopping intervals, Journal of Logic and Computation, vol. 1 (1991), pp. 453–476.CrossRefGoogle Scholar
[40]Venema, Y., Completeness by completeness: since and until, Colloquium on modal logic 1991 (de Rijke, M., editor), Dutch Network for Language, Logic and Information, Amsterdam, 1991, pp. 279–285.Google Scholar
[41]Venema, Y., The tense logic of dominoes, Journal of Philosophical Logic, vol. 21 (1992), pp. 173–182.CrossRefGoogle Scholar
[42]Venema, Y., Many-dimensional modal logic, Doctoral Dissertation, University of Amsterdam, Amsterdam, 1991.Google Scholar
[43]Venema, Y., Cylindric modal logic, 1992, this Journal (to appear).Google Scholar
[44]Zanardo, A., A finite axiomatization of the set of strongly valid Ockhamist formulas, Journal of Philosophical Logic, vol. 14(1985), pp. 447–468.CrossRefGoogle Scholar
[45]Venema, Y., A complete deductive system for since-until branching-time logic, Journal of Philosophical Logic, vol. 20 (1991), pp. 131–148.Google Scholar
[46]Venema, Y., Axiomatization of ‘Peircean’ branching-time logic, Studia Logica, vol. 49 (1990), pp. 183–196.Google Scholar