Handbook of Constructive Mathematics

Description

Constructive mathematics – mathematics in which 'there exists' always means 'we can construct' – is enjoying a renaissance. fifty years on from Bishop's groundbreaking account of constructive analysis, constructive mathematics has spread out to touch almost all areas of mathematics and to have profound influence in theoretical computer science. This handbook gives the most complete overview of modern constructive mathematics, with contributions from leading specialists surveying the subject's myriad aspects. Major themes include: constructive algebra and geometry, constructive analysis, constructive topology, constructive logic and foundations of mathematics, and computational aspects of constructive mathematics. A series of introductory chapters provides graduate students and other newcomers to the subject with foundations for the surveys that follow. Edited by four of the most eminent experts in the field, this is an indispensable reference for constructive mathematicians and a fascinating vista of modern constructivism for the increasing number of researchers interested in constructive approaches. Contents List of Contributors Preface References [10] Part I: Introductory 1. An Introduction to Intuitionistic Logic -- Michael Rathjen 1.1 Introduction 1.2 Constructive Existence 1.3 The Brouwer–Heyting–Kolmogorov Interpretation 1.4 Natural Deductions 1.5 A Hilbert-Style System for Intuitionistic Logic 1.6 Realizability 1.7 The Curry–Howard Correspondence References [27] 2. An Introduction to Constructive Set Theory: An Appetizer -- Michael Rathjen 2.1 Introduction 2.2 The Axiomatic Framework 2.3 Elementary Mathematics in CZF 2.4 The Development of Set Theory in CZF 2.5 Large Sets in CZF 2.6 Axioms of Choice in Constructive Set Theory 2.7 CZF and the Limited Principle of Omniscience 2.8 Models of CZF and Axiomatic Freedom References [5] [21] [39] [56] 3. Bishop’s Mathematics: A Philosophical Perspective -- Laura Crosilla 3.1 Introduction 3.2 Bishop on Brouwer 3.3 Brouwer’s Mathematics 3.4 Persuasion and Dialogue 3.5 Formalisation 3.6 Philosophy 3.7 Traditional Philosophical Arguments for Intuitionistic Logic 3.8 Philosophical Objections 3.9 Too Strong 3.10 Concluding Remarks Acknowledgements References [2] [19] [36] [54] [72] Part II: Algebra and Geometry 4. Algebra in Bishop’s style: A Course in Constructive Algebra -- Henri Lombardi 4.1 Introduction 4.2 Revisiting Bishop’s Set Theory 4.3 The Corpus of Classical Abstract Algebra Treated in the Book 4.4 Principal Ideal Domains 4.5 Factorization Problems 4.6 Noetherian Rings, Primary Decompositions and the Principal Ideal Theorem 4.7 Wedderburn Structure Theorem for Finite-Dimensional k-Algebras 4.8 Dedekind Domains Acknowledgements References [10] 5. Constructive Algebra: The Quillen–Suslin Theorem -- Ihsen Yengui 5.1 Introduction 5.2 Quillen’s Proof of Serre’s Problem 5.3 Suslin’s Proof of Serre’s Problem References [10] [26] [46] 6. Constructive Algebra and Point-Free Topology -- Thierry Coquand 6.1 Introduction 6.2 Zariski Spectrum 6.3 Minimal and Maximal Primes 6.4 Forcing over a Site 6.5 Concluding Remarks References [2] [21] [39] [55] [72] 7. Constructive Projective Geometry -- Mark Mandelkern 7.1 Introduction 7.2 Real Projective Plane 7.3 Projective Extensions References [5] [22] [41] Part III: Analysis 8. Elements of Constructive Analysis -- Hajime Ishihara 8.1 Introduction 8.2 Real Numbers 8.3 Metric Spaces 8.4 Normed Linear Spaces References [9] 9. Constructive Functional Analysis -- Hajime Ishihara 9.1 Introduction 9.2 Preliminaries 9.3 Completeness 9.4 Convexity 9.5 Duality in Hilbert Spaces References [11] [28] 10. Constructive Banach Algebra Theory -- Robin S. Havea and Douglas Bridges 10.1 Introduction 10.2 Preliminaries 10.3 The Spectral Mapping Theorem 10.4 Approximating the State Space 10.5 Hermitian and Positive Elements References [5] 11. Constructive Convex Optimisation -- Josef Berger and Gregor Svindland 11.1 Introduction 11.2 Some Definitions and Notation 11.3 Convexity and Existence of Infima and Minima 11.4 Convexity and Brouwer’s Fan Theorem 11.5 Lemmas of the Alternative and Consequences References 12. Constructive Mathematical Economics by Matthew Hendtlass and Douglas Bridges 12.1 Introduction 12.2 Preference and Utility 12.3 Demand Functions 12.4 Economic Equilibrium 12.5 Game Theory References [10] [29] 13. A Leisurely RandomWalk Down the Lane of a Constructive Theory of Stochastic Processes -- Yuen-Kwok Chan 13.1 Stochastic Process, in a Nutshell 13.2 Constructive Mathematics, in a Nutshell 13.3 Stochastic Processes, in a Bigger Nutshell 13.4 Constructive Theory of Stochastic Processes, in an Even Bigger Nutshell 13.5 Concluding Remarks References [14] Part IV: Topology 14. Bases of Pseudocompact Bishop Spaces -- Iosif Petrakis 14.1 The Problem of Constructivising General Topology 14.2 Overview of Recent Work on Bishop Spaces 14.3 Structure of the Technical Part of this Chapter 14.4 Basic Notions in the Theory of Bishop Spaces 14.5 Bases of Bishop Spaces 14.6 The First Base Theorem 14.7 The Second Base Theorem 14.8 Applications of the Second Base Theorem 14.9 Concluding Remarks Acknowledgements References [17] [38] [57] 15. Bishop Metric Spaces in Formal Topology by Tatsuji Kawai 15.1 Introduction 15.2 Formal Topology 15.3 Functorial Embedding of Locally Compact Metric Spaces 15.4 Located Subsets in Formal Topology 15.5 Pointfree Characterisation of Compact Metric Spaces 15.6 Pointfree Characterisation of Locally Compact Metric Spaces 15.7 Beyond Locally Compact Metric Spaces 15.8 Related Works References [6] [26] 16. Subspaces in Pointfree Topology: Towards a New Approach to Measure Theory -- Francesco Ciraulo 16.1 Introduction 16.2 Pointfree Parts of the Real Line 16.3 A Measure on σ-Sublocales 16.4 The Pointfree Approach to the Real Line 16.5 Concluding Remarks References [13] 17. Synthetic Topology -- Davorin Lešnik 17.1 Introduction 17.2 Topological Properties 17.3 Principles References [10] 18. Apartness on Lattices and Between Sets -- Douglas Bridges 18.1 Introduction 18.2 Lattices 18.3 Apartness on Frames 18.4 Frame Topologies 18.5 Join Homomorphisms and Continuity 18.6 Set–Set Pre-apartness 18.7 Strong and Uniform Continuity 18.8 Compactness 18.9 Concluding Remarks Acknowledgement References [8] Part V: Logic and Foundations 19. Countable Choice by Fred Richman 19.1 Axioms of Choice 19.2 Living without Countable Choice 19.3 The Fundamental Theorem of Algebra 19.4 Completions 19.5 The Ascending Tree Condition 19.6 Bishop’s Principle and the λ-Technique References [2] 20. The Minimalist Foundation and Bishop’s Constructive Mathematics -- Maria Emilia Maietti and Giovanni Sambin 20.1 Introduction 20.2 Why Adopt a Minimalist Foundation? 20.3 The Minimalist Foundation 20.4 Why Adopting the Pointfree Approach to Develop Topology in MF? 20.5 Extending MF with choice principles 20.6 Concluding Remarks Acknowledgements References [5] [20] [36] [51] [68] 21. Identity, Equality, and Extensionality in Explicit Mathematics -- Gerhard Jäger 21.1 Introduction 21.2 The Basic Axiomatic Operational Framework 21.3 Adding Elementary Classes 21.4 About Some Ontological Aspects of EC and EC+ 21.5 Abstract Data Structures 21.6 The Number Systems N, Z, and Q as Abstract Data Structures 21.7 Representing the Real Numbers References [6] 22. Inner and Outer Models for Constructive Set Theories -- Robert S. Lubarsky 22.1 Introduction 22.2 Heyting Models, or Constructive Forcing 22.3 Kripke Models 22.4 Heyting–Kripke Models 22.5 Classical Outer Models 22.6 Inner Models 22.7 A Final Example References [10] [26] 23. An Introduction to Constructive Reverse Mathematics -- Hajime Ishihara 23.1 Introduction 23.2 A Formal System 23.3 Continuity Properties 23.4 Compactness Properties 23.5 The Monotone Completeness Theorem 23.6 Concluding Remarks References [15] [32] 24. Systems for Constructive Reverse Mathematics -- Takako Nemoto 24.1 Introduction 24.2 Preliminary 24.3 Function-Based Language and Systems 24.4 Base Theory with the Strength of ACA0 24.5 Base Theory with the Strength of RCA0 24.6 Base Theory with the Strength of RCA0 24.7 Appendix: Proof of Lemma 24.27 and Lemma 24.28 References [12] 25. Brouwer’s Fan Theorem -- Josef Berger 25.1 Introduction 25.2 Notation 25.3 The Weak König Lemma 25.4 The Fan Theorem 25.5 The Uniform Continuity Theorem 25.6 The Fan Theorem for c-sets References [4] Part VI: Aspects of Computation 26. Computational Aspects of Bishop’s Constructive Mathematics by Helmut Schwichtenberg 26.1 Partial Continuous Functionals 26.2 A Term Language for Computable Functionals 26.3 A Theory of Computable Functionals 26.4 Computational Content of Proofs 26.5 Applications References [2] 27. Application of Constructive Analysis in Exact Real Arithmetic -- Kenji Miyamoto 27.1 Introduction 27.2 Preliminaries 27.3 Applications 27.4 Concluding Remarks References [16] [33] 28. Efficient Algorithms from Proofs in Constructive Analysis -- Mark Bickford 28.1 Introduction 28.2 Representation of Real Numbers 28.3 Nuprl Representation of Real Numbers 28.4 Some Type Theory 28.5 Extracts of Proofs by Induction 28.6 Inverse, Division, and Computation 28.7 Completeness 28.8 Constructing kth Roots 28.9 Computing Power Series 28.10 sin(x), cos(x), and ex 28.11 ln(x) and arcsin(x) 28.12 Computing π and arctan(x) 28.13 Constructive Content of Brouwer’s Principles 28.14 Concluding Remarks 29. On the Computational Content of Choice Principles -- Ulrich Berger and Monika Seisenberger 29.1 Introduction 29.2 A Semi-constructive System with Computational Content 29.3 Realizable and Unrealizable Choice Principles 29.4 Countable Choice and Classical Logic 29.5 Conclusion References [8] [24] [43] Index a b c de f ghi jkl m nop qr s t uvw yz