Proof and Computation

Digitization in Mathematics, Computer Science and Philosophy

Klaus Mainzer, Peter Schuster, Helmut Schwichtenberg

• Publisher: WSPC
• Year: 2018
• ISBN:
  9789813270954
• Topic: Matemáticas
• Subtopic: Lógica en matemáticas

-->

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:

• Proof and Computation (K Mainzer)
• Constructive Convex Programming (J Berger and G Svindland)
• Exploring Predicativity (L Crosilla)
• Constructive Functional Analysis: An Introduction (H Ishihara)
• Program Extraction (K Miyamoto)
• The Data Structures of the Lambda Terms (M Sato)
• Provable (and Unprovable) Computability (S Wainer)
• Introduction to Minlog (F Wiesnet)

--> -->
Readership: Graduate students, researchers, and professionals in Mathematics and Computer Science.
-->Keywords:Proof Theory;Computability Theory;Program Extraction;Constructive Analysis;PredicativityReview: Key Features:

• This book gathers recent contributions of distinguished experts
• It makes emerging fields accessible to a wider audience, appealing to a broad readership with diverse backgrounds
• It fills a gap between (under-)graduate level textbooks and state-of-the-art research papers

Chapter 1

Proof and Computation

Perspectives beyond Turing Computability

Klaus Mainzer

Lehrstuhl für Philosophie und Wissenschaftstheorie
Technische Universität München (TUM)
Arcisstraße 21, 80333 München, Germany
[email protected]

Contents

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

1.Introduction

From a digital point of view, constructive proofs should be realized by digital systems. If mathematics is restricted to computable functions of natural numbers, Turing machines will do the job. But, in higher mathematics and physics (e.g., functional analysis), we have to consider functionals and spaces of higher types. Therefore, a general concept of a digital information system is necessary to compute finite approximations of functionals of higher types. Contrary to the machine-orientation of computational mathematics, intuitionistic mathematics is rooted in the philosophy of human creativity. Mathematics is understood as a human activity of constructing and proving step-by-step. In the rigorous sense of Brouwer’s intuitionism, we even get a concept of real continuum and infinity which differs from the ordinary understanding of these concepts in classical mathematics. In the foundational research programs of proof mining and reverse mathematics, we offer degrees of constructivity and provability to classify problem solving and axiomatic strength for different mathematical applications.

Proof mining aims to extract effective procedures by purely logical analyses of mathematical proofs and principles [52]. Sometimes it is even sufficient to find bounds for search procedures of problem solving. At least, proof mining tells us how far away a proof is from being constructive. The research program of proof mining goes back to Georg Kreisel’s proof-theoretic research. He illustrates the extraction of effective procedures from proofs as “unwinding proofs” [25].

From a theoretical point of view, proof mining is an important link between logic, mathematics, and computer science. Logic is no longer only a formal activity beside and separated from mathematics. Actually, metatheorems of proof mining deliver logical tools to solve mathematical problems more effectively and to obtain new mathematical information: Proofs are more than verifications of theorems!

From a practical point of view, proof theory also has practical consequences in applied computer science. In this case, instead of formal theories and proofs, we consider formal models and computer programs of processes, e.g., in industry. Formal derivations of formulas correspond to, e.g., steps of industrial production. In order to avoid additional costs of mistakes and biases, we should test and prove that computer programs are correct and sound before applying them. Automated theorem proving is applied to integrated design and verification. Software and hardware design must be verified to prevent costly and life threatening errors. Dangerous examples in the past were flaws in the microchips of space rockets and medical equipment. Network security of the Internet is a challenge for banks, governments, and commercial organizations. In the age of Big Data and increasing complexity of our living conditions, rigorous proofs and tests are urgently demanded to avoid a dangerous future with overwhelming computational power running out of control.

But, in real mathematics, proofs cannot all be reduced to effective procedures. Actually, there are degrees of constructivity, computability, and provability. How strong must a theory be in order to prove a certain theorem? We try to determine which axioms are required to prove a theorem. How constructive and computational are these assumptions?

Instead of going forward from axioms to the theorems in usual proofs, we prove in the reverse way (backward) from a given theorem to the assumed axioms. Therefore, this research program is called reverse mathematics [29]. If an axiom system S proves a theorem T and theorem T together with an axiom system S′ (the reversal) prove axiom system S, then S is called equivalent to theorem T over S′. In order to determine the degrees of constructivity and computability, one tries to characterize mathematical theorems by equivalent subsystems of arithmetic. The formulas of these arithmetical subsystems can be distinguished by different degrees of complexity.

In (second-order) arithmetic, all objects are represented as natural numbers or sets of natural numbers. Therefore, proofs about real numbers must use Cauchy sequences of rational numbers, which can be represented as sets of natural numbers. In reverse mathematics, theorems and principles of real mathematics are characterized by equivalent subsystems of arithmetic with different degrees of constructivity and computability [45]. Some of them are computable in Turing’s sense, but others are definitely not and need stronger tools beyond Turing-computability. Therefore, it is proved that only parts of real mathematics can be reduced to the digital paradigm. Reverse mathematics and proof mining are important research programs aiming to connect mathematics, computer science, and logic in a rigorous way.

Philosophically, reverse mathematics and proof mining are deeply rooted in the epistemic tradition of efficient reasoning with the principle of parsimony in explanations, proofs, and theories. It was the medieval logician and philosopher William of Ockham (1285–1347) who first demanded that one should prefer explanations and proofs with the fewest number of assumed abstract concepts and principles. The reason is that, according to Ockham, universals (e.g., mathematical sets) are only abstractions from individuals (the elements of a set) without real existence. Ockham’s principle of parsimony became later popular as “Ockham’s razor” which should reduce abstract principles as far as possible.

The question arises of how far reduction is possible without loss of essential information. In order to analyze real computation in mathematics, we need an extension of digital computability beyond Turing-computability. Real computing machines can be considered idealized analog computers accepting real numbers as given infinite entities [8]. They are not only theoretically interesting but also practically inspiring with respect to their applications in scientific computing and technology (e.g., sensor technology) [62].

2.Basics of Computability

The early historical roots of computer science ...