Table of Contents

One. Practice and Philosophy of Constructive Mathematics.- I. Examples of Constructive Mathematics.- 1. The Real Numbers.- 2. Constructive Reasoning.- 3. Order in the Reals.- 4. Subfields of R with Decidable Order.- 5. Functions from Reals to Reals.- 6. Theorem of the Maximum.- 7. Intermediate Value Theorem.- 8. Sets and Metric Spaces.- 9. Compactness.- 10. Ordinary Differential Equations.- 11. Potential Theory.- 12. The Wave Equation.- 13. Measure Theory.- 14. Calculus of Variations.- 15. Plateau's Problem.- 16. Rings, Groups, and Fields.- 17. Linear Algebra.- 18. Approximation Theory.- 19. Algebraic Topology.- 20. Standard Representations of Metric Spaces.- 21. Some Assorted Problems.- II. Informal Foundations of Constructive Mathematics.- 1. Numbers.- 2. Operations or Rules.- 3. Sets and Presets.- 4. Constructive Proofs.- 5. Witnesses and Evidence.- 6. Logic.- 7. Functions.- 8. Axioms of Choice.- 9. Ways of Constructing Sets.- 10. Definite Presets.- III. Some Different Philosophies of Constructive Mathematics.- 1. The Russian Constructivists.- 2. Recursive Analysis.- 3. Bishop's Constructivism.- 4. Objective Intuitionism.- 5. Sets in Intuitionism.- 6. Brouwerian Intuitionism.- 7. Martin-Lof s Philosophy.- 8. Church's Thesis.- IV. Recursive Mathematics: Living with Church's Thesis.- 1. Constructive Recursion Theory.- 2. Diagonalization and "Weak Counterexamples".- 3. Continuity of Effective Operations.- 4. Specker Sequences.- 5. Failure of Konig's Lemma: Kleene's Singular Tree.- 6. Singular Coverings.- 7. Non-Uniformly Continuous Functions.- 8. The Infimum of a Positive Function.- 9. Theorem of the Maximum Revisited.- 10. The Topology of the Disk in Recursive Mathematics.- 11. Pointwise Convergence Versus Uniform Convergence.- 12. Connectivity of Intervals.- 13. Another Surprise in Recursive Topology.- 14. A Counterexample in Descriptive Set Theory.- 15. Differential Equations with no Computable Solutions.- V. The Role of Formal Systems in Foundational Studies.- 1. The Axiomatic Method.- 2. Informal Versus Formal Axiomatics.- 3. Adequacy and Fidelity: Criteria for Formalization.- 4. Constructive and Classical Mathematics Compared.- 5. Arithmetic of Finite Types.- 6. Formalizing Constructive Mathematics in HA?.- Two. Formal Systems of the Seventies.- VI. Theories of Rules.- 1. The Logic of Partial Terms.- 2. Combinatory Algebras.- 3. Axiomatizing Recursive Mathematics.- 4. Term Reduction and the Church-Rosser Theorem Ill.- 5. Combinatory Logic and ?-Calculus.- 6. Term Models.- 7. Continuous Models.- 8. Finite Type Structures and Continuity in Combinatory Algebras.- 9. Set-Theoretic and Topological Models.- 10. Discussion: Adequacy and Fidelity of EON?.- VII. Readability.- 1. Definition and Soundness of Realizability.- 2. Realizability and Models.- 3. Some Simple Applications.- 4. Existence Properties.- 5. q-Realizability.- 6. Rules of Choice.- 7. Discussion: Numerical Meaning.- VIII. Constructive Set Theories.- 1. Intuitionistic Zermelo-Fraenkel Set Theory, IZF.- 2. Non-Extensional Set Theory.- 3. The Double-Negation Interpretation for IZF.- 4. Realizability for Set Theory Without Extensionality.- 5. Realizability and Models.- 6. Realizability for IZF.- 7. Connection with Realizability for Arithmetic.- 8. Consistency of Church's Thesis with IZF.- 9. The Numerical Existence Property for IZF.- 10. Discussion.- 11. The Theory B.- 12. More Discussion.- 13. Intermediate Constructive Set Theories.- IX. The Existence Property in Constructive Set Theory.- 1. Introduction.- 2. The Set Existence Property for HAS.- 3. The Existence Property in Set Theories.- X. Theories of Rules, Sets, and Classes.- 1. The Theory FML.- 2. The Theories EM0 and EM0 +J.- 3. Models of Feferman's Theories.- 4. Realizability.- 5. The Axiom of Choice.- 6. q-Realizability.- 7. Term Existence Property.- 8. Evaluation of Numerical Terms.- 9. Numerical Existence Property.- 10. Decidable Equality.- 11. Extensionality in Feferman's Theories.- 12. Some Remarks on Formalizing Mathematics in FML + DC.- 13. Functions, Operations, and Axioms of Choice.- 14. The Theory SOF (Sets, Operations, Functions).- 15. Some Theorems of SOF.- 16. Realizability for SOF.- 17. Discussion.- XI. Constructive Type Theories.- 1. Forms of Judgment.- 2. Philosophical Remarks on Sets, Categories, and Canonical Elements.- 3. Hypothetical Judgments.- 4. Families of Sets.- 5. Disjoint Union and Existential Quantification.- 6. Abstraction.- 7. Cartesian Product and Conjunction.- 8. The Constant E and Projection Functions.- 9. Product and Universal Quantification.- 10. Implication.- 11. N, Nk, and R.- 12. Disjoint Union.- 13. The I-Rules.- 14. How Martin-Lof's Rules Actually Define a Formal System.- 15. List of Rule Schemata of Martin-Lof's System ML0.- 16. Other Formulations of ML0.- 17. Interpretation of HA? + AC + EXT in ML0.- 18. Formalizing Mathematics in ML0.- 19. Is the Theory HA? + EXT + AC Constructive?.- 20. The Realizability Model of ML0.- 21. Martin-Lof's Universes.- 22. The Arithmetic Theorems of Martin-Lof's Systems, and a New Realizability for Arithmetic.- 23. Discussion.- Three. Metamathematical Studies.- XII. Constructive Models of Set Theory.- 1. Aczel's "Iterative Sets".- 2. Interpreting Subtheories of Intuitionistic ZF in Feferman's Theories.- XIII. Proof-Theoretic Strength.- 1. Definitions About Proof-Theoretic Strength.- 2. ?1/1-AC and ID1-.- 3. The Strength of Feferman's Theory EM0 + J and Related Theories.- 4. The Strength of Constructive Set Theory T2.- 5. The Strength of Martin-Lof's Theories.- 6. Theories with the Strength of Arithmetic.- 7. Conservative Extension Theorems.- XIV. Some Formalized Metamathematics and Church's Rule.- 1. The Theories Tb and Ta.- 2. Formalization of Normal-Term Arguments.- 3. Formalized Models.- 4. Church's Rule.- 5. Truth Definitions and Reflection Principles.- 6. Formalized Realizability and Existence Properties.- 7. Discussion.- XV. Forcing.- 1. Ordinary Forcing.- 2. Conservative Extension Results.- 3. Uniform Forcing.- XVI. Continuity.- 1. Continuity Principles.- 2. Continuity and Church's Thesis.- 3. Consistency of Brouwer's Principle and Uniform Continuity.- 4. Derived Rules Related to Continuity.- Four. Metaphilosophical Studies.- XVII. Theories of Rules and Proofs.- 1. Review of the Relevant Literature.- 2. The Main Issues.- 3. A Theory of Rules and Proofs.- 4. Undecidability of the Proof-Predicate in C.- 5. Consistency of C.- 6. Discussion.- 7. Frege Structures.- 8. Existence of Frege Structures.- 9. Set Theory and Frege Structures.- 10. A Theory of Rules, Proofs, and Sets.- Historical Appendix.- 1. From Gauss to Zermelo: The Origins of Non-Constructive Mathematics.- 2. From Kant to Hilbert: Logic and Philosophy.- 3. Brouwer and the Dutch Intuitionists.- 4. Early Formal Systems for Intuitionism.- 5. Kleene: The Marriage of Recursion Theory and Intuitionism.- 6. The Russian Constructivists and Recursive Analysis.- 7. Model Theory of Intuitionistic Systems.- 8. Logical Studies of Intuitionistic Systems.- 9. Bishop and his Followers.- 10. The Latest Decade.- References.- Index of Axioms, Abbreviations, and Theories.- Index of Names.- Index of Symbols.