Algorithmic correspondence and completeness in modal logic

ABSTRACT. In [CON 06b] we introduced the algorithm SQEMA for computing first-order 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 SQEMA where that syntactic condition is replaced by a semantic one, viz. downward monotonicity. For the first, and most general, extension SemSQEMA we prove correctness for a large class of modal formulae containing an extension of the Sahlqvist formulae, defined by replacing polarity with monotonicity. By employing a special modal version of Lyndon's monotonicity theorem and imposing additional requirements on the Ackermann rule we obta...

• Type: Journal
• Year: 2008
• Where: JANCL
• Authors: Willem Conradie, Valentin Goranko
• Keywords: Certain Negative Polarity, JANCL 2008, Modal Formulae, Modal Version