Open AccessClassifying Toposes for First Order Theories
Author(s) -
Carsten Butz,
Peter Johnstone
Publication year - 1997
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v4i20.18946
Subject(s) - topos theory , morphism , mathematics , order (exchange) , gödel's completeness theorem , completeness (order theory) , extension (predicate logic) , category theory , pure mathematics , discrete mathematics , computer science , mathematical analysis , art , literature , finance , economics , programming language
By a classifying topos for a first-order theory T, we mean a topos E such that, for any topos F, models of T in F correspond exactly to open geometric morphisms F ! E. We show that not every (infinitary) 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.