9 found
Sort by:
  1. Peter Aczel, Benno van den Berg, Johan Granström & Peter Schuster (forthcoming). Are There Enough Injective Sets? Studia Logica.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  2. Benno van den Berg & Ieke Moerdijk (2014). The Axiom of Multiple Choice and Models for Constructive Set Theory. Journal of Mathematical Logic 14 (1):1450005.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  3. Benno van den Berg (2013). Non-Deterministic Inductive Definitions. Archive for Mathematical Logic 52 (1-2):113-135.
    We study a new proof principle in the context of constructive Zermelo-Fraenkel set theory based on what we will call “non-deterministic inductive definitions”. We give applications to formal topology as well as a predicative justification of this principle.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  4. Benno van den Berg, Eyvind Briseid & Pavol Safarik (2012). A Functional Interpretation for Nonstandard Arithmetic. Annals of Pure and Applied Logic 163 (12):1962-1994.
    We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Gödel and Shoenfield can be used to rewrite proofs performed in these systems into standard ones. These functional interpretations show in particular that our nonstandard systems are conservative extensions of E-HAω and E-PAω, strengthening earlier results by Moerdijk and Palmgren, and Avigad and Helzner. We will also indicate how our rewriting algorithm can be used for term extraction purposes. To conclude the (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  5. Benno van den Berg & Ieke Moerdijk (2012). Derived Rules for Predicative Set Theory: An Application of Sheaves. Annals of Pure and Applied Logic 163 (10):1367-1383.
  6. Benno Van Den Berg & Ieke Moerdijk (2008). Aspects of Predicative Algebraic Set Theory I: Exact Completion. Annals of Pure and Applied Logic 156 (1):123-159.
    This is the first in a series of papers on Predicative Algebraic Set Theory, where we lay the necessary groundwork for the subsequent parts, one on realizability [B. van den Berg, I. Moerdijk, Aspects of predicative algebraic set theory II: Realizability, Theoret. Comput. Sci. . Available from: arXiv:0801.2305, 2008], and the other on sheaves [B. van den Berg, I. Moerdijk, Aspects of predicative algebraic set theory III: Sheaf models, 2008 ]. We introduce the notion of a predicative category with small (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  7. Benno van Den Berg & Federico de Marchi (2007). Models of Non-Well-Founded Sets Via an Indexed Final Coalgebra Theorem. Journal of Symbolic Logic 72 (3):767-791.
    The paper uses the formalism of indexed categories to recover the proof of a standard final coalgebra theorem, thus showing existence of final coalgebras for a special class of functors on finitely complete and cocomplete categories. As an instance of this result, we build the final coalgebra for the powerclass functor, in the context of a Heyting pretopos with a class of small maps. This is then proved to provide models for various non-well-founded set theories, depending on the chosen axiomatisation (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  8. Benno van den Berg & Federico De Marchi (2007). Non-Well-Founded Trees in Categories. Annals of Pure and Applied Logic 146 (1):40-59.
    Non-well-founded trees are used in mathematics and computer science, for modelling non-well-founded sets, as well as non-terminating processes or infinite data structures. Categorically, they arise as final coalgebras for polynomial endofunctors, which we call M-types. We derive existence results for M-types in locally cartesian closed pretoposes with a natural numbers object, using their internal logic. These are then used to prove stability of such categories with M-types under various topos-theoretic constructions; namely, slicing, formation of coalgebras , and sheaves for an (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  9. Benno van den Berg (2005). Inductive Types and Exact Completion. Annals of Pure and Applied Logic 134 (2-3):95-121.
    Using the theory of exact completions, I construct a certain class of pretoposes, consisting of what one might call “predicative realizability toposes”, that can act as categorical models of certain predicative type theories, including Martin-Löf Type Theory.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation