Sheaf semantics is developed within a constructive and predicative framework, Martin‐Löf's type theory. We prove strong completeness of many sorted, first order intuitionistic logic with respect to this semantics, by using sites of provably functional relations.

By a classifying topos for a first-order theory , we mean a topos such that, for any topos models of in correspond exactly to open geometric morphisms → . We show that not every first-order theory has a classifying topos in this sense, but we characterize those which do by an appropriate ‘smallness condition’, and we show that every Grothendieck topos arises as the classifying topos of such a theory. We also show that every first-order theory has a conservative extension (...) to one which possesses a classifying topos, and we obtain a Heyting-valued completeness theorem for infinitary first-order logic. (shrink)