Algorithmic correspondence and completeness in modal logic. IV. Semantic extensions of SQEMA

Journal of Applied Non-Classical Logics 18 (2-3):175-211 (2008)
Download Edit this record How to cite View on PhilPapers
In a previous work 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 \SSQEMA\ 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 obtain restricted versions of \SSQEMA\ which guarantee canonicity, too.
PhilPapers/Archive ID
Upload history
Archival date: 2018-04-20
View other versions
Added to PP index

Total views
51 ( #54,959 of 2,448,853 )

Recent downloads (6 months)
1 ( #63,627 of 2,448,853 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.