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

✍ Scribed by Klaus Mainzer, Peter Schuster, Helmut Schwichtenberg

• Publisher: World Scientific Publishing
• Year: 2018
• Tongue: English
• Leaves: 300
• Category: Library

✦ Synopsis

This book is for graduate students and researchers, introducing modern foundational research in mathematics, computer science, and philosophy from an interdisciplinary point of view. Its scope includes Predicative Foundations, Constructive Mathematics and Type Theory, Computation in Higher Types, Extraction of Programs from Proofs, and Algorithmic Aspects in Financial Mathematics. By filling the gap between (under-)graduate level textbooks and advanced research papers, the book gives a scholarly account of recent developments and emerging branches of the aforementioned fields.

✦ Table of Contents

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