Tech Reports

ULCS-02-030

Observational Truth as Categorical Modality

Grant Malcom

Abstract

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.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.