Two-dimensional Kripke Semantics II: Stability and Completeness

G. A. Kavvos

doi:10.48550/arXiv.2406.03578

Two-dimensional Kripke Semantics II: Stability and Completeness

G. A. Kavvos

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

100 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Electronic Notes in Theoretical Informatics and Computer Science (ENTICS)
Number of pages	20
Volume	4
DOIs	https://doi.org/10.48550/arXiv.2406.03578 https://doi.org/10.46298/entics.14767
Publication status	Published - 15 Dec 2024
Event	40th Conference on Mathematical Foundations of Programming Semantics - Oxford, United Kingdom Duration: 19 Jun 2024 → 21 Jun 2024 Conference number: 40 https://oxford24.github.io/

Publication series

Name	Electronic Notes in Theoretical Informatics and Computer Science (ENTICS)
ISSN (Electronic)	2969-2431

Conference

Conference	40th Conference on Mathematical Foundations of Programming Semantics
Abbreviated title	MFPS XL
Country/Territory	United Kingdom
City	Oxford
Period	19/06/24 → 21/06/24
Internet address	https://oxford24.github.io/

Bibliographical note

Publisher Copyright:
© G.A. Kavvos.

Research Groups and Themes

Programming Languages

Keywords

modal logic
category theory
Lawvere theories
algebraic theories
categorification
semantics
intuitionism
intuitionistic logic
relational semantics

Access to Document

10.48550/arXiv.2406.03578Licence: CC BY
10.46298/entics.14767Licence: CC BY

Full-text PDF (pre-print)Submitted manuscript, 595 KBLicence: CC BY
Full-text PDF (final published version)Final published version, 536 KBLicence: CC BY

Handle.net

Persistent link

Towards Directed Model Categories
Kavvos, A. (Principal Investigator)
1/03/24 → 30/11/24
Project: Research
Language Embeddings for Proof Engineering
Kavvos, A. (Principal Investigator)
1/12/23 → 30/11/25
Project: Research

Cite this

@inproceedings{228cc0ecc32f431c92b5ff72e68131bc,

title = "Two-dimensional Kripke Semantics II: Stability and Completeness",

abstract = "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.",

keywords = "modal logic, category theory, Lawvere theories, algebraic theories, categorification, semantics, intuitionism, intuitionistic logic, relational semantics",

author = "Kavvos, \{G. A.\}",

note = "Publisher Copyright: {\textcopyright} G.A. Kavvos.; 40th Conference on Mathematical Foundations of Programming Semantics, MFPS XL ; Conference date: 19-06-2024 Through 21-06-2024",

year = "2024",

month = dec,

day = "15",

doi = "10.48550/arXiv.2406.03578",

language = "English",

volume = "4",

series = "Electronic Notes in Theoretical Informatics and Computer Science (ENTICS)",

booktitle = "Electronic Notes in Theoretical Informatics and Computer Science (ENTICS)",

url = "https://oxford24.github.io/",

}

Kavvos, GA 2024, Two-dimensional Kripke Semantics II: Stability and Completeness. in Electronic Notes in Theoretical Informatics and Computer Science (ENTICS). vol. 4, Electronic Notes in Theoretical Informatics and Computer Science (ENTICS), 40th Conference on Mathematical Foundations of Programming Semantics, Oxford, United Kingdom, 19/06/24. https://doi.org/10.48550/arXiv.2406.03578, https://doi.org/10.46298/entics.14767

TY - GEN

T1 - Two-dimensional Kripke Semantics II

T2 - 40th Conference on Mathematical Foundations of Programming Semantics

AU - Kavvos, G. A.

N1 - Conference code: 40

PY - 2024/12/15

Y1 - 2024/12/15

N2 - 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.

AB - 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.

KW - modal logic

KW - category theory

KW - Lawvere theories

KW - algebraic theories

KW - categorification

KW - semantics

KW - intuitionism

KW - intuitionistic logic

KW - relational semantics

U2 - 10.48550/arXiv.2406.03578

DO - 10.48550/arXiv.2406.03578

M3 - Conference Contribution (Conference Proceeding)

VL - 4

T3 - Electronic Notes in Theoretical Informatics and Computer Science (ENTICS)

BT - Electronic Notes in Theoretical Informatics and Computer Science (ENTICS)

Y2 - 19 June 2024 through 21 June 2024

ER -

Two-dimensional Kripke Semantics II: Stability and Completeness

Abstract

Publication series

Conference

Bibliographical note

Research Groups and Themes

Keywords

Access to Document

Handle.net

Fingerprint

Projects

Towards Directed Model Categories

Language Embeddings for Proof Engineering

Cite this