Some results in reverse mathematics inspired by proof mining
Sam Sanders (RUB Bochum)
Abstract: The study of (compact) metric spaces in second-order Reverse Mathematics (RM hereafter) is fundamentally based on separability conditions, while the latter are generally avoided in proof mining to enable the extraction of good computational data. Inspired by this observation, we study basic properties of ‘unrepresented’ compact metric spaces in Kohlenbach’s higher-order RM, i.e. we do not assume separability conditions. Our results are four-fold as follows, each building on the next.
Most definitions of compactness yield third-order theorems not provable from second-order comprehension axioms. Only one very specific choice of compactness definitions yields equivalences involving the so-called Big Five of second-order RM.
Many basic properties of compact metric spaces inhabit the range of hyperarithmetical analysis. Until recently, few natural examples of the latter were known.
Some basic properties of compact metric spaces, like the intermediate value theorem, are equivalent to countable choice as studied in higher-order RM, namely QF-AC0,1.
Some basic properties of compact metric spaces, like a continuous function has a supremum and a countable set has measure zero, imply strong axioms including Feferman’s projection principle, full second-order arithmetic, and Kleene’s quantifier (∃3).
In conclusion, the removal of separability conditions from compact metric spaces results in rather interesting phenomena.
logic
Audience: researchers in the topic
Series comments: Description: Seminar on all areas of logic
| Organizer: | Wesley Calvert* |
| *contact for this listing |