A Topos-Theoretic Semantics of Intuitionistic Modal Logic with an Application to the Logic of Branching Spacetime

TL;DR

This paper develops a topos-theoretic semantics for intuitionistic modal logic using Alexandrov topology, with applications to branching space-time models and philosophical implications about the nature of possible entities.

Contribution

It introduces an internal topological semantics for intuitionistic modal logic within elementary toposes, linking it to branching space-time and epistemic interpretations.

Findings

Models intuitionistic S4 and S5 using topological operators

Applies semantics to branching space-time of Belnap

Shows invalidity of certain first-order formulas like the Barcan converse

Abstract

The Alexandrov topology affords a well-known semantics of modal necessity and possibility. This paper develops an Alexandrov topological semantics of intuitionistic propositional modal logic internally in any elementary topos. This is done by constructing interior and closure operators on the power-object associated to a given relation in the ambient topos. When the relation is an order, these operators model intuitionistic S4; when the relation is an equivalence relation, they also model the characteristic (B) axiom of classical S5. The running example of interest arises from the Branching space-time of Nuel Belnap, which is shown to induce a histories presheaf upon which can be defined an equivalence relation of being obviously undivided at a given point event. These results have some philosophical implications. For example, we study the branching space-time example in light of the indistinguishability interpretation of epistemic modal logic. We will also study several famous first-order formulas in presheaf topos semantics such as the so-called Barcan formula. We shall see, however, that one of the Barcan converses is invalidated by a simple example of non-trivial space-time branching. This invalidates a thesis of metaphysical actualism, namely, that there are no possibly existing but non-actual entities.