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

Description

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. 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