The previously introduced algorithm \sqema\ computes first-order 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 first-order logic with monadic least fixed-points \mffo. This computation operates by transforming input formulae into locally frame equivalent ones in the pure fragment of the hybrid mu-calculus. In particular, we prove that (...) the recursive extension of \sqema\ succeeds on the class of `recursive formulae'. We also show that a certain version of this algorithm guarantees the canonicity of the formulae on which it succeeds. (shrink)

We show that every extension of the basic hybrid logic with modal Sahlqvist axioms is complete. As a corollary of our approach, we also obtain the Beth property for a large class of hybrid logics. Finally, we show that the new completeness result cannot be combined with the existing general completeness result for pure axioms.

Minimal predicates P satisfying a given first-order description ϕ(P) occur widely in mathematical logic and computer science. We give an explicit first-order syntax for special first-order 'PIA conditions' ϕ(P) which quarantees unique existence of such minimal predicates. Our main technical result is a preservation theorem showing PIA-conditions to be expressively complete for all those first-order formulas that are preserved under a natural model-theoretic operation of 'predicate intersection'. Next, we show how iterated predicate minimization on PIA-conditions yields a language MIN(FO) equal (...) in expressive power to LFP(FO), first-order logic closed under smallest fixed-points for monotone operations. As a concrete illustration of these notions, we show how our sort of predicate minimization extends the usual frame correspondence theory of modal logic, leading to a proper hierarchy of modal axioms: first-order-definable, first-order fixed-point definable, and beyond. (shrink)

Taking Löb's Axiom in modal provability logic as a running thread, we discuss some general methods for extending modal frame correspondences, mainly by adding fixed-point operators to modal languages as well as their correspondence languages. Our suggestions are backed up by some new results – while we also refer to relevant work by earlier authors. But our main aim is advertizing the perspective, showing how modal languages with fixed-point operators are a natural medium to work with.

Minimal predicates P satisfying a given first-order description φ(P) occur widely in mathematical logic and computer science. We give an explicit first-order syntax for special first-order ‘PIA conditions’ φ(P) which guarantees unique existence of such minimal predicates. Our main technical result is a preservation theorem showing PIA-conditions to be expressively complete for all those first-order formulas that are preserved under a natural model-theoretic operation of ‘predicate intersection’. Next, we show how iterated predicate minimization on PIA-conditions yields a language MIN(FO) equal (...) in expressive power to LFP(FO), first-order logic closed under smallest fixed-points for monotone operations. As a concrete illustration of these notions, we show how our sort of predicate minimization extends the usual frame correspondence theory of modal logic, leading to a proper hierarchy of modal axioms: first-order-definable, first-order fixed-point definable, and beyond. (shrink)

We generalize and extend the class of Sahlqvist formulae in arbitrary polyadic modal languages, to the class of so called inductive formulae. To introduce them we use a representation of modal polyadic languages in a combinatorial style and thus, in particular, develop what we believe to be a better syntactic approach to elementary canonical formulae altogether. By generalizing the method of minimal valuations à la Sahlqvist–van Benthem and the topological approach of Sambin and Vaccaro we prove that all inductive formulae (...) are elementary canonical and thus extend Sahlqvist’s theorem over them. In particular, we give a simple example of an inductive formula which is not frame-equivalent to any Sahlqvist formula. Then, after a deeper analysis of the inductive formulae as set-theoretic operators in descriptive and Kripke frames, we establish a somewhat stronger model-theoretic characterization of these formulae in terms of a suitable equivalence to syntactically simpler formulae in the extension of the language with reversive modalities. Lastly, we study and characterize the elementary canonical formulae in reversive languages with nominals, where the relevant notion of persistence is with respect to discrete frames. (shrink)

We study a canonical modal logic introduced by Lemmon, and axiomatised by an infinite sequence of axioms generalising McKinsey’s formula. We prove that the class of all frames for this logic is not closed under elementary equivalence, and so is non-elementary. We also show that any axiomatisation of the logic involves infinitely many non-canonical formulas.