Handbook of Constructive Mathematics

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