Constructive canonicity for lattice-based fixed point logics

DOI10.1007/978-3-662-55386-2_7MaRDI QIDQ1685915zbMATH OpenOpenAlexFDO

Authors Willem Conradie, Alessandra Palmigiano, Zhiguang Zhao, Andrew P. K. Craig

Publication date 20 December 2017

Full work available at URL https://arxiv.org/abs/1603.06547

zbMATH Keywords

canonicitylattice-based fixed point logicslogics for categorizationunified correspondence

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Other constructive mathematics (03F65)

Abstract: We prove the algorithmic canonicity of two classes of $mu$-inequalities in a constructive meta-theory of normal lattice expansions. This result simultaneously generalizes Conradie and Craig's canonicity for $mu$-inequalities based on a bi-intuitionistic bi-modal language, and Conradie and Palmigiano's constructive canonicity for inductive inequalities (restricted to normal lattice expansions to keep the page limit). Besides the greater generality, the unification of these strands smoothes the existing treatments for the canonicity of $mu$-formulas and inequalities. In particular, the rules of the algorithm ALBA used for this result have exactly the same formulation as those of Conradie and Palmigiano, with no additional rule added specifically to handle the fixed point binders. Rather, fixed points are accounted for by certain restrictions on the application of the rules, concerning the order-theoretic properties of the term functions associated with the formulas to which the rules are applied.

Recommendations

• Canonicity results of substructural and lattice-based logics
• Constructive canonicity in non-classical logics
• Canonical extensions for congruential logics with the deduction theorem
• Fixed point theory for complete T-lattice in logic programming
• Canonicity for intensional logics with even axioms
• Canonicity for intensional logics without iterative axioms
• scientific article; zbMATH DE number 1543335
• Note on some fixed point constructions in provability logic
• Algorithmic correspondence and canonicity for non-distributive logics

Cited in

(16)

• Constructive canonicity in non-classical logics
• Canonical extensions: an algebraic approach to Stone duality
• Modelling socio-political competition
• Algorithmic correspondence and canonicity for non-distributive logics
• Algebraic modal correspondence: Sahlqvist and beyond
• Categories: how I learned to stop worrying and love two sorts
• Canonicity results of substructural and lattice-based logics
• Toward an epistemic-logical theory of categorization
• THE LOGIC OF RESOURCES AND CAPABILITIES
• Sahlqvist via translation
• Slanted canonicity of analytic inductive inequalities
• Constructive canonicity of inductive inequalities
• Linear Logic Properly Displayed
• Rough concepts
• Inductive sequents for distributive modal logic
• Unified inverse correspondence for LE-logics

This page was built for publication: Constructive canonicity for lattice-based fixed point logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1685915)