Foundations of Constructive Mathematics

This book is about some recent work in a subject usually considered part of "logic" and the" foundations of mathematics", but also having close connec­ tions with philosophy and computer science. Namely, the creation and study of "formal systems for constructive mathematics". The general organization of the book is described in the" User's Manual" which follows this introduction, and the contents of the book are described in more detail in the introductions to Part One, Part Two, Part Three, and Part Four. This introduction has a different purpose; it is intended to provide the reader with a general view of the subject. This requires, to begin with, an elucidation of both the concepts mentioned in the phrase, "formal systems for constructive mathematics". "Con­ structive mathematics" refers to mathematics in which, when you prove that l a thing exists (having certain desired properties) you show how to find it. Proof by contradiction is the most common way of proving something exists without showing how to find it - one assumes that nothing exists with the desired properties, and derives a contradiction. It was only in the last two decades of the nineteenth century that mathematicians began to exploit this method of proof in ways that nobody had previously done; that was partly made possible by the creation and development of set theory by Georg Cantor and Richard Dedekind.

Contenu

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-Löf's Rules Actually Define a Formal System.- 15. List of Rule Schemata of Martin-Löf'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-Löf'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-Löf'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, …