Proof and Computation: Digitization in Mathematics, Computer Science, and Philosophy

Contents
Preface
1. Proof and Computation
	1. Introduction
	2. Basics of Computability
	3. Hierarchies of Computability
	4. Constructive Ordinal Proof Theory
	5. Computability in Higher Types
	6. Intuitionistic Mathematics and Human Creativity
	7. Constructive Proof Mining
	8. Constructive Reverse Mathematics
	9. Analog Computability and Real Analysis
	10. Perspectives of Proof and Computation for Mathematics, Computer Science and Philosophy
	References
2. Constructive Convex Programming
	1. Introduction
	2. Bishop-style constructive mathematics
	3. Convexity and constructive infima
	4. The fundamental theorem of asset pricing
	5. Brouwer’s fan theorem and convexity
	Acknowledgements
	References
3. Exploring Predicativity
	1. Introduction
	2. The emergence of predicativity
		2.1. Circularity and Russell’s VCP
		2.2. Characterising predicativity
			2.2.1. Examples
	3. Shedding light on predicativity: Russell’s ramified type theory and Weyl’s “Das Kontinuum”
		3.1. Russell's type theory
		3.2. Weyl’s “Das Kontinuum”
	4. The re-emergence of predicativity
		4.1. A new stage for predicativity
	5. Plurality
	6. Conclusion
	Acknowledgements
	References
4. Constructive Functional Analysis: An Introduction
	1. Introduction
	2. Intuitionistic logic
		2.1. The BHK-interpretation
		2.2. Minimal, intuitionistic and classical logic
	3. Constructive set theory
		3.1. The constructive set theory CZF
		3.2. Omniscience principles
	4. Real numbers
		4.1. Cauchy reals
		4.2. Completeness and total boundedness
	5. Metric spaces
		5.1. Fundamental definitions
		5.2. Complete and compact metric spaces
		5.3. Continuity properties
	6. Normed spaces
		6.1. Normed and Banach spaces
		6.2. Bounded and normable linear mappings
		6.3. Finite-dimensional normed spaces
		6.4. Uniformly convex spaces
		6.5. Hilbert spaces
	7. Convexity
		7.1. Minkowski functionals
		7.2. The Hahn-Banach theorem
	8. Completeness
		8.1. The Banach-Steinhaus theorem
		8.2. The open mapping theorem and the closed graph theorem
	9. Adjoint and compact operators
		9.1. Adjoint operators
		9.2. Compact operators
	Acknowledgments
	References
5. Program Extraction
	1. Introduction
	2. Realizability logic TCF
		2.1. Terms
		2.2. Formulas
		2.3. Derivation
		2.4. Realizability
	3. Case studies
		3.1. Even and odd numbers
		3.2. Parsing
		3.3. Approximate splitting property of real numbers
	4. Notes
		4.1. Logic for program extraction
		4.2. Active research topics
		4.3. Proof assistants
	Acknowledgments
	References
6. The Data Structures of the Lambda Terms
	1. Introduction
	2. Church’s syntax
		2.1. An alternative definition of Λ
		2.2. The set Λ0 of closed terms
	3. From Church’s syntax to de Bruin notation
	4. de Bruijn algebra
		4.1. Extended de Bruijn notation
		4.2. Datatype D and de Bruijn algebra D
	5. Extension of Church’s syntax
		5.1. Datatype of extended Church’s syntax and Church algebra
		5.2. Further extension of Church’s syntax
	6. Datatype L of combinatory λ-terms
	7. Conclusion
	Acknowledgements
	References
7. Provable (and Unprovable) Computability
	1. The Computable Hierarchy
		1.1. Goodstein Sequences and the Hardy Hierarchy H
	2. “Input-Output” Arithmetics
		2.1. Working in EA(I;O)
		2.2. Provably Computable Functions in EA(I;O)
		2.3. Peano Arithmetic — by adding an Inductive Definition
		2.4. Unravelling the LFP-Axiom by Buchholz’ Ω-Rule
		2.5. Cut Elimination and Collapsing in ID1(I;O)∞
		2.6. ID2(I;O) and ID2(I;O)∞
		2.7. Generalizing to ID<ω
	3. Friedman’s Independence Result for Π11−CA0: Kruskal’s Theorem for Labelled Trees
		3.1. The Computation Sequence for τn
		3.2. Recall the Slow Growing Hierarchy Gα(n)
	References
8. Introduction to Minlog
	1. Fundamental Commands in Minlog
		1.1. Declaration of Predicate Variables
		1.2. First Proof
		1.3. Representation of Proofs
		1.4. Saving Theorems
		1.5. Display Settings
		1.6. Loading External Files
		1.7. Proofs in Predicate Logic
		1.8. use-with
		1.9. inst-with
		1.10. assert and cut
		1.11. Proof Search
		1.12. Cheating in Minlog
		1.13. Searching in Minlog
	2. Algebras and Inducively Defined Predicates
		2.1. Algebras
		2.2. Declaration of Term Variables
		2.3. Inductively Defined Predicates
		2.4. Proofs with Inductively Defined Predicates
	3. Decorations
		3.1. Non-computational Universal Quantifier
		3.2. Non-computational Implication
		3.3. Decorated Predicates
		3.4. Leibniz Equality and Simplification
		3.5. Examples of Inductively Defined Predicates
	4. Terms
		4.1. define Command
		4.2. Program Constants
		4.3. Examples of Program Constants
		4.4. Abstraction and Application
		4.5. Boolean Terms as Formulas
		4.6. Normalisation
		4.7. The Extracted Term
	5. Totality
		5.1. Implementation of Totality
		5.2. Implicit Representation of Totality
		5.3. Totality of Program Constants
		5.4. Totality of Boolean Terms
		5.5. Induction
		5.6. Case Distinction
	Acknowledgements
	References
List of Contributors