Two-dimensional Kripke Semantics I: Presheaves

TL;DR

This paper explores the relationship between Kripke semantics and categorical semantics for modal logic, focusing on the two-dimensional perspective using presheaves, bridging traditional and modern approaches.

Contribution

It establishes a correspondence between Kripke semantics and categorical semantics for modal logic using presheaves, advancing the understanding of their connection.

Findings

Demonstrates the equivalence between Kripke and categorical semantics

Introduces a two-dimensional framework using presheaves

Bridges modal logic with category theory

Abstract

The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.