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
Revision history
Archival date: 2018-04-20
View upload history
References found in this work BETA
Modal Logic.Blackburn, Patrick; de Rijke, Maarten & Venema, Yde
Modal Logic.Chagrov, Alexander

View all 8 references / Add more references

Citations of this work BETA

Add more citations

Added to PP index

Total views
36 ( #44,492 of 48,987 )

Recent downloads (6 months)
9 ( #45,266 of 48,987 )

How can I increase my downloads?

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