Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-29T12:52:12.393Z Has data issue: false hasContentIssue false
  • English
  • Français

The undecidability of the disjunction property of propositional logics and other related problems

Published online by Cambridge University Press:  12 March 2014

Alexander Chagrov  and
Michael Zakharyaschev
Alexander Chagrov
Affiliation:
Tver State University, 170013 Tver, Russia
Michael Zakharyaschev
Affiliation:
Keldysh Institute of Applied Mathematics, Russian Academy of Sciences, 125047 Moscow, Russia, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Extract

‘How can we recognize, given axioms and inference rules of a calculus, whether the calculus has such-and-such property?’ A question of this kind arises whenever we deal with a new logic system. For large families of logics, this question may be considered as an algorithmic problem, and a property is called decidable in a given family if there exists an algorithm which is capable of deciding, for a finite axiomatics of a calculus in the family, whether or not it has the property.

In the class of intermediate propositional logics, for instance, nontrivial properties such as the tabularity, pretabularity, and interpolation property (Maksimova [1972, 1977]) are decidable. However, for many other important properties—decidability, finite model property, disjunction property, Halldén-completeness, etc.—effective criteria were not found in spite of considerable efforts.

In this paper we show that the difficulties in investigating these properties in the classes of intermediate logics and normal modal logics containing S4 are of principal nature, since all of them turn out to be algorithmically undecidable. In other words, there are no algorithms which, given a finite set of axioms of an intermediate or modal calculus, can recognize whether or not it is decidable, Halldén-complete, has the finite model or disjunction property.

The first results concerning the undecidability of properties of calculi seem to have been obtained by Linial and Post [1949], who proved the undecidability of the problem of equivalence to classical calculus in the class of all propositional calculi with the same language as the classical one and the two inference rules: modus ponens and substitution. Kuznetsov [1963] generalized this result having proved the undecidability of the problem of equivalence to any fixed intermediate calculus (for instance, to intuitionistic calculus or even the inconsistent one). However, these results will not hold if we confine ourselves only to the class of intermediate logics, though the problem of equivalence to the undecidable intermediate calculus of Shehtman [1978] is clearly undecidable in this class as well.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 58 , Issue 3 , September 1993 , pp. 967 - 1002
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

