Citations of:
An undecidable problem in correspondence theory
Journal of Symbolic Logic 56 (4):12611272 (1991)
Add citations
You must login to add citations.




This papers gives a survey of recent results about simulations of one class of modal logics by another class and of the transfer of properties of modal logics under extensions of the underlying modal language. We discuss: the transfer from normal polymodal logics to their fusions, the transfer from normal modal logics to their extensions by adding the universal modality, and the transfer from normal monomodal logics to minimal tense extensions. Likewise, we discuss simulations of normal polymodal logics by normal (...) 

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2 BASIC MODAL LOGIC . . . . . . . . . . . . . . . . . . . . . . . . . . . 3. 

In the basic modal language and in the basic modal language with the added universal modality, firstorder definability of all formulas over the class of all frames is shown. Also, it is shown that the problems of modal definability of firstorder sentences over the class of all frames in the languages and are both PSPACEcomplete. 

In a previous work we introduced the algorithm \SQEMA\ for computing firstorder equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. \SQEMA\ is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is satisfied. In this paper we develop several extensions of (...) 

We give a new proof of the following result : it is undecidable whether a given calculus, that is a finite set of propositional formulas together with the rules of modus ponens and substitution, axiomatizes the classical logic. Moreover, we prove the same for every superintuitionistic calculus. As a corollary, it is undecidable whether a given calculus is consistent, whether it is superintuitionistic, whether two given calculi have the same theorems, whether a given formula is derivable in a given calculus. (...) 



The main result is that is no effective algorithmic answer to the question:how to recognize whether arbitrary modal formula has a firstorder equivalent on the class of finite frames. Besides, two known problems are solved: it is proved algorithmic undecidability of finite frame consequence between modal formulas; the difference between global and local variants of firstorder definability of modal formulas on the class of transitive frames is shown. 

We provide syntactic necessary and sufficient conditions on the formulae reducible by the secondorder quantifier elimination algorithm DLS. It is shown that DLS is compete for all modal Sahlqvist and Inductive formulae, and that all modal formulae in a single propositional variable on which DLS succeeds are canonical. 