arXiv subjects
Publications and source records attributed to 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 the Dialectica interpretation is provable inside the system itself, which allows for both intensional and extensional models and for which the deduction theorem holds.
Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky's univalent foundations and the interpretation of Martin-Lof's identity types in Quillen model categories as some of the highlights. In this paper we establish a connection between a natural weakening of Martin-Lof's rules for the identity types which has been considered by Cohen, Coquand, Huber and Mortberg in their work on a constructive interpretation of the univalence axiom on the one hand, and the notion of a path category, a slight variation on the classic notion of a category of fibrant objects due to Brown. This involves showing that the syntactic category associated to a type theory with weak identity types carries the structure of a path category, strengthening earlier results by Avigad, Lumsdaine and Kapulkin. In this way we not only relate a well-known concept in homotopy theory with a natural concept in logic, but also provide a framework for further developments.
We will give a detailed account of why the simplicial sets model of the univalence axiom due to Voevodsky also models W-types. In addition, we will discuss W-types in categories of simplicial presheaves and an application to models of set theory.
We review the concept of a univalent fibration and show by elementary means that every Kan fibration in simplicial sets can be embedded in a univalent Kan fibration.
Any functor from the category of C*-algebras to the category of locales that assigns to each commutative C*-algebra its Gelfand spectrum must be trivial on algebras of nxn-matrices for n at least 3. This obstruction also applies to other spectra such as those named after Zariski, Stone, and Pierce. We extend these no-go results to functors with values in (ringed) topological spaces, (ringed) toposes, schemes, and quantales. The possibility of spectra in other categories is discussed.
Recently, the second author, Briseid and Safarik introduced nonstandard Dialectica, a functional interpretation that is capable of eliminating instances of familiar principles of nonstandard arithmetic - including overspill, underspill, and generalisations to higher types - from proofs. We show that, under few metatheoretical assumptions, 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. In doing so, we also draw some new connections between nonstandard principles, and principles that are rejected by strict constructivism. Furthermore, we introduce a variant of the Diller-Nahm interpretion with two different kinds of quantifiers (with and without computational meaning), similar to Hernest's light Dialectica interpretation, and show that one can obtain nonstandard Dialectica from this by weakening the computational content of the existential quantifiers -- a process we call herbrandisation. We also define a constructive sheaf model mirroring this new functional interpretation and show that the process of herbrandisation has a clear meaning in terms of these sheaf models.
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 is interpretable in Martin-Lof's type theory (hence acceptable from a constructive and generalised-predicative standpoint). In addition, it is strong enough to prove the Set Compactness Theorem and the results in formal topology which make use of this theorem. Moreover, it is stable under the standard constructions from algebraic set theory, namely exact completion, realizability models, forcing as well as more general sheaf extensions. As a result, methods from our earlier work can be applied to show that this extension satisfies various derived rules, such as a derived compactness rule for Cantor space and a derived continuity rule for Baire space. Finally, we show that this extension is robust in the sense that it is also reflected by the model constructions from algebraic set theory just mentioned.
We define a new topos, the Herbrand topos, inspired by the modified realizability topos and our earlier work on Herbrand realizability. We also introduce the category of Herbrand assemblies and characterise these as the double-negation-separated objects in the Herbrand topos. In addition, we show that the category of sets is included as the category of double-negation-sheaves and prove that the inclusion functor preserves and reflects validity of first-order formulas.
We introduce a new topos in order to give a semantic account of the nonstandard functional interpretation introduced by Eyvind Briseid, Pavol Safarik and the author.
Any functor from the category of C*-algebras to the category of locales that assigns to each commutative C*-algebra its Gelfand spectrum must be trivial on algebras of nxn-matrices for n at least 3. The same obstruction applies to the Zariski, Stone, and Pierce spectra. The possibility of spectra in categories other than that of locales is briefly discussed.
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.
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 rewrite proofs performed in these systems into standard ones. These functional interpretations show in particular that our nonstandard systems are conservative extensions of extensional Heyting and Peano arithmetic in all finite types, strengthening earlier results by Moerdijk, Palmgren, Avigad and Helzner. We will also indicate how our rewriting algorithm can be used for term extraction purposes. To conclude the paper, we will point out some open problems and directions for future research and mention some initial results on saturation principles.
We explain the motivation for looking for a predicative analogue of the notion of a topos and propose two definitions. For both notions of a predicative topos we will present the basic results, providing the groundwork for future work in this area.
Every partial algebra is the colimit of its total subalgebras. We prove this result for partial Boolean algebras (including orthomodular lattices) and the new notion of partial C*-algebras (including noncommutative C*-algebras), and variations such as partial complete Boolean algebras and partial AW*-algebras. The first two results are related by taking projections. As corollaries we find extensions of Stone duality and Gelfand duality. Finally, we investigate the extent to which the Bohrification construction, that works on partial C*-algebras, is functorial.
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 projective sets has been discussed as an additional axiom taken from the interpretation of CZF in Martin-Loef's intuitionistic type theory. On the other hand, every non-empty set is injective in classical ZF, which argument fails to work in CZF. The aim of this paper is to shed some light on the problem whether there are (enough) injective sets in CZF. We show that no two element set is injective unless the law of excluded middle is admitted for negated formulas, and that the axiom of power set is required for proving that there are strongly enough injective sets. The latter notion is abstracted from the singleton embedding into the power set, which ensures enough injectives both in every topos and in IZF. We further show that it is consistent with CZF to assume that the only injective sets are the singletons. In particular, assuming the consistency of CZF one cannot prove in CZF that there are enough injective sets. As a complement we revisit the duality between injective and projective sets from the point of view of intuitionistic type theory.
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 Baire space, by constructing sheaf models and using their preservation properties.
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 categorical logic. The key notion is that of a "predicative category with small maps" which axiomatises the idea of a category of classes and class morphisms, together with a selected class of maps whose fibres are sets (in some axiomatic set theory). The main result of the present paper is that such predicative categories with small maps are stable under internal sheaves. We discuss the sheaf models of constructive set theory this leads to, as well as ideas for future work.
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 so building on earlier work of Awodey and Warren, which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorisation system in the sense of Bousfield--Quillen. It turns out that this is not quite enough for a sound model, due to some subtle coherence issues concerned with stability under substitution; and so our first task is to introduce a slightly richer structure---which we call a homotopy-theoretic model of identity types---and to prove that this is sufficient for a sound interpretation. Now, although both Top and SSet are categories endowed with a weak factorisation system---and indeed, an entire Quillen model structure---exhibiting the additional structure required for a homotopy-theoretic model is quite hard to do. However, the categories we are interested in share a number of common features, and abstracting away from these leads us to introduce the notion of a path object category. This is a relatively simple axiomatic framework, which is nonetheless sufficiently strong to allow the construction of homotopy-theoretic models. Now by exhibiting suitable path object structures on Top and SSet, we endow those categories with the structure of a homotopy-theoretic model: and in this way, obtain the desired topological and simplicial models of identity types.