zbMATH — the first resource for mathematics

An undecidable problem in correspondence theory. (English) Zbl 0737.03018
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 J. van Benthem [Handbook of philosophical logic, Vol. II, 167-247 (1984; Zbl 0572.03003); Modal logic and classical logic (1985; Zbl 0639.03014); see Notre Dame J. Formal Logic 30, No. 1, 20-35 (1989; Zbl 0671.03013) 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.

03D35 Undecidability and degrees of sets of sentences
03D05 Automata and formal grammars in connection with logical questions
03B20 Subsystems of classical logic (including intuitionistic logic)
03B45 Modal logic (including the logic of norms)
Full Text: DOI
[1] Theoria 43 pp 195– (1977)
[2] Notre Dame Journal of Formal Logic 30 pp 20– (1989)
[3] Handbook of philosophical logic 2 pp 167– (1984)
[4] Modal logic and classical logic (1985) · Zbl 0639.03014
[5] DOI: 10.2307/1970290 · Zbl 0105.00802 · doi:10.2307/1970290
[6] Algebra i Logika 29 pp 613– (1990)
[7] Logical methods of constructing effective algorithms pp 135– (1986)
[8] Logical-algebraic constructions pp 96– (1987)
[9] Undecidability of the disjunction property of superintuitionistic calculi (1989)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.