Book contents
- Frontmatter
- Preface
- Contents
- Possible m-diagrams ofmodels of arithmetic
- Weak theories of nonstandard arithmetic and analysis
- Notions of compactness in weak subsystems of second order arithmetic
- Proof-theoretic strength of the stable marriage theorem and other problems
- Free sets and reversemathematics
- Interpreting arithmetic in the r.e. degrees under Σ4-induction
- Reverse mathematics, Archimedean classes, and Hahn's Theorem
- The Baire category theoremover a feasible base theory
- Basic applications of weak König's lemma in feasible analysis
- Maximal nonfinitely generated subalgebras
- Metamathematics of comparability
- A note on compactness of countable sets
- A survey of the reversemathematics of ordinal arithmetic
- Reversemathematics and ordinal suprema
- Did Cantor need set theory?
- Models of arithmetic: quantifiers and complexity
- Higher order reversemathematics
- Arithmetic saturation
- WQO and BQO theory in subsystems of second order arithmetic
- Reverse mathematics and graph coloring: eliminating diagonalization
- Undecidable theories and reversemathematics
- Π01 sets and models of WKL0
- Manipulating the reals in RCA0
- Reverse mathematics and weak systems of 0-1 strings for feasible analysis
- References
Weak theories of nonstandard arithmetic and analysis
Published online by Cambridge University Press: 31 March 2017
- Frontmatter
- Preface
- Contents
- Possible m-diagrams ofmodels of arithmetic
- Weak theories of nonstandard arithmetic and analysis
- Notions of compactness in weak subsystems of second order arithmetic
- Proof-theoretic strength of the stable marriage theorem and other problems
- Free sets and reversemathematics
- Interpreting arithmetic in the r.e. degrees under Σ4-induction
- Reverse mathematics, Archimedean classes, and Hahn's Theorem
- The Baire category theoremover a feasible base theory
- Basic applications of weak König's lemma in feasible analysis
- Maximal nonfinitely generated subalgebras
- Metamathematics of comparability
- A note on compactness of countable sets
- A survey of the reversemathematics of ordinal arithmetic
- Reversemathematics and ordinal suprema
- Did Cantor need set theory?
- Models of arithmetic: quantifiers and complexity
- Higher order reversemathematics
- Arithmetic saturation
- WQO and BQO theory in subsystems of second order arithmetic
- Reverse mathematics and graph coloring: eliminating diagonalization
- Undecidable theories and reversemathematics
- Π01 sets and models of WKL0
- Manipulating the reals in RCA0
- Reverse mathematics and weak systems of 0-1 strings for feasible analysis
- References
Summary
Abstract. A general method of interpreting weak higher-type theories of nonstandard arithmetic in their standard counterparts is presented. In particular, this provides natural nonstandard conservative extensions of primitive recursive arithmetic, elementary recursive arithmetic, and polynomial-time computable arithmetic. A means of formalizing basic real analysis in such theories is sketched.
Introduction. Nonstandard analysis, as developed by Abraham Robinson, provides an elegant paradigm for the application of metamathematical ideas in mathematics. The idea is simple: use model-theoretic methods to build rich extensions of a mathematical structure, like second-order arithmetic or a universe of sets; reason about what is true in these enriched structures; and then transfer the results back to the ordinary mathematical universe. Robinson showed that this allows one, for example, to provide a coherent and consistent development of calculus based on the use of infinitesimals.
From a foundational point of view, it is natural to try to axiomatize such nonstandard structures. By formalizing the model-theoretic arguments, one can, in general, embed standard mathematical theories is conservative, nonstandard extensions. This was done e.g. by Kreisel, for second-order arithmetic [31]; Friedman, for first-order Peano arithmetic (unpublished); Nelson, for set theory [33]; and Moerdijk and Palmgren for intuitionistic first-order Heyting arithmetic [32] (see also [7]).
In recent years there has also been an interest in formalizing parts of mathematics in weak theories, at the level of primitive recursive arithmetic (PRA), or below. The underlying motivations vary. One may be drawn by the general philosophical goal of minimizing ontological commitments, or, less ethereally, by the sport of seeing how little one can get away with. Alternatively, one may be interested in extracting additional mathematical information from standard mathematical developments (e.g. [26, 27, 29, 30]), or narrowing the theoretical gap between abstract mathematics and concrete computation. In any event, a number of appropriate formal frameworks have been developed, including subsystems of first- and second-order arithmetic (e.g. [10, 37, 17, 19, 18, 49]), theories of finite types (e.g. [28, 30]), and versions of Feferman's theories of explicit mathematics (e.g. [41]), to name just a few.
- Type
- Chapter
- Information
- Reverse Mathematics 2001 , pp. 19 - 46Publisher: Cambridge University PressPrint publication year: 2005
References
- 1
- Cited by