Order:
  1.  28
    Relating First-Order Set Theories, Toposes and Categories of Classes.Steve Awodey, Carsten Butz, Alex Simpson & Thomas Streicher - 2014 - Annals of Pure and Applied Logic 165 (2):428-502.
  2.  49
    Relating First-Order Set Theories and Elementary Toposes.Steve Awodey, Carsten Butz & Alex Simpson - 2007 - Bulletin of Symbolic Logic 13 (3):340-358.
    We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  3.  9
    Classifying Toposes for First-Order Theories.Carsten Butz & Peter Johnstone - 1998 - Annals of Pure and Applied Logic 91 (1):33-58.
    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 (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  4.  9
    Saturated Models of Intuitionistic Theories.Carsten Butz - 2004 - Annals of Pure and Applied Logic 129 (1-3):245-275.
    We use the language of categorical logic to construct generic saturated models of intuitionistic theories. Our main technique is the thorough study of the filter construction on categories with finite limits, which is the completion of subobject lattices under filtered meets. When restricted to coherent or Heyting categories, classifying categories of intuitionistic first-order theories, the resulting categories are filtered meet coherent categories, coherent categories with complete subobject lattices such that both finite disjunctions and existential quantification distribute over filtered meets. Such (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  30
    A Topological Completeness Theorem.Carsten Butz - 1999 - Archive for Mathematical Logic 38 (2):79-101.
    We prove a topological completeness theorem for infinitary geometric theories with respect to sheaf models. The theorem extends a classical result of Makkai and Reyes, stating that any topos with enough points has an open spatial cover. We show that one can achieve in addition that the cover is connected and locally connected.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  6.  6
    Syntax and Semantics of the Logic.Carsten Butz - 1997 - Notre Dame Journal of Formal Logic 38 (3):374-384.
    In this paper we study the logic , which is first-order logic extended by quantification over functions (but not over relations). We give the syntax of the logic as well as the semantics in Heyting categories with exponentials. Embedding the generic model of a theory into a Grothendieck topos yields completeness of with respect to models in Grothendieck toposes, which can be sharpened to completeness with respect to Heyting-valued models. The logic is the strongest for which Heyting-valued completeness is known. (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  7.  3
    Syntax and Semantics of the Logic Llambdaomega Omega.Carsten Butz - 1997 - Notre Dame Journal of Formal Logic 38 (3):374-384.
  8.  2
    Syntax and Semantics of the Logic $\Mathcal{L}^\Lambda_{\Omega\Omega}$.Carsten Butz - 1997 - Notre Dame Journal of Formal Logic 38 (3):374-384.
    In this paper we study the logic $\mathcal{L}^\lambda_{\omega\omega}$, which is first-order logic extended by quantification over functions . We give the syntax of the logic as well as the semantics in Heyting categories with exponentials. Embedding the generic model of a theory into a Grothendieck topos yields completeness of $\mathcal{L}^\lambda_{\omega\omega}$ with respect to models in Grothendieck toposes, which can be sharpened to completeness with respect to Heyting-valued models. The logic $\mathcal{L}^\lambda_{\omega\omega}$ is the strongest for which Heyting-valued completeness is known. Finally, (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark