62 citations · 126 across the 28 of their papers we have counts for
16 papers · 1 filter
Initial algebras from constructive ordinals
Benno van den Berg
We show how a standard constructive notion of ordinal supports a useful constructive theory of transfinite recursion. We do this by giving constructive proofs of various initial al…
Apartness and the elimination of strong forms of extensionality
Benno van den Berg
We introduce a new version of arithmetic in all finite types which extends the usual versions with primitive notions of extensionality and extensional equality. This new hybrid ver…
Conservativity of Type Theory over Higher-order Arithmetic
Benno van den Berg, Daniël Otten
We investigate how much type theory is able to prove about the natural numbers. A classical result in this area shows that dependent type theory without any universes is conservati…
Converse extensionality and apartness
Benno van den Berg, Robert Passmann
In this paper we try to find a computational interpretation for a strong form of extensionality, which we call "converse extensionality". Converse extensionality principles, which…
A Kuroda-style j-translation
Benno van den Berg
In topos theory it is well-known that any nucleus j gives rise to a translation of intuitionistic logic into itself in a way which generalises the Goedel-Gentzen negative translati…
Reverse Mathematics and parameter-free Transfer
Benno van den Berg, Sam Sanders
Recently, conservative extensions of Peano and Heyting arithmetic in the spirit of Nelson's axiomatic approach to Nonstandard Analysis, have been proposed. In this paper, we study…
A note on arithmetic in finite types
Benno van den Berg
We present a version of arithmetic in all finite types which allows for a definition of equality at higher types for which all congruence are derivable, for which the soundness of…
Nonstandard functional interpretations and categorical models
Amar Hadzihasanovic, Benno van den Berg
Recently, the second author, Briseid and Safarik introduced nonstandard Dialectica, a functional interpretation that is capable of eliminating instances of familiar principles of n…
The Axiom of Multiple Choice and Models for Constructive Set Theory
Benno van den Berg, Ieke Moerdijk
We propose an extension of Aczel's constructive set theory CZF by an axiom for inductive types and a choice principle, and show that this extension has the following properties: it…
Are There Enough Injective Sets?
Peter Aczel, Benno van den Berg, Johan Granstroem +1
The axiom of choice ensures precisely that, in ZFC, every set is projective: that is, a projective object in the category of sets. In constructive ZF (CZF) the existence of enough…
A functional interpretation for nonstandard arithmetic
Benno van den Berg, Eyvind Briseid, Pavol Safarik
We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Goedel and Shoenfield can be used to rewri…
Non-deterministic inductive definitions
Benno van den Berg
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…
Derived rules for predicative set theory: an application of sheaves
Benno van den Berg, Ieke Moerdijk
We show how one may establish proof-theoretic results for constructive Zermelo-Fraenkel set theory, such as the compactness rule for Cantor space and the Bar Induction rule for Bai…
Topological and simplicial models of identity types
Benno van den Berg, Richard Garner
In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do s…
Aspects of Predicative Algebraic Set Theory III: Sheaves
Benno van den Berg, Ieke Moerdijk
This is the third installment in a series of papers on algebraic set theory. In it, we develop a uniform approach to sheaf models of constructive set theories based on ideas from c…
Types are weak omega-groupoids
Benno van den Berg, Richard Garner
We define a notion of weak omega-category internal to a model of Martin-Löf type theory, and prove that each type bears a canonical weak omega-category structure obtained from the…