Elementary canonical formulae: extending Sahlqvist's theorem

DOI10.1016/j.apal.2005.10.005zbMath1111.03018OpenAlexW2048154108MaRDI QIDQ2498906

Dimiter Vakarelov, Valentin F. Goranko

Publication date: 16 August 2006

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2005.10.005

zbMATH Keywords

modal logicpersistencefirst-order definabilitynominalselementary canonical formulaepolyadic modal languagespure formulaereversive languagesSahlqvist formulae

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Related Items

Algebraic modal correspondence: Sahlqvist and beyond, Correspondence theory for modal Fairtlough-Mendler semantics of intuitionistic modal logic, Unnamed Item, Algorithmic correspondence and canonicity for distributive modal logic, Sahlqvist theorem for modal fixed point logic, The Ackermann approach for modal logic, correspondence theory and second-order reduction, Algorithmic correspondence and completeness in modal logic. V. Recursive extensions of SQEMA, Modal frame correspondences and fixed-points, Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras via an implementation of the algorithm \textsf{PEARL}, Sahlqvist correspondence for modal mu-calculus, On canonicity of poset expansions, Modal definability of first-order formulas with free variables and query answering, CANONICITY RESULTS OF SUBSTRUCTURAL AND LATTICE-BASED LOGICS, A dichotomy for some elementarily generated modal logics, A SAHLQVIST THEOREM FOR SUBSTRUCTURAL LOGIC, Algorithmic correspondence and canonicity for non-distributive logics, The bounded proof property via step algebras and step frames, Unnamed Item, Non-finitely axiomatisable modal product logics with infinite canonical axiomatisations, Towards incorporating background theories into quantifier elimination, Completeness and Correspondence in Hybrid Logic via an Extension of SQEMA, On the strength and scope of DLS, An extension of Kracht's theorem to generalized Sahlqvist formulas, Unnamed Item, Algorithmic Correspondence for Relevance Logics I. The Algorithm $$\mathsf {PEARL}$$

Uses Software

• SQEMA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A Sahlqvist theorem for distributive modal logic
• An incomplete system of modal logic
• Topology and duality in modal logic
• Atom structures and Sahlqvist equations
• Tools and techniques in modal logic
• Modal logic with names
• Generalized quantifiers and modal logic
• On the canonicity of Sahlqvist identities
• Sahlqvist's theorem for Boolean algebras with operators with an application to cylindric algebras
• Constructive canonicity in non-classical logics
• Computing circumscription revisited: A reduction algorithm
• Simulation and transfer results in modal logic -- a survey
• Varieties of complex algebras
• Sahlqvist Formulas in Hybrid Polyadic Modal Logics
• Algorithmic Correspondence and Completeness in Modal Logic. II. Polyadic and Hybrid Extensions of the Algorithm SQEMA
• First-order definability in modal logic
• Derivation rules as anti-axioms in modal logic
• Erdős Graphs Resolve Fine's Canonicity Problem
• A new proof of Sahlqvist's theorem on modal definability and completeness
• Bounded distributive lattice expansions
• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
• Relational and Kleene-Algebraic Methods in Computer Science
• Boolean Algebras with Operators. Part I
• Rudiments of \(\mu\)-calculus
• Persistence and atomic generation for varieties of Boolean algebras with operators