This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice. This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued (...) today is predicativistic constructivism based on Martin-Löf type theory. Associated philosophical foundations are meaning theories in the tradition of Wittgenstein, Dummett, Prawitz and Martin-Löf. What is the relation between proof-theoretical semantics in the tradition of Gentzen, Prawitz, and Martin-Löf and Wittgensteinian or other accounts of meaning-as-use? What can proof-theoretical analyses tell us about the scope and limits of constructive and predicative mathematics? (shrink)

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 presents several independence results concerning the topos-valid and the intuitionistic predicative theory of locales. In particular, certain consequences of the consistency of a general form of Troelstra's uniformity principle with constructive set theory and type theory are examined.

In this paper a method to construct Kripke models for subtheories of constructive set theory is introduced that uses constructions from classical model theory such as constructible sets and generic extensions. Under the main construction all axioms except the collection axioms can be shown to hold in the constructed Kripke model. It is shown that by carefully choosing the classical models various instances of the collection axioms, such as exponentiation, can be forced to hold as well. The paper does not (...) contain any deep results. It consists of first observations on the subject, and is meant to introduce some notions that could serve as a foundation for further research. (shrink)

In intuitionistic generalized predicative systems as constructive set theory, or constructive type theory, two categories have been proposed to play the role of the category of locales: the category FSp of formal spaces, and its full subcategory FSpi of inductively generated formal spaces. Considered in impredicative systems as the intuitionistic set theory IZF, FSp and FSpi are both equivalent to the category of locales. However, in the mentioned predicative systems, FSp fails to be closed under basic constructions such as that (...) of finite products, while FSpi is complete , but does not contain some naturally occurring classes of formal spaces. Moreover, completeness of FSpi only holds under the assumption of strong principles for the existence of inductively defined sets.In this paper, working in the context of constructive set theory, the category ImLoc of imaginary locales is introduced. ImLoc is complete already over weak formulations of constructive set theory, contains FSp and FSpi as full subcategories, and, as FSp and FSpi, is equivalent to the category of locales in IZF.Applications of the concept of imaginary locale to a proof of a point-free version of Tychonoff embedding theorem, and to set-representation theorems, are then presented. (shrink)