Tech Reports


Observational Truth as Categorical Modality

Grant Malcom


This paper examines the notion of truth-up-to-observability in the setting of categorical logic and shows that it can be captured by a modal operator. Our main results extend the Kripke-Beth-Joyal semantics for the logics of presheaf toposes to the observational modality. We also give a categorical account of coinduction (or bisimulation) as a proof-technique for establishing observational truth. We assume familiarity with basic notions from category theory, including: functor, natural transformation, subcategory and subfunctor. Keywords: modal logics, categorical logic, topos theory, Kripke-Beth-Joyal semantics, behavioural equality, observational equality, hidden algebra.

[Full Paper]