A topos-theoretic approach to reference and modality (Q1182706)

The paper develops a topos-theoretic semantics for a higher-order modal theory supposed to interprete a fragment of natural language. The author begins with some linguistic arguments explaining his approach, in which count nouns are interpreted as ``kinds'' which are modally constant. Formally, ``kinds'' correspond to sorts and ``predicates of kinds'' to terms (or formulas). The semantics is given by a geometric morphism \({\mathcal E}\to\mathbb{S}\), where \(\mathcal E\) is thought of as a universe of variable sets, and \(\mathbb{S}\) as a universe of constant sets. The modal theory is described as a Gentzen-type axiomatic system; the soundness theorem is proved.