Intuitionistic Set Theory J o h n L. Bell Studies in Logic Volume 50 Intuitionistic Set Theory Volume 39 Non-contradiction Lawrence H. Powers, with a Foreword by Hans V. Hansen Volume 40 The Lambda Calculus. Its Syntax and Semantics Henk P. Barendregt Volume 41 Symbolic Logic from Leibniz to Husserl Abel Lassalle Casanave, ed. Volume 42 Meta-argumentation. An Approach to Logic and Argumentation Theory Maurice A. Finocchiaro Volume 43 Logic, Truth and Inquiry Mark Weinstein Volume 44 Meta-logical Investigations in Argumentation Networks Dov M. Gabbay Volume 45 Errors of Reasoning. Naturalizing the Logic of Inference John Woods Volume 46 Questions, Inferences, and Scenarios Andrzej Wisniewski Volume 47 Logic Across the University: Foundations and Applications. Proceedings of the Tsinghua Logic Conference, Beijing, 2013 Johan van Benthem and Fenrong Liu, eds. Volume 48 Trends in Belief Revision and Argumentation Dynamics Eduardo L. Ferme, Dov M. Gabbay, and Guillermo R. Simari Volume 49 Introduction to Propositional Satisfiability Victor Marek Volume 50 Intuitionistic Set Theory John L. Bell Studies in Logic Series Editor Dov Gabbay [email protected] Intuitionistic Set Theory John L. Bell © Individual author and College Publications 2014. All rights reserved. ISBN 978-1-84890-140-7 College Publications Scientific Director: Dov Gabbay Managing Director: Jane Spurr http://www.collegepublications.co.uk Original cover design by Orchid Creative www.orchidcreative.co.uk Printed by Lightning Source, Milton Keynes, UK All rights reserved. No part of this publication may be reproduced, stored in a retrieval system or transmitted in any form, or by any means, electronic, mechanical, photocopying, recording or otherwise without prior permission, in writing, from the publisher. To Sandra, who has given me new life Table of Contents Introduction 1 The natural numbers and countability 1 Power sets 4 The Continuum 6 Chapter I. Intuitionistic Zermelo Set Theory 11 Axioms and basic definitions 11 Logical principles in IZ 15 The axiom of choice 18 Chapter II. Natural Numbers and Finite Sets 25 The natural numbers 25 Models of Peano's axioms 27 Definitions by recursion 28 Finite sets 33 Frege’s construction of the natural numbers 37 Chapter III. The Real Numbers 45 Dedekind real numbers and weak real numbers 45 Cauchy real numbers 49 Chapter IV. Intuitionistic Zermelo-Fraenkel Set Theory and Frame-Valued Models 51 Intuitionistic Zermelo-Fraenkel set theory IZF 51 Frame-valued models of IZF developed in IZF 54 The consistency of ZF and ZFC relative to IZF 65 Frame-valued models of IZF developed in ZFC 66 A frame-valued model in which NN is subcountable 71 The axiom of choice in frame-valued extensions 76 Real numbers and real functions in spatial extensions 77 Properties of the set of real numbers over R 84 Properties of the set of real numbers over Baire space 85 The independence of the fundamental theorem of algebra from IZF 88 Appendix. Heyting Algebras and Frames 91 Lattices 91 Heyting and Boolean algebras 93 Coverages on partially ordered sets and their associated frames 97 Connections with logic 98 Concluding Observations 103 Historical Notes 105 Bibliography 107 Index 111 Preface While intuitionistic (or constructive) set theory 1ST has received a certain attention from mathematical logicians, so far as I am aware no book providing a systematic introduction to the subject has yet been published. This may be the case in part because, as a form of higher-order intuitionistic logic - the internal logic of a topos - 1ST has been chiefly developed in a tops-theoretic context. In particular, proofs of relative consistency with 1ST for mathematical assertions have been (implicitly) formulated in topos- or sheaf-theoretic terms, rather than in the framework of Heyting-algebra-valued models, the natural extension to 1ST of the well-known Boolean-valued models for classical set theory. In this book I offer a brief but systematic introduction to 1ST which develops the subject up to and including the use of Heyting-algebra-valued models in relative consistency proofs. I believe that 1ST, presented as it is in the familiar language of set theory, will appeal particularly to those logicians, mathematicians and philosophers who are unacquainted with the methods of topos theory. The title I originally had in mind for this book was Constructive Set Theory. Then it occurred to me that the term “constructive” has come to connote not merely the use of intuitionistic logic, , but also the avoidance of impredicative definitions. This is the case, for example, with Aczel’s Constructive Set Theory in which the power set axiom (which permits impredicative definirions of sets) is not postulated. Since the power set axiom and impredicative definitions are very much a part of 1ST, to avoid confusion I have decided (with some reluctance) to give the book its present title. JLB January 2014