Hostname: page-component-7b7567c8c-tnzcf Total loading time: 0 Render date: 2026-11-15T00:58:49.223Z Has data issue: false hasContentIssue false
  • English
  • Français

An undecidable problem in correspondence theory

Published online by Cambridge University Press:  12 March 2014

L. A. Chagrova
L. A. Chagrova*
Affiliation:
Department of Mathematics, Tver State University, 170013 Tver, USSR
Get accessRights & Permissions [Opens in a new window]

Extract

In this paper we prove undecidability of first-order definability of propositional formulas. The main result is proved for intuitionistic formulas, but it remains valid for other kinds of propositional formulas by analogous arguments or with the help of various translations.

For general background on correspondence theory the reader is referred to van Benthem [1], [2] (see [3] for a survey of recent results).

The method for the proofs of undecidability in this paper will be to simulate calculations of a Minsky machine by intuitionistic formulas. §3 concerns this simulation. Effective procedures for the construction of simulating modal formulas can be found in the literature (cf. [4]).

The principal results of the paper are in §4. §5 gives some further undecidability results, that will be proved in another paper by modification of the method of this paper.

I am indebted to the referee for drawing my attention to some errors in an earlier version of this paper.

Information

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 56 , Issue 4 , December 1991, pp. 1261 - 1272
Copyright
Copyright © Association for Symbolic Logic 1991

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]van Benthem, J. F. A. K., Modal logic and classical logic, Bibliopolis, Napoli, 1985.Google Scholar
[2]van Benthem, J. F. A. K., Correspondence theory, Handbook of philosophical logic. Vol. 2, Reidel, Dordrecht, 1984, pp. 167–247.CrossRefGoogle Scholar
[3]van Benthem, J. F. A. K., Notes on modal definability, Notre Dame Journal of Formal Logic, vol. 30 (1989), pp. 20–35.Google Scholar
[4]Isard, S., A finitely axiomatizable undecidable extension of K, Theoria, vol. 43 (1977), pp. 195–202.CrossRefGoogle Scholar
[5]Minsky, M. L., Recursive unsolvability of Post's problem of “Tag” and other topics in the theory of Turing machines, Annals of Mathematics, ser. 2, vol. 74 (1961), pp. 437–455.CrossRefGoogle Scholar
[6]Chagrova, L. A., An algorithm for constructing a first-order equivalent on frames for disjunctionless intuitionistic formulas, Logical-algebraic constructions (Gorchakov, Yu. M., editor), Kalininskiĭ Gosudarstvennyĭ Universitet, Kalinin, 1987, pp. 96–100. (Russian)Google Scholar
[7]Rodenburg, P. H., Intuitionistic correspondence theory, Dissertation, Amsterdam, 1986.Google Scholar
[8]Chagrova, L. A., On first-order definability of intuitionistic formulas with limitations on occurrences of conductions, Logical methods of constructing effective algorithms (Kanovich, M. I., editor), Kalininskiĭ Gosudarstvennyĭ Universitet, Kalinin, 1986, pp. 135–136. (Russian)Google Scholar
[9]Zakhar'yashchev, M. V. and Chagrov, A. V., Undecidability of the disjunction property of superintuitionistic calculi, Preprint No. 57, Keldysh Institute of Applied Mathematics, Academy of Sciences of the USSR, Moscow, 1989. (Russian). MR 90 j: 03046.Google Scholar
[10]Chagrov, A. V., Undecidable properties of extensions of the provability logic. I, II, Algebra i Logika, vol. 29 (1990), pp. 350–367, 613–623; English translation, Algebra and Logic, vol. 29 (1990) (to appear).Google Scholar