Topos Semantics for Higher-Order Modal Logic

DOI10.2143/LEA.228.0.3078176MaRDI QIDQ2974975zbMATH OpenFDO

Authors Kohei Kishida, Hans-Christoph Kotzsch, Steve Awodey

Publication date 11 April 2017

Full work available at URL https://arxiv.org/abs/1403.0020

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Categorical logic, topoi (03G30) Topoi (18B25)

Abstract: We define the notion of a model of higher-order modal logic in an arbitrary elementary topos $mathcalE$. In contrast to the well-known interpretation of (non-modal) higher-order logic, the type of propositions is not interpreted by the subobject classifier $Omeg{a}_{mathcalE}$, but rather by a suitable complete Heyting algebra $H$. The canonical map relating $H$ and $Omeg{a}_{mathcalE}$ both serves to interpret equality and provides a modal operator on $H$ in the form of a comonad. Examples of such structures arise from surjective geometric morphisms $f:mathcalFomathcalE$, where $H=f_{a}stOmeg{a}_{mathcalF}$. The logic differs from non-modal higher-order logic in that the principles of functional and propositional extensionality are no longer valid but may be replaced by modalized versions. The usual Kripke, neighborhood, and sheaf semantics for propositional and first-order modal logic are subsumed by this notion.

Cited in

(8)

• On Blass translation for Leśniewski's propositional ontology and modal logics
• scientific article; zbMATH DE number 7453977 (Why is no real title available?)
• AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS
• Doctrines, modalities and comonads
• Morpho-logic from a topos perspective -- application to symbolic AI
• A presheaf semantics for quantified temporal logics
• Two-dimensional Kripke semantics i: presheaves
• Modal hyperdoctrine: higher-order and non-normal extensions

This page was built for publication: Topos Semantics for Higher-Order Modal Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2974975)