Book contents
- Frontmatter
- Introduction
- Contents
- K. Jon Barwise (1942-2000)
- TUTORIALS
- PHOTOGRAPHS
- ARTICLES
- Bounded forcing axioms and the size of the continuum
- Hilbert's wide program
- Rigidity conjectures
- Metapredicative and explicit Mahlo: a proof-theoretic perspective
- A two-dimensional tree ideal
- Psychology looks hopefully to logic
- Russell's logics
- Partitioning pairs of uncountable sets
- Aspects of the Turing jump
- Liouville functions
- References
Metapredicative and explicit Mahlo: a proof-theoretic perspective
from ARTICLES
Published online by Cambridge University Press: 27 June 2017
- Frontmatter
- Introduction
- Contents
- K. Jon Barwise (1942-2000)
- TUTORIALS
- PHOTOGRAPHS
- ARTICLES
- Bounded forcing axioms and the size of the continuum
- Hilbert's wide program
- Rigidity conjectures
- Metapredicative and explicit Mahlo: a proof-theoretic perspective
- A two-dimensional tree ideal
- Psychology looks hopefully to logic
- Russell's logics
- Partitioning pairs of uncountable sets
- Aspects of the Turing jump
- Liouville functions
- References
Summary
Abstract. After briefly discussing the concepts of predicativity, metapredicativity and impredicativity, we turn to the notion of Mahloness as it is treated in various contexts. Afterwards the appropriate Mahlo axioms for the framework of explicit mathematics are presented. The article concludes with relating explicit Mahlo to certain nonmonotone inductive definitions.
Introduction. More than 100 years ago Cantor developed the theory of infinite sets (Cantor's paradise). Shortly afterwards,Russell found his famous paradox, and, as a consequence,manymathematicians became very concerned about the foundations of mathematics, and the expression foundational crisis was coined.
To overcome this crisis, Hilbert proposed the program of Beweistheorie as a method of rescuing Cantor's paradise. A few years later, however, Gödel showed that Hilbert's program—at least in its original strong form—cannot work. Again, after only a short while a first new idea was brought in by Gentzen, and a break-through along these lines was obtained by his prooftheoretic analysis of first order arithmetic. Then, during the last decades, Gentzen's work has been extended to stronger and stronger subsystems of second order arithmetic and set theory, most prominently by the schools of Schütte and Takeuti, leading to what today is denoted as infinitary and finitary proof theory, respectively.
A position completely different from Hilbert's was taken by Brouwer who advocated the restriction of mathematics to those principles which could be justified on constructive grounds. Starting off from his pioneering work various “dialects” of constructive mathematics have been put forward (e.g., in the Netherlands directly following Brouwer and Heyting, the Russian form(s) of constructivism, Bishop's approach, Martin-Löf type theory, Feferman's explicit mathematics).
In a certain sense the research directions originating from Hilbert's and Brouwer's original ideas come together again under the heading of reductive proof theory which tries to justify classical theories and classical principles by reducing them to a (more) constructive framework. For further reading and detailed information about this topic we refer, for example, to Beeson [6], Feferman [17] and Troelstra and van Dalen [61].
- Type
- Chapter
- Information
- Logic Colloquium 2000 , pp. 272 - 293Publisher: Cambridge University PressPrint publication year: 2005
References
- 3
- Cited by