Related papers: The Axiom of Multiple Choice and Models for Constr…
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…
In "Extensional realizability for intuitionistic set theory", we introduced an extensional variant of generic realizability, where realizers act extensionally on realizers, and showed that this form of realizability provides "inner" models…
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…
CZF is a system of set theory which, over classical logic, is equivalent to ZF, while over intuitionistic logic, it has a well-known constructive type-theoretic interpretation. This article introduces a simpler, intuitive family of…
In Feferman's work, explicit mathematics and theories of generalized inductive definitions play a central role. One objective of this article is to describe the connections with Martin-Lof type theory and constructive Zermelo-Fraenkel set…
In generic realizability for set theories, realizers treat unbounded quantifiers generically. To this form of realizability, we add another layer of extensionality by requiring that realizers ought to act extensionally on realizers, giving…
Choice and independence of premise principles play an important role in characterizing Kreisel's modified realizability and G\"odel's Dialectica interpretation. In this paper we show that a great many intuitionistic set theories are closed…
Rathjen proved that Aczel's constructive set theory $\mathbf{CZF}$ extended with inaccessible sets of all transfinite orders can be interpreted in Martin-L\"{o}f type theory $\mathbf{MLTT}$ extended with Setzer's Mahlo universe and another…
In [G. Curi, "Exact approximations to Stone-Cech compactification'', Ann. Pure Appl. Logic, 146, 2-3, 2007, pp. 103-123] a characterization is obtained of the locales of which the Stone-Cech compactification can be defined in constructive…
A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset. In this work we will investigate the notion of iterative…
In this paper we consider the problem of building rich categories of setoids, in standard intensional Martin-L\"of type theory (MLTT), and in particular how to handle the problem of equality on objects in this context. Any…
This paper introduces an alternative approach to proving the existence of choice functions for specific families of sets within Zermelo-Fraenkel set theory (ZF) without assuming any form on the Axiom of Choice (AC). Traditional methods of…
We work in set-theory without choice ZF. Denoting by AC(N) the countable axiom of choice, we show in ZF+AC(N) that the closed unit ball of a uniformly convex Banach space is compact in the convex topology (an alternative to the weak…
A special final coalgebra theorem, in the style of Aczel's, is proved within standard Zermelo-Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions.…
Independence of premise principles play an important role in characterizing the modified realizability and the Dialectica interpretations. In this paper we show that a great many intuitionistic set theories are closed under the…
Motivated by problems involving end extensions of models of set theory, we develop the rudiments of the power admissible cover construction (over ill-founded models of set theory), an extension of the machinery of admissible covers invented…
We present a Kleene realizability semantics for the intensional level of the Minimalist Foundation, for short mtt, extended with inductively generated formal topologies, Church's thesis and axiom of choice. This semantics is an extension of…
Whilst Power Kripke-Platek set theory, KPP, shares many properties with ordinary Kripke-Platek set theory, KP, in several ways it behaves quite differently from KP. This is perhaps most strikingly demonstrated by a result, due to Mathias,…
We survey the logical structure of constructive set theories and point towards directions for future research. Moreover, we analyse the consequences of being extensible for the logical structure of a given constructive set theory. We…
We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel's…