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

(14)

• Slanted canonicity of analytic inductive inequalities
• scientific article; zbMATH DE number 7243670 (Why is no real title available?)
• Canonical extensions: an algebraic approach to Stone duality
• Modelling socio-political competition
• Sahlqvist via translation
• Toward an epistemic-logical theory of categorization
• Algebraic modal correspondence: Sahlqvist and beyond
• Constructive canonicity in non-classical logics
• Canonicity results of substructural and lattice-based logics
• Categories: how I learned to stop worrying and love two sorts
• Linear Logic Properly Displayed
• Rough concepts
• THE LOGIC OF RESOURCES AND CAPABILITIES
• Algorithmic correspondence and canonicity for non-distributive 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)