Abstract

The category-theoretic notion of a topos is called upon to study the syntax and semantics of higher-order logic. Syntactical systems of logic are replaced by topoi, and models by functors on those topoi, as per the general scheme of functorial semantics. Each logical theory T gives rise to a syntactic topos ${\cal I}\lbrack U\sb{T}\rbrack$ of polynomial-like objects. The chief result is the universal characterization of ${\cal I}\lbrack U\sb{T}\rbrack$ as a so-called classifying topos: for any topos ${\cal E},$ the category ${\bf Log}$ of logical morphisms ${\cal I}\lbrack U\sb{T}\rbrack\to{\cal E}$ is naturally equivalent to the category ${\bf Mod}\sb{T}$ of models of T in ${\cal E}$,$${\bf Log}\simeq{\bf Mod}\sb{T}.$$In particular, there is a T-model $U\sb{T}$ in ${\cal I}\lbrack U\sb{T}\rbrack$ such that any T-model in any topos is an image of $U\sb{T}$ under an essentially unique logical morphism. In this sense, ${\cal I}\lbrack U\sb{T}\rbrack$ is freely generated by this "universal" model $U\sb{T}$ of T. ;Having cast the principal logical notions in familiar algebraic terms, it becomes possible to apply standard algebraic and functorial techniques to some classical logical topics, such as interpolation, definability, and completeness. For example, a well-known theorem of Grothendieck states that every commutative ring is isomorphic to the ring of global sections of a sheaf of local rings. A similar sheaf representation theorem for topoi is proved using the theory of stacks and indexed categories. Combining this result with the classifying topos theorem, one can infer the completeness of higher-order logic with respect to certain topoi that are much like Sets. A stronger version of the classical Henkin completeness theorem for higher-order logic follows as a corollary.