>>556 追加

higher-order logic topos で検索すると
高名な 下記のSteve Awodey先生がヒット
Kohei Kishida Who?
” sheaf semantics, models are built on presheaves ”
なるほど、層や圏から、higher-order logicへ繋がっていくのか（＾＾

参考
https://arxiv.org/pdf/1403.0020.pdf
Topos Semantics for Higher-Order Modal Logic March 4, 2014
Steve Awodey? Kohei Kishida† Hans-Christoph Kotzsch‡
†Department of Computer Science, University of Oxford
(抜粋)
Abstract. We define the notion of a model of higher-order modal logic
in an arbitrary elementary topos E. In contrast to the well-known interpretation of (non-modal) higher-order logic, the type of propositions is not interpreted by the subobject classifier ΩE , but rather by a suitable complete Heyting algebra H.
The canonical map relating H and ΩE 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 : F → E, where H = f?ΩF .
The logic differs from non-modal higher-order logic in that the principles of functional and propositional extensionality are not 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.

In many conventional systems of semantics for quantified modal logic, models are built on presheaves.
Given a set K of “possible worlds”, Kripke’s semantics [11], for
instance, assigns to each world k ∈ K a domain of quantification P(k) - regarded
as the set of possible individuals that “exist” in k - and then ∃x Φ is true at k iff
some a ∈ P(k) satisfies Φ at k.
(引用終り)