Fefermans argument is indeed convincing in a certain context, it can be dissolved entirely by modifying the context appropriately.

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 (...) maps and show that it provides a sound and complete semantics for constructive set theories like IZF and CZF. The main technical contribution of this paper is that it shows in detail that such categories can always be conservatively embedded in categories that are exact. These exactness properties play a crucial rôle in showing that predicative categories with small maps contain models of set theory and that they are closed under sheaves and realizability. We will prove the former statement in this paper as well, leaving a proof of the closure properties to the papers on realizability and sheaves as mentioned above. (shrink)

This paper introduces Basic Intuitionistic Set Theory BIST, and investigates it as a first-order set theory extending the internal logic of elementary toposes. Given an elementary topos, together with the extra structure of a directed structural system of inclusions on the topos, a forcing-style interpretation of the language of first-order set theory in the topos is given, which conservatively extends the internal logic of the topos. This forcing interpretation applies to an arbitrary elementary topos, since any such is equivalent to (...) one carrying a dssi. We prove that the set theory BIST+Coll is sound and complete relative to forcing interpretations in toposes with natural numbers object. Furthermore, in the case that the structural system of inclusions is superdirected, the full Separation schema is modelled. We show that all cocomplete and realizability toposes can be endowed with such superdirected systems of inclusions.A large part of the paper is devoted to an alternative notion of category-theoretic model for BIST, which, following the general approach of Joyal and Moerdijkʼs Algebraic Set Theory, axiomatizes the structure possessed by categories of classes compatible with BIST. We prove soundness and completeness results for BIST relative to the class-category semantics. Furthermore, BIST+Coll is complete relative to the restricted collection of categories of classes given by categories of ideals over elementary toposes with nno and dssi. It is via this result that the completeness of the original forcing interpretation is obtained, since the internal logic of categories of ideals coincides with the forcing interpretation. (shrink)

In this paper we define a notion of relativization for higher order logic. We then show that there is a higher order theory of Grothendieck topoi such that all Grothendieck topoi relativizes to all models of set theory with choice.

By obtaining several new results on Cook-style two-sorted bounded arithmetic, this paper measures the strengths of the axiom of extensionality and of other weak fundamental set-theoretic axioms in the absence of the axiom of infinity, following the author’s previous work [K. Sato, The strength of extensionality I — weak weak set theories with infinity, Annals of Pure and Applied Logic 157 234–268] which measures them in the presence. These investigations provide a uniform framework in which three different kinds of reverse (...) mathematics–Friedman–Simpson’s “orthodox” reverse mathematics, Cook’s bounded reverse mathematics and large cardinal theory–can be reformulated within one language so that we can compare them more directly. (shrink)