Anderson, J. G. [1972], Superconstructive propositional calculi with extra axiom schemes containing one variable, Zeitschrift für Mathematisehe Logik und Grundlagen der Mathematik, vol. 18, pp. 113–130.CrossRefGoogle Scholar
van Benthem, J. F. A. K. and Humberstone, I. L. [1983], Hallden-completeness by gluing of Kripke frames, Notre Dame Journal of Formal Logic, vol. 24, pp. 426–430.Google Scholar
Blok, W. J. [1976], Varieties of interior algebras, Dissertation, University of Amsterdam, Amsterdam.Google Scholar
Chagrov, A. V. [1990], Undecidable properties of extensions of the provability logic, Part I, Algebra and Logic, vol. 29, pp. 350–367; Part 11, Algebra and Logic, pp. 614–623.Google Scholar
Chagrov, A. V. [1992], The cardinality of the set of maximal intermediate logics with the disjunction property is of continuum, Mathematicheskie Zametki, vol. 51, pp. 117–123. (Russian)Google Scholar
Chagrov, A. V. [1993], Undecidable properties of superintuitionistic logics, Mathematical problems of cybernetics (Jablonsky, S. V. editor) (to appear). (Russian)Google Scholar
Chagrova, L. V. [1991], An undecidable problem in correspondence theory, this Journal, vol. 56, pp. 1261–1272.Google Scholar
Chagrov, A. V. and Zakharyaschev, M. V. [1989], The undecidability of the disjunction property of intermediate calculi, Institute of Applied Mathematics, the USSR Academy of Sciences, no. 57, preprint. (Russian)Google Scholar
Chagrov, A. V. and Zakharyaschev, M. V. [1991], The disjunction property of intermediate propositional logics, Stadia Logica, vol. 50, pp. 189–216.CrossRefGoogle Scholar
Chagrov, A. V. and Zakharyaschev, M. V. [1992], Modal companions of intermediate propositional logics, Studia Logica, vol. 51, pp. 49–82.CrossRefGoogle Scholar
Dummett, M. A. E. and Lemmon, E. J. [1959], Modal logics between S4 and S5, Zeitschrift für Mathematisehe Logik und Grundlagen der Mathematik, vol. 5, pp. 250–264.CrossRefGoogle Scholar
Esakia, L. L. [1979], On the variety of Grzegorczyk algebras, Study on non-classical logics and set theory, “Nauka”, Moscow, pp. 257–287. (Russian)Google Scholar
Fine, K. [1974], An ascending chain of S4 logics, Theoria, vol. 40, pp. 110–116.CrossRefGoogle Scholar
Fine, K. [1985], Logics containing K4. Part II, this Journal, vol. 50, pp. 619–651.Google Scholar
Gabbay, D. M. [1970], The decidability of the Kreisel-Putnam system, this Journal, vol. 35, pp. 431–437.Google Scholar
Gabbay, D. M. and De Jongh, D. H. J. [1974], A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property, this Journal, vol. 39, pp. 67–78.Google Scholar
Galanter, G. I. [1988], Halldén-completeness for superintuitionistic logics, Proceedings of IV Soviet-Finland Symposium for Mathematical Logic, Tbilisi, Moscow, Institute of Philosophy, USSR Academy of Sciences, pp. 81–89. (Russian)Google Scholar
Goldblatt, R. I. [1976], Metamathematics of modal logic, Reports on Mathematical Logic, vol. 6, pp. 41–77; Reports on Mathematical Logic, vol. 7, pp. 21–52.Google Scholar
Gudovshchikov, V. L. and Rybakov, V. V. [1982], The disjunction property in modal logics, Proceedings of 8th USSR Conference “Logic and Methodology of Science”, Vilnius, Moscow, Institute of Philosophy, USSR Academy of Sciences, pp. 35–36. (Russian)Google Scholar
Jankov, V. A. [1963], Relationship between deducibility in the intuitionistic propositional calculus and finite implicational structures, Soviet Mathematics Doklady, vol. 8, pp. 1203–1204.Google Scholar
Kracht, M. [1991], Internal definability and completeness in modal logic, Dissertation, Freie Univer-sität, Berlin.Google Scholar
Kreisel, G. and Putnam, H. [1957], Eine Vnableitbarkeit-sbeweismethode für den intuitionistischen Aussagenkalkul, Archiv für Mathematische Logik undGrundlagenforschung, vol. 3, pp. 74–78.CrossRefGoogle Scholar
Kuznetsov, A. V. [1963], The undecidability of the general problems of completeness, solvability and equivalence of propositional calculi, Algebra and Logic, vol. 2, pp. 47–66. (Russian)Google Scholar
Linial, S. and Post, E. L. [1949], Recursive unsolvability of the deducibility, Tarski's completeness and independence of axioms problems of the propositional calculus, Bulletin of the American Mathematical ociety, vol. 55, p. 50.Google Scholar
McKay, C. G. [1968], The decidability of certain intermediate logics, this Journal, vol. 33, pp. 258–264.Google Scholar
Maksimova, L. L. [1972], Pretabular superintuitionistic logics, Algebra and Logic, vol. 11, pp. 558–570. (Russian)CrossRefGoogle Scholar
Maksimova, L. L. [1976], The principle of variable separation in propositional logics, Algebra and Logic, vol. 15, pp. 168–184. (Russian)CrossRefGoogle Scholar
Maksimova, L. L. [1977], The Craig theorem in superintuitionistic logics and amalgamated varieties of pseudo-Boolean algebras, Algebra and Logic, vol. 16, pp. 643–681. (Russian)CrossRefGoogle Scholar
Maksimova, L. L. [1979], Interpolation properties of superintuitionistic logics, Stadia Logica, vol. 38, pp. 419–428.CrossRefGoogle Scholar
Maksimova, L. L. [1979a], Interpolation theorems in modal logics and amalgamated varieties of topo-Boolean algebras, Algebra and Logic, vol. 18, pp. 556–586. (Russian)CrossRefGoogle Scholar
Maksimova, L. L. [1986], On maximal intermediate logics with the disjunction property, Studia Logica, vol. 45, pp. 69–75.CrossRefGoogle Scholar
Maksimova, L. L. and Rybakov, V. V. [1974], On the lattice of normal modal logics, Algebra and Logic, vol. 13, pp. 188–216. (Russian)CrossRefGoogle Scholar
Minari, P. [1986], Intermediate logics with the same disjunctionless fragment as intuitionistic logic, Studia Logica, vol. 45, pp. 207–222.CrossRefGoogle Scholar
Minsky, M. L. [1961], Recursive unsolvability of Post's problem of “Tag” and other topics in the theory of Turing machines, Annals of Mathematics, vol. 74, pp. 437–455.CrossRefGoogle Scholar
Nishimura, I. [1960], On formulas of one variable in intuitionistic propositional calculus, this Journal, vol. 25, pp. 327–331.Google Scholar
Ono, H. [1972], Some results on the intermediate logics, Research Institute for Mathematical Sciences vol. 8, Kyoto University, Kyoto, pp. 117–130.Google Scholar
Rasiowa, H. and Sikorski, R. [1963], The mathematics of metamathematics, Polish Scientific Publishers, Warsaw.Google Scholar
Segerberg, K. [1971], An essay in classical modal logic, Philosophical Studies, vol. 13, University of Uppsala, Uppsala.Google Scholar
Shehtman, V. B. [1978], An undecidable superintuitionistic calculus, Soviet Mathematics Doklady, vol. 240, pp. 549–552. (Russian)Google Scholar
Shehtman, V. B. [1980], Topological models of propositional logics, Semiotics and Informatics, vol. 15, pp. 74–98. (Russian)Google Scholar
Sobolev, S. K. [1977], On the finite approximability of superintuitionistic logics, Mathematicheskiĭ Sbornik, vol. 102, pp. 289–301. (Russian)Google Scholar
Thomason, S. K. [1982], Undecidability of the completeness problem of modal logic, Universal Algebra and Applications, vol. 9, Banach Center Publications, Warsaw, pp. 341–345.Google Scholar
Wronski, A. [1973], Intermediate logics and the disjunction property, Reports on Mathematical Logic, vol. 1, pp. 39–51.Google Scholar
Wronski, A. [1974], Remarks on intermediate logics with axioms containing only one variable, Reports on Mathematical Logic, vol. 2, pp. 63–75.Google Scholar
Zakharyaschev, M. V. [1983], On intermediate logics, Soviet Mathematics Doklady, vol. 27, pp. 274–277.Google Scholar
Zakharyaschev, M. V. [1984], Normal modal logics containing S4, Soviet Mathematics Doklady, vol. 29, pp. 252–255.Google Scholar
Zakharyaschev, M. V. [1987], On the disjunction property of intermediate and modal logics, Mathematicheskie Zametki, vol. 42, pp. 729–738; English translation, Mathematical Notes, vol. 42, pp. 901–905.Google Scholar
Zakharyaschev, M. V. [1988], Syntax and semantics of modal logics containing S4, Algebra and logic, vol. 27, pp. 659–689; English translation, Algebra and Logic, vol. 27, pp. 408–428.Google Scholar
Zakharyaschev, M. V. [1989], Syntax and semantics of intermediate logics, Algebra and Logic, vol. 28, pp. 402–429; English translation, Algebra and Logic, vol. 28, pp. 262–282.Google Scholar
Zakharyaschev, M. V. [1989a], Modal companions of intermediate logics: syntax, semantics and preservation theorems, Mathematicheskiĭ Sbornik, vol. 180, pp. 1415–1427; English translation, Mathematics of the USSR Sbornik, vol. 68 (1991), pp. 277–289.Google Scholar
Zakharyaschev, M. V. [1990], The greatest extension of S4 in which the Heyting propositional calculus is embeddable, manuscript.Google Scholar
Zakharyaschev, M. V. [1992], Canonical formulas for K4. Part I: Basic results, this Journal, vol. 57 (1992), pp. 1377–1402.Google Scholar
Zakharyaschev, M. V. [1993], A new solution to a problem of T. Hosoi and H. Ono, Notre Dame Journal of Formal Logic (to appear).Google Scholar