Two-dimensional Kripke Semantics II: Stability and Completeness
Copyright policy )Two-dimensional Kripke Semantics II: Stability and Completeness
We revisit the duality between Kripke and algebraic semantics of intuitionistic and intuitionistic modal logic. We find that there is a certain mismatch between the two semantics, which means that not all algebraic models can be embedded into a Kripke model. This leads to an alternative proposal for a relational semantics, the stable semantics. Instead of an arbitrary partial order, the stable semantics requires a distributive lattice of worlds. We constructively show that the stable semantics is exactly as complete as the algebraic semantics. Categorifying these results leads to a 2-duality between two-dimensional stable semantics and categories of product-preserving presheaves, i.e. models of algebraic theories in the style of Lawvere. Comment: Accepted at MFPS 2024
- University of Bristol
- University of Bristol United Kingdom
FOS: Computer and information sciences, relational semantics, Computer Science - Logic in Computer Science, /dk/atira/pure/core/keywords/programming_languages, intuitionistic logic, algebraic theories, FOS: Mathematics, Category Theory (math.CT), semantics, modal logic, Mathematics - Category Theory, Mathematics - Logic, /dk/atira/pure/core/keywords/programming_languages; name=Programming Languages, F.4.1; F.3.2, 03B45 (Primary), 03B20, 03B70, 68Q55, 06D20, 06D22, 06D05, 06D50, 18A15, 18A40, 18F20, 18D60, 18C10 (Secondary), 004, Logic in Computer Science (cs.LO), category theory, categorification, intuitionism, F.4.1, F.3.2, name=Programming Languages, Logic (math.LO), Lawvere theories
FOS: Computer and information sciences, relational semantics, Computer Science - Logic in Computer Science, /dk/atira/pure/core/keywords/programming_languages, intuitionistic logic, algebraic theories, FOS: Mathematics, Category Theory (math.CT), semantics, modal logic, Mathematics - Category Theory, Mathematics - Logic, /dk/atira/pure/core/keywords/programming_languages; name=Programming Languages, F.4.1; F.3.2, 03B45 (Primary), 03B20, 03B70, 68Q55, 06D20, 06D22, 06D05, 06D50, 18A15, 18A40, 18F20, 18D60, 18C10 (Secondary), 004, Logic in Computer Science (cs.LO), category theory, categorification, intuitionism, F.4.1, F.3.2, name=Programming Languages, Logic (math.LO), Lawvere theories
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).0 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!