Citations of:
Add citations
You must login to add citations.


In this paper we consider the normal modal logics of elementary classes defined by firstorder formulas of the form \. We prove that many properties of these logics, such as finite axiomatisability, elementarity, axiomatisability by a set of canonical formulas or by a single generalised Sahlqvist formula, together with modal definability of the initial formula, either simultaneously hold or simultaneously do not hold. 

The previously introduced algorithm \sqema\ computes firstorder frame equivalents for modal formulae and also proves their canonicity. Here we extend \sqema\ with an additional rule based on a recursive version of Ackermann's lemma, which enables the algorithm to compute local frame equivalents of modal formulae in the extension of firstorder logic with monadic least fixedpoints \mffo. This computation operates by transforming input formulae into locally frame equivalent ones in the pure fragment of the hybrid mucalculus. In particular, we prove that (...) 





Sahlqvist formulas are a syntactically specified class of modal formulas proposed by Hendrik Sahlqvist in 1975. They are important because of their firstorder definability and canonicity, and hence axiomatize complete modal logics. The firstorder properties definable by Sahlqvist formulas were syntactically characterized by Marcus Kracht in 1993. The present paper extends Kracht's theorem to the class of ‘generalized Sahlqvist formulas' introduced by Goranko and Vakarelov and describes an appropriate generalization of Kracht formulas. 



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 define analogues of modal Sahlqvist formulas for the modal mucalculus, and prove a correspondence theorem for them. 

We define analogues of modal Sahlqvist formulas for the modal mucalculus, and prove a correspondence theorem for them. 





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. 

Minimal predicates P satisfying a given firstorder description φ(P) occur widely in mathematical logic and computer science. We give an explicit firstorder syntax for special firstorder ‘PIA conditions’ φ(P) which guarantees unique existence of such minimal predicates. Our main technical result is a preservation theorem showing PIAconditions to be expressively complete for all those firstorder formulas that are preserved under a natural modeltheoretic operation of ‘predicate intersection’. Next, we show how iterated predicate minimization on PIAconditions yields a language MIN(FO) equal (...) 

In this paper, we extend the canonicity methodology in Ghilardi & Meloni (1997) to arbitrary lattice expansions, and syntactically describe canonical inequalities for lattice expansions consisting of meet preserving operations, multiplicative operations, adjoint pairs, and constants. This approach gives us a uniform account of canonicity for substructural and latticebased logics. Our method not only covers existing results, but also systematically accounts for many canonical inequalities containing nonsmooth additive and multiplicative uniform operations. Furthermore, we compare our technique with the approach in (...) 



In this paper, we establish the firstorder definability of sequents with consistent variable occurrence on biapproximation semantics by means of the Sahlqvist–van Benthem algorithm. Then together with the canonicity results in Suzuki (2011), this allows us to establish a Sahlqvist theorem for substructural logic. Our result is not limited to substructural logic but is also easily applicable to other latticebased logics. 





