Made with higher types
I have written a book on higher-order Reverse Mathematics, currently under review.
The provisional title is:
Reverse Mathematics: there and back again
with about 450 pages and ample references. The title is explained at the end of this page.
Drop me an email if you are interested! Here is an overview of the chapters:
Chapter A: Introduction
We sketch an overview of the content (see below).
Chapter B: The base theory and around
We introduce the base theory of higher-order arithmetic and develop the RM of discontinuous functions. This development is based solely on the following axiom:
This is just second-order "recursive comprehension" axiom with the usual first-order parameter bumped up to a second-order parameter (the variable f in (B.1) above).
Chapter C: The Biggest Five
We establish many equivalences between:
(a) the second-order Big Five of RM.
(b) third-order theorems of real analysis pertaining to (possibly) discontinuous functions.
We also show that slight variations/generalisations of theorems in (b) cannot be proved from the Big Five (and much stronger systems).
Chapter D: The Bigger Five
We identify four principles that boast many equivalences and deserve the title "Big" system.
i) The uncountability of the reals: there is no injection from the reals to the naturals.
2) The enumeration principle: a countable set of reals can be enumerated.
3) The Baire category theorem for the unit interval.
4) Tao's pigeon hole principle for the Lebesgue measure.
These principles cannot be proved from the Big Five (and much stronger systems).
Chapter E: Hyperarithmetical analysis.
We show that many natural third-order theorems exist in the range of hyperarithmetical analysis. This means that these theorems are sandwiched between conservative extensions of systems of hyperarithmetical analysis. A number of equivalences for countable and dependent choice are obtained.
Chapter F: Towards full second-order arithmetic
We identify a number of natural theorems that imply second-order arithmetic in its various guises, including Feferman's projection principle and Kleene's fourth-order quantifier.
Chapter G: Gems etc in RM
A long list of interesting RM-results that did not fit the previous chapters. This includes the RM of the coding principle open, which expresses that third-order open sets have RM-codes, and a higher-order version of Weihrauch reducibility.
Chapter H: Foundational matters
Chapters A-G are written in a neutral tone with foundational discussion relegated to this chapter. Do let me know what you think, even if you disagree!
Chapter I: Technical Appendix:
A number of important technical results that shore up the previous chapters.
Explanation of the title:
The title "RM: there and back again" refers to going "there", i.e. from second- to third-order arithmetic, and obtaining RM-equivalences in third-order arithmetic. The "back again" refers to a large number of results (usually at the end of each chapter) of the following form:
equivalences between third-order theorems from real analysis can be "pushed down" to equivalences involving second-order systems by restricting the functions to effective versions of Baire 2, measurable, simply continuous, etc.
An example is as follows:
countable choice for quantifier-free formulas (denoted QFAC^{0,1})
is equivalent to the
local equivalence between sequential and ordinary continuity for any function on the reals.
The previous equivalence is third-order in nature, not in the least because ZF cannot prove QFAC^{0,1}. However, the following restriction deals with a second-order system:
the system of hyperarithmetical analysis
is equivalent to the
local equivalence between sequential and ordinary continuity for any effectively Baire 2 functions on the reals.
Here, a function is 'effectively Baire 2' if it is the pointwise limit of a double sequence of continuous functions.
