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.

We study constructive set theories, which deal with operations applying both to sets and operations themselves. Our starting point is a fully explicit, finitely axiomatized system ESTE of constructive sets and operations, which was shown in 10 to be as strong as PA. In this paper we consider extensions with operations, which internally represent description operators, unbounded set quantifiers and local fixed point operators. We investigate the proof theoretic strength of the resulting systems, which turn out to be impredicative . (...) © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim. (shrink)

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)

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)

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)