13 found
Order:
  1.  15
    A Functional Interpretation for Nonstandard Arithmetic.Benno van den Berg, Eyvind Briseid & Pavol Safarik - 2012 - 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)  
     
    Export citation  
     
    Bookmark   6 citations  
  2.  4
    Aspects of Predicative Algebraic Set Theory I: Exact Completion.Benno van den Berg & Ieke Moerdijk - 2008 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  3.  7
    Reverse Mathematics and Parameter-Free Transfer.Benno van den Berg & Sam Sanders - 2019 - Annals of Pure and Applied Logic 170 (3):273-296.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  4.  4
    Inductive Types and Exact Completion.Benno van den Berg - 2005 - 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)  
     
    Export citation  
     
    Bookmark   4 citations  
  5.  5
    Derived Rules for Predicative Set Theory: An Application of Sheaves.Benno van den Berg & Ieke Moerdijk - 2012 - Annals of Pure and Applied Logic 163 (10):1367-1383.
  6.  1
    A Kuroda-Style J -Translation.Benno van den Berg - forthcoming - Archive for Mathematical Logic:1-8.
    A nucleus is an operation on the collection of truth values which, like double negation in intuitionistic logic, is monotone, inflationary, idempotent and commutes with conjunction. Any nucleus determines a proof-theoretic translation of intuitionistic logic into itself by applying it to atomic formulas, disjunctions and existentially quantified subformulas, as in the Gödel–Gentzen negative translation. Here we show that there exists a similar translation of intuitionistic logic into itself which is more in the spirit of Kuroda’s negative translation. The key is (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  7.  4
    Non-Well-Founded Trees in Categories.Benno van den Berg & Federico De Marchi - 2007 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  8.  4
    Models of Non-Well-Founded Sets Via an Indexed Final Coalgebra Theorem.Benno van Den Berg & Federico de Marchi - 2007 - 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 (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  9.  5
    Nonstandard Functional Interpretations and Categorical Models.Amar Hadzihasanovic & Benno van den Berg - 2017 - Notre Dame Journal of Formal Logic 58 (3):343-380.
    Recently, the second author, Briseid, and Safarik introduced nonstandard Dialectica, a functional interpretation capable of eliminating instances of familiar principles of nonstandard arithmetic—including overspill, underspill, and generalizations to higher types—from proofs. We show that the properties of this interpretation are mirrored by first-order logic in a constructive sheaf model of nonstandard arithmetic due to Moerdijk, later developed by Palmgren, and draw some new connections between nonstandard principles and principles that are rejected by strict constructivism. Furthermore, we introduce a variant of (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  10.  11
    Non-Deterministic Inductive Definitions.Benno van den Berg - 2013 - 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)  
     
    Export citation  
     
    Bookmark  
  11.  2
    A Note on Equality in Finite-Type Arithmetic.Benno van den Berg - 2017 - Mathematical Logic Quarterly 63 (3-4):282-288.
    We present a version of arithmetic in all finite types based on a systematic use of an internally definable notion of observational equivalence for dealing with equalities at higher types. For this system both intensional and extensional models are possible, the deduction theorem holds and the soundness of the Dialectica interpretation is provable inside the system itself.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  12.  2
    The Strength of Countable Saturation.Benno van den Berg, Eyvind Briseid & Pavol Safarik - 2017 - Archive for Mathematical Logic 56 (5-6):699-711.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  13.  5
    The Axiom of Multiple Choice and Models for Constructive Set Theory.Benno van den Berg & Ieke Moerdijk - 2014 - Journal of Mathematical Logic 14 (1):1450005.