Exploring the abyss in Reverse Mathematics
Sam Sanders (jww Dag Normann)
Department of Philosophy II, RUB Bochum, Germany

CiE 2023, Batumi, Georgia, July 26, 2023

This talk reports on my joint project with Dag Normann (U. of Oslo) on
the Reverse Mathematics of the uncountable (see other talk for . . . ).

This talk reports on my joint project with Dag Normann (U. of Oslo) on
the Reverse Mathematics of the uncountable (see other talk for . . . ).

Firstly, we introduce and greatly extend the Big Five phenomenonof Reverse Mathematics.

This talk reports on my joint project with Dag Normann (U. of Oslo) on
the Reverse Mathematics of the uncountable (see other talk for . . . ).

Firstly, we introduce and greatly extend the Big Five phenomenonof Reverse Mathematics.
Secondly, we discuss the very different logical and mathematicallimits of this extension. (chasm, abyss)

This talk reports on my joint project with Dag Normann (U. of Oslo) on
the Reverse Mathematics of the uncountable (see other talk for . . . ).

Firstly, we introduce and greatly extend the Big Five phenomenonof Reverse Mathematics.
Secondly, we discuss the very different logical and mathematicallimits of this extension. (chasm, abyss)
Thirdly, we may discuss foundational implications, though . . .

Introduction

The Biggest Five of Reverse Mathematics

Reverse Mathematics

The abyss

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Reverse Mathematics= finding the minimal axioms needed to prove a theorem ofordinary mathematics.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Reverse Mathematics= finding the minimal axioms needed to prove a theorem ofordinary mathematics.

Harvey Friedman & Steve Simpson (courtesy of MFO).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Reverse Mathematics= finding the minimal axioms needed to prove a theorem ofordinary mathematics.

Introduction

The Big Five

The Biggest Five of Reverse Mathematics

The abyss

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Big Five
Reverse Mathematics = finding the minimal axioms needed toprove a theorem of ordinary mathematics.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Big Five
Reverse Mathematics = finding the minimal axioms needed toprove a theorem of ordinary mathematics.
One always assume the base theory RCA0 , a weak systemformalising ‘computable mathematics’.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Big Five
Reverse Mathematics = finding the minimal axioms needed toprove a theorem of ordinary mathematics.
One always assume the base theory RCA0 , a weak systemformalising ‘computable mathematics’.
Big Five phenomenon

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Big Five
Reverse Mathematics = finding the minimal axioms needed toprove a theorem of ordinary mathematics.
One always assume the base theory RCA0 , a weak systemformalising ‘computable mathematics’.
Big Five phenomenon=most/many theorems of ordinary mathematics are either provablein RCA0 ,Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Big Five
Reverse Mathematics = finding the minimal axioms needed toprove a theorem of ordinary mathematics.
One always assume the base theory RCA0 , a weak systemformalising ‘computable mathematics’.
Big Five phenomenon=most/many theorems of ordinary mathematics are either provablein RCA0 , or equivalent to one of the other ‘Big Five’ systems:

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Big Five
Reverse Mathematics = finding the minimal axioms needed toprove a theorem of ordinary mathematics.
One always assume the base theory RCA0 , a weak systemformalising ‘computable mathematics’.
Big Five phenomenon=most/many theorems of ordinary mathematics are either provablein RCA0 , or equivalent to one of the other ‘Big Five’ systems:(countable) Heine-Borel compactness: WKL0 ,Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Big Five
Reverse Mathematics = finding the minimal axioms needed toprove a theorem of ordinary mathematics.
One always assume the base theory RCA0 , a weak systemformalising ‘computable mathematics’.
Big Five phenomenon=most/many theorems of ordinary mathematics are either provablein RCA0 , or equivalent to one of the other ‘Big Five’ systems:(countable) Heine-Borel compactness: WKL0 ,Sequential compactness: ACA0 ,Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Big Five
Reverse Mathematics = finding the minimal axioms needed toprove a theorem of ordinary mathematics.
One always assume the base theory RCA0 , a weak systemformalising ‘computable mathematics’.
Big Five phenomenon=most/many theorems of ordinary mathematics are either provablein RCA0 , or equivalent to one of the other ‘Big Five’ systems:(countable) Heine-Borel compactness: WKL0 ,Sequential compactness: ACA0 ,Transfinite recursion: ATR0 ,Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Big Five
Reverse Mathematics = finding the minimal axioms needed toprove a theorem of ordinary mathematics.
One always assume the base theory RCA0 , a weak systemformalising ‘computable mathematics’.
Big Five phenomenon=most/many theorems of ordinary mathematics are either provablein RCA0 , or equivalent to one of the other ‘Big Five’ systems:(countable) Heine-Borel compactness: WKL0 ,Sequential compactness: ACA0 ,Transfinite recursion: ATR0 ,Some descriptive set theory: Π11 -comprehension.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Big Five
Reverse Mathematics = finding the minimal axioms needed toprove a theorem of ordinary mathematics.
One always assume the base theory RCA0 , a weak systemformalising ‘computable mathematics’.
Big Five phenomenon=most/many theorems of ordinary mathematics are either provablein RCA0 , or equivalent to one of the other ‘Big Five’ systems:(countable) Heine-Borel compactness: WKL0 ,Sequential compactness: ACA0 ,Transfinite recursion: ATR0 ,Some descriptive set theory: Π11 -comprehension.
Mummert: a few equivalences for Π12 -comprehension and topology.

Introduction

The Biggest Five of Reverse Mathematics

Higher-order Reverse Mathematics

The abyss

Introduction

The Biggest Five of Reverse Mathematics

Higher-order Reverse Mathematics
Kohlenbach introduces higher-order RM in RM2001.

The abyss

Introduction

The Biggest Five of Reverse Mathematics

Higher-order Reverse Mathematics
Kohlenbach introduces higher-order RM in RM2001.

Second-order RM only has variables n ∈ N and X ⊂ N.

The abyss

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Higher-order Reverse Mathematics
Kohlenbach introduces higher-order RM in RM2001.

Second-order RM only has variables n ∈ N and X ⊂ N. Functions
on R, metric spaces, etc have to be ‘represented’ or ‘coded’.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Higher-order Reverse Mathematics
Kohlenbach introduces higher-order RM in RM2001.

Second-order RM only has variables n ∈ N and X ⊂ N. Functions
on R, metric spaces, etc have to be ‘represented’ or ‘coded’.
Kohlenbach’s higher-order RM uses the richer language of all finite
types.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Higher-order Reverse Mathematics
Kohlenbach introduces higher-order RM in RM2001.

Second-order RM only has variables n ∈ N and X ⊂ N. Functions
on R, metric spaces, etc have to be ‘represented’ or ‘coded’.
Kohlenbach’s higher-order RM uses the richer language of all finite
types. Thus, the use of codes or representations is seriously
reduced.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Higher-order Reverse Mathematics
Kohlenbach introduces higher-order RM in RM2001.

Second-order RM only has variables n ∈ N and X ⊂ N. Functions
on R, metric spaces, etc have to be ‘represented’ or ‘coded’.
Kohlenbach’s higher-order RM uses the richer language of all finite
types. Thus, the use of codes or representations is seriously
reduced. E.g. discontinuous functions on R are directly available.

Introduction

The Biggest Five of Reverse Mathematics

The base theory RCAω0
RCAω0 makes use of the language of finite types: n ∈ N or n0 ,f ∈ NN or f 1 , Y : NN → N or Y 2 , et cetera.

The abyss

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The base theory RCAω0
RCAω0 makes use of the language of finite types: n ∈ N or n0 ,f ∈ NN or f 1 , Y : NN → N or Y 2 , et cetera.
RCA0 and RCAω0 prove the same second-order sentences (ECF).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The base theory RCAω0
RCAω0 makes use of the language of finite types: n ∈ N or n0 ,f ∈ NN or f 1 , Y : NN → N or Y 2 , et cetera.
RCA0 and RCAω0 prove the same second-order sentences (ECF).
RCAω0 has axioms for primitive recursion and induction (variationof RCA0 ),Introduction

The Biggest Five of Reverse Mathematics

The abyss

The base theory RCAω0
RCAω0 makes use of the language of finite types: n ∈ N or n0 ,f ∈ NN or f 1 , Y : NN → N or Y 2 , et cetera.
RCA0 and RCAω0 prove the same second-order sentences (ECF).
RCAω0 has axioms for primitive recursion and induction (variationof RCA0 ), axiom of function extensionality,

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The base theory RCAω0
RCAω0 makes use of the language of finite types: n ∈ N or n0 ,f ∈ NN or f 1 , Y : NN → N or Y 2 , et cetera.
RCA0 and RCAω0 prove the same second-order sentences (ECF).
RCAω0 has axioms for primitive recursion and induction (variationof RCA0 ), axiom of function extensionality, and QF-AC1,0 :(∀f 1 )(∃n0 )(Y (f , n) = 0) → (∃G 2 )(∀f 1 )(Y (f , G (f )) = 0),

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The base theory RCAω0
RCAω0 makes use of the language of finite types: n ∈ N or n0 ,f ∈ NN or f 1 , Y : NN → N or Y 2 , et cetera.
RCA0 and RCAω0 prove the same second-order sentences (ECF).
RCAω0 has axioms for primitive recursion and induction (variationof RCA0 ), axiom of function extensionality, and QF-AC1,0 :(∀f 1 )(∃n0 )(Y (f , n) = 0) → (∃G 2 )(∀f 1 )(Y (f , G (f )) = 0),
which guarantees that second-order codes denote third-order functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The base theory RCAω0
RCAω0 makes use of the language of finite types: n ∈ N or n0 ,f ∈ NN or f 1 , Y : NN → N or Y 2 , et cetera.
RCA0 and RCAω0 prove the same second-order sentences (ECF).
RCAω0 has axioms for primitive recursion and induction (variationof RCA0 ), axiom of function extensionality, and QF-AC1,0 :(∀f 1 )(∃n0 )(Y (f , n) = 0) → (∃G 2 )(∀f 1 )(Y (f , G (f )) = 0),
which guarantees that second-order codes denote third-order functions.

Real numbers and ‘=R ’ defined as in RCA0 ; R → R-functions are
NN → NN -functions extensional relative to ‘=R ’.

Introduction

The Biggest Five of Reverse Mathematics

The Biggest Five
Real analysis has been studied in second-order RM, mostly forcontinuous functions.

The abyss

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Biggest Five
Real analysis has been studied in second-order RM, mostly forcontinuous functions.
Coding continuous functions (on Baire space and the reals) does
not change the RM of the Big Five (Kleene, Kohlenbach, Normann,
Sanders).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Biggest Five
Real analysis has been studied in second-order RM, mostly forcontinuous functions.
Coding continuous functions (on Baire space and the reals) does
not change the RM of the Big Five (Kleene, Kohlenbach, Normann,
Sanders).

Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 ) between:
second-order Big Five systems
third-order theorems about (slightly) discontinuous functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Biggest Five
Real analysis has been studied in second-order RM, mostly forcontinuous functions.
Coding continuous functions (on Baire space and the reals) does
not change the RM of the Big Five (Kleene, Kohlenbach, Normann,
Sanders).

Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 ) between:
second-order Big Five systems
third-order theorems about (slightly) discontinuous functions.
These third-order theorems are called second-order-ish for obvious
reasons.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Biggest Five
Real analysis has been studied in second-order RM, mostly forcontinuous functions.
Coding continuous functions (on Baire space and the reals) does
not change the RM of the Big Five (Kleene, Kohlenbach, Normann,
Sanders).

Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 ) between:
second-order Big Five systems
third-order theorems about (slightly) discontinuous functions.
These third-order theorems are called second-order-ish for obvious
reasons. A similar phenomenon does not exist for first- andsecond-order theorems (AFAIK).

Introduction

The Biggest Five of Reverse Mathematics

Weak König’s lemma

The following are equivalent to WKL0 over RCA0 :The abyss

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Weak König’s lemma

The following are equivalent to WKL0 over RCA0 :A continuous function on [0, 1] is bounded.
A bounded continuous function on [0, 1] has a supremum.
A continuous function on [0, 1] attains a maximum.
Cousin’s lemma for continuous functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Weak König’s lemma

The following are equivalent to WKL0 over RCA0 :A continuous function on [0, 1] is bounded.
A bounded continuous function on [0, 1] has a supremum.
A continuous function on [0, 1] attains a maximum.
Cousin’s lemma for continuous functions.
There is no mathematical need to restrict to continuity here!

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Weak König’s lemma
The following third-order thms are equivalent to WKL0 over RCAω0 :Introduction

The Biggest Five of Reverse Mathematics

The abyss

Weak König’s lemma
The following third-order thms are equivalent to WKL0 over RCAω0 :A regulated function on [0, 1] is bounded.
A bounded Baire 1 function on [0, 1] has a supremum.
A upper semi-continuous function on [0, 1] attains a max.
A bounded quasi-continuous function on [0, 1] has a sup.

Cousin’s lemma for quasi-continuous functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Weak König’s lemma
The following third-order thms are equivalent to WKL0 over RCAω0 :A regulated function on [0, 1] is bounded.
A bounded Baire 1 function on [0, 1] has a supremum.
A upper semi-continuous function on [0, 1] attains a max.
A bounded quasi-continuous function on [0, 1] has a sup.

Cousin’s lemma for quasi-continuous functions.
Regulated means: the left and right limits exist.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Weak König’s lemma
The following third-order thms are equivalent to WKL0 over RCAω0 :A regulated function on [0, 1] is bounded.
A bounded Baire 1 function on [0, 1] has a supremum.
A upper semi-continuous function on [0, 1] attains a max.
A bounded quasi-continuous function on [0, 1] has a sup.

Cousin’s lemma for quasi-continuous functions.
Regulated means: the left and right limits exist.
Baire 1 means: pointwise limit of continuous functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Weak König’s lemma
The following third-order thms are equivalent to WKL0 over RCAω0 :A regulated function on [0, 1] is bounded.
A bounded Baire 1 function on [0, 1] has a supremum.
A upper semi-continuous function on [0, 1] attains a max.
A bounded quasi-continuous function on [0, 1] has a sup.

Cousin’s lemma for quasi-continuous functions.
Regulated means: the left and right limits exist.
Baire 1 means: pointwise limit of continuous functions.
Upper semi-continuity means: . . . (Baire).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Weak König’s lemma
The following third-order thms are equivalent to WKL0 over RCAω0 :A regulated function on [0, 1] is bounded.
A bounded Baire 1 function on [0, 1] has a supremum.
A upper semi-continuous function on [0, 1] attains a max.
A bounded quasi-continuous function on [0, 1] has a sup.

Cousin’s lemma for quasi-continuous functions.
Regulated means: the left and right limits exist.
Baire 1 means: pointwise limit of continuous functions.
Upper semi-continuity means: . . . (Baire).
Quasi-continuity means: . . . (Baire and Volterra).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Weak König’s lemma
The following third-order thms are equivalent to WKL0 over RCAω0 :A regulated function on [0, 1] is bounded.
A bounded Baire 1 function on [0, 1] has a supremum.
A upper semi-continuous function on [0, 1] attains a max.
A bounded quasi-continuous function on [0, 1] has a sup.

Cousin’s lemma for quasi-continuous functions.
Regulated means: the left and right limits exist.
Baire 1 means: pointwise limit of continuous functions.
Upper semi-continuity means: . . . (Baire).
Quasi-continuity means: . . . (Baire and Volterra).
WILD: there are 2c non-measurable quasi-continuous functions and2c non-Borel bounded and measurable quasi-continuous functions.

Introduction

The Biggest Five of Reverse Mathematics

Arithmetical comprehension

The following are equivalent to ACA0 over RCA0 :Let F : C → R be continuous where C ⊂ [0, 1] is an
RM-closed set. Then supx∈C F (x) exists.
Let F : C → R be continuous where C ⊂ [0, 1] is an
RM-closed set. Then F attains a maximum value on C .
Jordan decomposition theorem restricted to codes.

The abyss

Introduction

The Biggest Five of Reverse Mathematics

Arithmetical comprehension

The following are equivalent to ACA0 over RCA0 :Let F : C → R be continuous where C ⊂ [0, 1] is an
RM-closed set. Then supx∈C F (x) exists.
Let F : C → R be continuous where C ⊂ [0, 1] is an
RM-closed set. Then F attains a maximum value on C .
Jordan decomposition theorem restricted to codes.
There is no mathematical need to restrict to continuity here!

The abyss

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Arithmetical comprehension
These third-order thms are equivalent to ACA0 over RCAω0 :Let F : C → R be cadlag where C ⊂ [0, 1] is an RM-closed
set. Then supx∈C F (x) exists.
Let F : C → R be cadlag and upper semi-continuous whereC ⊂ [0, 1] is an RM-closed set. Then F attains a maximum
value on C .
Jordan decomposition theorem restricted to cadlag.
Jordan decomposition theorem restricted to quasi-continuity.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Arithmetical comprehension
These third-order thms are equivalent to ACA0 over RCAω0 :Let F : C → R be cadlag where C ⊂ [0, 1] is an RM-closed
set. Then supx∈C F (x) exists.
Let F : C → R be cadlag and upper semi-continuous whereC ⊂ [0, 1] is an RM-closed set. Then F attains a maximum
value on C .
Jordan decomposition theorem restricted to cadlag.
Jordan decomposition theorem restricted to quasi-continuity.
Cadlag means: the continuous on the right with left limit.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Arithmetical comprehension
These third-order thms are equivalent to ACA0 over RCAω0 :Let F : C → R be cadlag where C ⊂ [0, 1] is an RM-closed
set. Then supx∈C F (x) exists.
Let F : C → R be cadlag and upper semi-continuous whereC ⊂ [0, 1] is an RM-closed set. Then F attains a maximum
value on C .
Jordan decomposition theorem restricted to cadlag.
Jordan decomposition theorem restricted to quasi-continuity.
Cadlag means: the continuous on the right with left limit.
Upper semi-continuity means: . . . (Baire).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Arithmetical comprehension
These third-order thms are equivalent to ACA0 over RCAω0 :Let F : C → R be cadlag where C ⊂ [0, 1] is an RM-closed
set. Then supx∈C F (x) exists.
Let F : C → R be cadlag and upper semi-continuous whereC ⊂ [0, 1] is an RM-closed set. Then F attains a maximum
value on C .
Jordan decomposition theorem restricted to cadlag.
Jordan decomposition theorem restricted to quasi-continuity.
Cadlag means: the continuous on the right with left limit.
Upper semi-continuity means: . . . (Baire).
Quasi-continuity means: . . . (Baire and Volterra).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Arithmetical Transfinite Recursion
These third-order thms are equivalent to ATR0 over RCAω0 :Jordan decomposition theorem restricted to arithmetical (or:Σ11 ) functions.
A non-enumerable arithmetical set in R has a limit point.
Cousin’s lemma for effectively Baire 2 functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Arithmetical Transfinite Recursion
These third-order thms are equivalent to ATR0 over RCAω0 :Jordan decomposition theorem restricted to arithmetical (or:Σ11 ) functions.
A non-enumerable arithmetical set in R has a limit point.
Cousin’s lemma for effectively Baire 2 functions.
Baire 1 means: pointwise limit of continuous functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Arithmetical Transfinite Recursion
These third-order thms are equivalent to ATR0 over RCAω0 :Jordan decomposition theorem restricted to arithmetical (or:Σ11 ) functions.
A non-enumerable arithmetical set in R has a limit point.
Cousin’s lemma for effectively Baire 2 functions.
Baire 1 means: pointwise limit of continuous functions.
Baire 2 means: pointwise limit of Baire 1 functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Arithmetical Transfinite Recursion
These third-order thms are equivalent to ATR0 over RCAω0 :Jordan decomposition theorem restricted to arithmetical (or:Σ11 ) functions.
A non-enumerable arithmetical set in R has a limit point.
Cousin’s lemma for effectively Baire 2 functions.
Baire 1 means: pointwise limit of continuous functions.
Baire 2 means: pointwise limit of Baire 1 functions.
Effectively Baire 2 means: iterated limit of double sequence ofcontinuous functions (≈ second-order codes for Baire 2).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Arithmetical Transfinite Recursion
These third-order thms are equivalent to ATR0 over RCAω0 :Jordan decomposition theorem restricted to arithmetical (or:Σ11 ) functions.
A non-enumerable arithmetical set in R has a limit point.
Cousin’s lemma for effectively Baire 2 functions.
Baire 1 means: pointwise limit of continuous functions.
Baire 2 means: pointwise limit of Baire 1 functions.
Effectively Baire 2 means: iterated limit of double sequence ofcontinuous functions (≈ second-order codes for Baire 2).
Baire (1905) notes that Baire 2 functions can be represented as
iterated limits.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Π11 -comprehension
These third-order thms are equivalent to Π11 -CA0 over RCAω0 + X :+For any x ∈ NN , any bounded Σ1,x
1 -class in Q has asupremum.

A bounded effectively Baire 2 f : [0, 1] → R has a supremum.
For n ≥ 2, a bounded and effectively Baire n f : [0, 1] → R
has a supremum.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Π11 -comprehension
These third-order thms are equivalent to Π11 -CA0 over RCAω0 + X :+For any x ∈ NN , any bounded Σ1,x
1 -class in Q has asupremum.

A bounded effectively Baire 2 f : [0, 1] → R has a supremum.
For n ≥ 2, a bounded and effectively Baire n f : [0, 1] → R
has a supremum.
Effectively Baire 2 means: iterated limit of double sequence ofcontinuous functions (≈ second-order codes for Baire 2).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Π11 -comprehension
These third-order thms are equivalent to Π11 -CA0 over RCAω0 + X :+For any x ∈ NN , any bounded Σ1,x
1 -class in Q has asupremum.

A bounded effectively Baire 2 f : [0, 1] → R has a supremum.
For n ≥ 2, a bounded and effectively Baire n f : [0, 1] → R
has a supremum.
Effectively Baire 2 means: iterated limit of double sequence ofcontinuous functions (≈ second-order codes for Baire 2).
Baire (1905) notes that Baire 2 functions can be represented as
iterated limits.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Biggest Five phenomenon of higher-order RM

Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 ) between:
second-order Big Five systems
third-order theorems about (slightly) discontinuous functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Biggest Five phenomenon of higher-order RM

Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 ) between:
second-order Big Five systems
third-order theorems about (slightly) discontinuous functions.
These third-order theorems are called second-order-ish for obvious
reasons.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Biggest Five phenomenon of higher-order RM

Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 ) between:
second-order Big Five systems
third-order theorems about (slightly) discontinuous functions.
These third-order theorems are called second-order-ish for obvious
reasons.
There are a gazillion variations of the previous examples, as there
are a gazillion function classes with gazillion different definitions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The Biggest Five phenomenon of higher-order RM

Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 ) between:
second-order Big Five systems
third-order theorems about (slightly) discontinuous functions.
These third-order theorems are called second-order-ish for obvious
reasons.
There are a gazillion variations of the previous examples, as there
are a gazillion function classes with gazillion different definitions.
There are however hard limits to the Biggest Five phenomenon,
with interesting consequences.

Introduction

Abyss? Abyss!

The Biggest Five of Reverse Mathematics

The abyss

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Abyss? Abyss!

In ordinal analysis, the difference between the systems Π11 -CA0 andΠ12 -CA0 has been described as an abyss or chasm by Michael
Rathjen and Per Martin-Löf.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Abyss? Abyss!

In ordinal analysis, the difference between the systems Π11 -CA0 andΠ12 -CA0 has been described as an abyss or chasm by Michael
Rathjen and Per Martin-Löf.
The difference between Π11 -CA0 and Z2 is therefore galactic innatureIntroduction

The Biggest Five of Reverse Mathematics

The abyss

Abyss? Abyss!

In ordinal analysis, the difference between the systems Π11 -CA0 andΠ12 -CA0 has been described as an abyss or chasm by Michael
Rathjen and Per Martin-Löf.
The difference between Π11 -CA0 and Z2 is therefore galactic innature (about 12 parsecs?)

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Abyss? Abyss!

In ordinal analysis, the difference between the systems Π11 -CA0 andΠ12 -CA0 has been described as an abyss or chasm by Michael
Rathjen and Per Martin-Löf.
The difference between Π11 -CA0 and Z2 is therefore galactic innature (about 12 parsecs?)
Slight variations of the aforementioned second-order-ish theorems
are not provable in RCAω0 + Z2 and stronger systems.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Abyss? Abyss!

In ordinal analysis, the difference between the systems Π11 -CA0 andΠ12 -CA0 has been described as an abyss or chasm by Michael
Rathjen and Per Martin-Löf.
The difference between Π11 -CA0 and Z2 is therefore galactic innature (about 12 parsecs?)
Slight variations of the aforementioned second-order-ish theorems
are not provable in RCAω0 + Z2 and stronger systems.
The mathematical difference between the original and the variation
is infinitesimal.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and Π11 -CA0
This third-order thm is equivalent to Π11 -CA0 over RCAω0 + X :An effectively Baire 2 function F : [0, 1] → [0, 1] has a supremum.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and Π11 -CA0
This third-order thm is equivalent to Π11 -CA0 over RCAω0 + X :An effectively Baire 2 function F : [0, 1] → [0, 1] has a supremum.
This third-order thm is not provable in RCAω0 + X + Z2 :A Baire 2 function F : [0, 1] → [0, 1] has a supremum.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and Π11 -CA0
This third-order thm is equivalent to Π11 -CA0 over RCAω0 + X :An effectively Baire 2 function F : [0, 1] → [0, 1] has a supremum.
This third-order thm is not provable in RCAω0 + X + Z2 :A Baire 2 function F : [0, 1] → [0, 1] has a supremum.
Baire 1 means: pointwise limit of continuous functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and Π11 -CA0
This third-order thm is equivalent to Π11 -CA0 over RCAω0 + X :An effectively Baire 2 function F : [0, 1] → [0, 1] has a supremum.
This third-order thm is not provable in RCAω0 + X + Z2 :A Baire 2 function F : [0, 1] → [0, 1] has a supremum.
Baire 1 means: pointwise limit of continuous functions.
Baire 2 means: pointwise limit of Baire 1 functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and Π11 -CA0
This third-order thm is equivalent to Π11 -CA0 over RCAω0 + X :An effectively Baire 2 function F : [0, 1] → [0, 1] has a supremum.
This third-order thm is not provable in RCAω0 + X + Z2 :A Baire 2 function F : [0, 1] → [0, 1] has a supremum.
Baire 1 means: pointwise limit of continuous functions.
Baire 2 means: pointwise limit of Baire 1 functions.
Effectively Baire 2 means: iterated limit of double sequence ofcontinuous functions (≈ second-order codes for Baire 2).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and Π11 -CA0
This third-order thm is equivalent to Π11 -CA0 over RCAω0 + X :An effectively Baire 2 function F : [0, 1] → [0, 1] has a supremum.
This third-order thm is not provable in RCAω0 + X + Z2 :A Baire 2 function F : [0, 1] → [0, 1] has a supremum.
Baire 1 means: pointwise limit of continuous functions.
Baire 2 means: pointwise limit of Baire 1 functions.
Effectively Baire 2 means: iterated limit of double sequence ofcontinuous functions (≈ second-order codes for Baire 2).
Nota Bene: AC is not the problem!

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and arithmetical comprehension
The following is equivalent to ACA0 over RCAω0 :Jordan decomposition theorem restricted to quasi-continuity.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and arithmetical comprehension
The following is equivalent to ACA0 over RCAω0 :Jordan decomposition theorem restricted to quasi-continuity.
The following is not provable in RCAω0 + Z2 :Jordan decomposition theorem restricted to cliquishness.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and arithmetical comprehension
The following is equivalent to ACA0 over RCAω0 :Jordan decomposition theorem restricted to quasi-continuity.
The following is not provable in RCAω0 + Z2 :Jordan decomposition theorem restricted to cliquishness.
Every cliquish function is the sum of two quasi-continuousfunctions (on the reals).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and arithmetical comprehension
The following is equivalent to ACA0 over RCAω0 :Jordan decomposition theorem restricted to quasi-continuity.
The following is not provable in RCAω0 + Z2 :Jordan decomposition theorem restricted to cliquishness.
Every cliquish function is the sum of two quasi-continuousfunctions (on the reals).
f : [0, 1] → R is quasi-continuous if for all ϵ > 0, N ∈ N, x ∈ [0, 1],
there is (a, b) ⊂ B(x, 21N ) with (∀y ∈ (a, b))(|f (x) − f (y )| < ϵ).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and arithmetical comprehension
The following is equivalent to ACA0 over RCAω0 :Jordan decomposition theorem restricted to quasi-continuity.
The following is not provable in RCAω0 + Z2 :Jordan decomposition theorem restricted to cliquishness.
Every cliquish function is the sum of two quasi-continuousfunctions (on the reals).
f : [0, 1] → R is quasi-continuous if for all ϵ > 0, N ∈ N, x ∈ [0, 1],
there is (a, b) ⊂ B(x, 21N ) with (∀y ∈ (a, b))(|f (x) − f (y )| < ϵ).
f : [0, 1] → is cliquish if for all ϵ > 0, N ∈ N, x ∈ [0, 1], there is(a, b) ⊂ B(x, 21N ) such that (∀y , z ∈ (a, b))(|f (z) − f (y )| < ϵ).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and weak König’s lemmaThis third-order thm is equivalent to WKL0 over RCAω0 :A bounded Baire 1 function F : [0, 1] → R has a supremum.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and weak König’s lemmaThis third-order thm is equivalent to WKL0 over RCAω0 :A bounded Baire 1 function F : [0, 1] → R has a supremum.
This third-order thm is not provable in RCAω0 + Z2 :A regulated function F : [0, 1] → R has a supremum.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and weak König’s lemmaThis third-order thm is equivalent to WKL0 over RCAω0 :A bounded Baire 1 function F : [0, 1] → R has a supremum.
This third-order thm is not provable in RCAω0 + Z2 :A regulated function F : [0, 1] → R has a supremum.
Classically, regulated functions are Baire 1, but this fact is only
provable in certain strong systems.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The abyss and weak König’s lemmaThis third-order thm is equivalent to WKL0 over RCAω0 :A bounded Baire 1 function F : [0, 1] → R has a supremum.
This third-order thm is not provable in RCAω0 + Z2 :A regulated function F : [0, 1] → R has a supremum.
Classically, regulated functions are Baire 1, but this fact is only
provable in certain strong systems.
Many similar results: the classical hierarchy of function classes
looks very different in weak (and some strong) systems.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

On Kleene’s arithmetical quantifier ∃2
The above was obtained based on the RM of Kleene’s ∃2 :(∃E )(∀f ∈ NN )(E (f ) = 0 ↔ (∃n ∈ N)(f (n) = 0)).

(∃2 )

Introduction

The Biggest Five of Reverse Mathematics

The abyss

On Kleene’s arithmetical quantifier ∃2
The above was obtained based on the RM of Kleene’s ∃2 :(∃E )(∀f ∈ NN )(E (f ) = 0 ↔ (∃n ∈ N)(f (n) = 0)).
The system RCAω0 + (∃2 ) is L2 -conservative over ACA0 .

(∃2 )Introduction

The Biggest Five of Reverse Mathematics

The abyss

On Kleene’s arithmetical quantifier ∃2
The above was obtained based on the RM of Kleene’s ∃2 :(∃E )(∀f ∈ NN )(E (f ) = 0 ↔ (∃n ∈ N)(f (n) = 0)).
The system RCAω0 + (∃2 ) is L2 -conservative over ACA0 .
2
Over RCAω
0 , the following are equivalent to (∃ ):(∃2 )Introduction

The Biggest Five of Reverse Mathematics

The abyss

On Kleene’s arithmetical quantifier ∃2
The above was obtained based on the RM of Kleene’s ∃2 :(∃E )(∀f ∈ NN )(E (f ) = 0 ↔ (∃n ∈ N)(f (n) = 0)).
The system RCAω0 + (∃2 ) is L2 -conservative over ACA0 .
2
Over RCAω
0 , the following are equivalent to (∃ ):the existence of a discontinuous R → R-function (Kohlenbach).

(∃2 )Introduction

The Biggest Five of Reverse Mathematics

The abyss

On Kleene’s arithmetical quantifier ∃2
The above was obtained based on the RM of Kleene’s ∃2 :(∃E )(∀f ∈ NN )(E (f ) = 0 ↔ (∃n ∈ N)(f (n) = 0)).
The system RCAω0 + (∃2 ) is L2 -conservative over ACA0 .
2
Over RCAω
0 , the following are equivalent to (∃ ):the existence of a discontinuous R → R-function (Kohlenbach).
the existence of a R → R-function that is not regulated.

(∃2 )Introduction

The Biggest Five of Reverse Mathematics

The abyss

On Kleene’s arithmetical quantifier ∃2
The above was obtained based on the RM of Kleene’s ∃2 :(∃E )(∀f ∈ NN )(E (f ) = 0 ↔ (∃n ∈ N)(f (n) = 0)).
The system RCAω0 + (∃2 ) is L2 -conservative over ACA0 .
2
Over RCAω
0 , the following are equivalent to (∃ ):the existence of a discontinuous R → R-function (Kohlenbach).
the existence of a R → R-function that is not regulated.
the existence of a R → R-function that is not semi-continuous.

(∃2 )Introduction

The Biggest Five of Reverse Mathematics

The abyss

On Kleene’s arithmetical quantifier ∃2
The above was obtained based on the RM of Kleene’s ∃2 :(∃E )(∀f ∈ NN )(E (f ) = 0 ↔ (∃n ∈ N)(f (n) = 0)).

(∃2 )The system RCAω0 + (∃2 ) is L2 -conservative over ACA0 .
2
Over RCAω
0 , the following are equivalent to (∃ ):the existence of a discontinuous R → R-function (Kohlenbach).
the existence of a R → R-function that is not regulated.
the existence of a R → R-function that is not semi-continuous.
the existence of a R → R-function that is not Riemann integrable.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

On Kleene’s arithmetical quantifier ∃2
The above was obtained based on the RM of Kleene’s ∃2 :(∃E )(∀f ∈ NN )(E (f ) = 0 ↔ (∃n ∈ N)(f (n) = 0)).

(∃2 )The system RCAω0 + (∃2 ) is L2 -conservative over ACA0 .
2
Over RCAω
0 , the following are equivalent to (∃ ):the existence of a discontinuous R → R-function (Kohlenbach).
the existence of a R → R-function that is not regulated.
the existence of a R → R-function that is not semi-continuous.
the existence of a R → R-function that is not Riemann integrable.
the existence of a R → R-function that is not Baire 1.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

On Kleene’s arithmetical quantifier ∃2
The above was obtained based on the RM of Kleene’s ∃2 :(∃E )(∀f ∈ NN )(E (f ) = 0 ↔ (∃n ∈ N)(f (n) = 0)).

(∃2 )The system RCAω0 + (∃2 ) is L2 -conservative over ACA0 .
2
Over RCAω
0 , the following are equivalent to (∃ ):the existence of a discontinuous R → R-function (Kohlenbach).
the existence of a R → R-function that is not regulated.
the existence of a R → R-function that is not semi-continuous.
the existence of a R → R-function that is not Riemann integrable.
the existence of a R → R-function that is not Baire 1.
the existence of a R → R-function that is not effectively Baire 2.
...

Introduction

The Biggest Five of Reverse Mathematics

The abyss

On Kleene’s arithmetical quantifier ∃2
The above was obtained based on the RM of Kleene’s ∃2 :(∃E )(∀f ∈ NN )(E (f ) = 0 ↔ (∃n ∈ N)(f (n) = 0)).

(∃2 )The system RCAω0 + (∃2 ) is L2 -conservative over ACA0 .
2
Over RCAω
0 , the following are equivalent to (∃ ):the existence of a discontinuous R → R-function (Kohlenbach).
the existence of a R → R-function that is not regulated.
the existence of a R → R-function that is not semi-continuous.
the existence of a R → R-function that is not Riemann integrable.
the existence of a R → R-function that is not Baire 1.
the existence of a R → R-function that is not effectively Baire 2.
...

The following is not provable in RCAω0 + (∃2 ) + Z2 :There is a R → R-function that is not Baire 2.

Introduction

The Biggest Five of Reverse Mathematics

Exploring the abyss: the uncountability of R
Cantor’s first set theory paper (1874): uncountability of R.

The abyss

Introduction

The Biggest Five of Reverse Mathematics

Exploring the abyss: the uncountability of R
Cantor’s first set theory paper (1874): uncountability of R.

Cantor’s theorem: there is no surjection from N to [0, 1].
NIN: there is no injection from [0, 1] to N.
NBI there is no bijection from [0, 1] to N.

The abyss

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Exploring the abyss: the uncountability of R
Cantor’s first set theory paper (1874): uncountability of R.

Cantor’s theorem: there is no surjection from N to [0, 1].
NIN: there is no injection from [0, 1] to N.
NBI there is no bijection from [0, 1] to N.
Many many many (third-order) mainstream theorems imply NIN or
NBI.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Exploring the abyss: the uncountability of R
Cantor’s first set theory paper (1874): uncountability of R.

Cantor’s theorem: there is no surjection from N to [0, 1].
NIN: there is no injection from [0, 1] to N.
NBI there is no bijection from [0, 1] to N.
Many many many (third-order) mainstream theorems imply NIN or
NBI. However, NIN and NBI cannot be proved in RCAω0 + Z2 andstronger (higher-order) systems (see Normann-Sanders, JSL, 2022).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

What causes this abyss?
A function class is second-order-ish if its definition allows one toapproximate f (x) for all x ∈ R given only f (q) for all q ∈ Q.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

What causes this abyss?
A function class is second-order-ish if its definition allows one toapproximate f (x) for all x ∈ R given only f (q) for all q ∈ Q.
Examples: continuity, quasi-continuity, effectively Baire 2, Baire 1.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

What causes this abyss?
A function class is second-order-ish if its definition allows one toapproximate f (x) for all x ∈ R given only f (q) for all q ∈ Q.
Examples: continuity, quasi-continuity, effectively Baire 2, Baire 1.
Non-examples: regulated, cliquish, Baire 2, upper semi-continuity.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

What causes this abyss?
A function class is second-order-ish if its definition allows one toapproximate f (x) for all x ∈ R given only f (q) for all q ∈ Q.
Examples: continuity, quasi-continuity, effectively Baire 2, Baire 1.
Non-examples: regulated, cliquish, Baire 2, upper semi-continuity.
Theorems about second-order-ish function classes can generally be
proved from second-order axioms.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

What causes this abyss?
A function class is second-order-ish if its definition allows one toapproximate f (x) for all x ∈ R given only f (q) for all q ∈ Q.
Examples: continuity, quasi-continuity, effectively Baire 2, Baire 1.
Non-examples: regulated, cliquish, Baire 2, upper semi-continuity.
Theorems about second-order-ish function classes can generally be
proved from second-order axioms.
Theorems about NON-second-order-ish function classes generally
cannot be proved from second-order axioms (alone).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

What causes this abyss?
A function class is second-order-ish if its definition allows one toapproximate f (x) for all x ∈ R given only f (q) for all q ∈ Q.
Examples: continuity, quasi-continuity, effectively Baire 2, Baire 1.
Non-examples: regulated, cliquish, Baire 2, upper semi-continuity.
Theorems about second-order-ish function classes can generally be
proved from second-order axioms.
Theorems about NON-second-order-ish function classes generally
cannot be proved from second-order axioms (alone).
Classically, regulated functions are Baire 1 but this fact is only
provable in strong systems.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

What causes this abyss?
A function class is second-order-ish if its definition allows one toapproximate f (x) for all x ∈ R given only f (q) for all q ∈ Q.
Examples: continuity, quasi-continuity, effectively Baire 2, Baire 1.
Non-examples: regulated, cliquish, Baire 2, upper semi-continuity.
Theorems about second-order-ish function classes can generally be
proved from second-order axioms.
Theorems about NON-second-order-ish function classes generally
cannot be proved from second-order axioms (alone).
Classically, regulated functions are Baire 1 but this fact is only
provable in strong systems.
Many similar results: the classical hierarchy of function classes
looks very different in weak (and some strong) systems.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The state of the art
Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 or extensions) between:(a) second-order Big Five systems(b) third-order theorems about (slightly) discontinuous functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The state of the art
Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 or extensions) between:(a) second-order Big Five systems(b) third-order theorems about (slightly) discontinuous functions.
The theorems in (b) are called second-order-ish for obvious reasons.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The state of the art
Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 or extensions) between:(a) second-order Big Five systems(b) third-order theorems about (slightly) discontinuous functions.
The theorems in (b) are called second-order-ish for obvious reasons.
There are a gazillion possible equivalences, warranting the namethe Biggest Five phenomenon.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The state of the art
Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 or extensions) between:(a) second-order Big Five systems(b) third-order theorems about (slightly) discontinuous functions.
The theorems in (b) are called second-order-ish for obvious reasons.
There are a gazillion possible equivalences, warranting the namethe Biggest Five phenomenon.
Slight variations or generalisations of the theorems in (b) imply
NIN and cannot be proved in RCAω0 + Z2 and stronger systems.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The state of the art
Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 or extensions) between:(a) second-order Big Five systems(b) third-order theorems about (slightly) discontinuous functions.
The theorems in (b) are called second-order-ish for obvious reasons.
There are a gazillion possible equivalences, warranting the namethe Biggest Five phenomenon.
Slight variations or generalisations of the theorems in (b) imply
NIN and cannot be proved in RCAω0 + Z2 and stronger systems.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The state of the art
Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 or extensions) between:(a) second-order Big Five systems(b) third-order theorems about (slightly) discontinuous functions.
The theorems in (b) are called second-order-ish for obvious reasons.
There are a gazillion possible equivalences, warranting the namethe Biggest Five phenomenon.
Slight variations or generalisations of the theorems in (b) imply
NIN and cannot be proved in RCAω0 + Z2 and stronger systems.
Similar results for WWKL, Vitali’s covering lemma, and Kleene’s (∃2 ).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The state of the art
Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 or extensions) between:(a) second-order Big Five systems(b) third-order theorems about (slightly) discontinuous functions.
The theorems in (b) are called second-order-ish for obvious reasons.
There are a gazillion possible equivalences, warranting the namethe Biggest Five phenomenon.
Slight variations or generalisations of the theorems in (b) imply
NIN and cannot be proved in RCAω0 + Z2 and stronger systems.
Similar results for WWKL, Vitali’s covering lemma, and Kleene’s (∃2 ).
Many equivalences for NIN and basic properties of regulated
functions.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

The state of the art
Recently, Dag Normann and I have obtained a plethora ofequivalences (over RCAω0 or extensions) between:(a) second-order Big Five systems(b) third-order theorems about (slightly) discontinuous functions.
The theorems in (b) are called second-order-ish for obvious reasons.
There are a gazillion possible equivalences, warranting the namethe Biggest Five phenomenon.
Slight variations or generalisations of the theorems in (b) imply
NIN and cannot be proved in RCAω0 + Z2 and stronger systems.
Similar results for WWKL, Vitali’s covering lemma, and Kleene’s (∃2 ).
Many equivalences for NIN and basic properties of regulated
functions. Same for basic properties of measure and category andsemi-continuity (Baire, Volterra, . . . ).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Foundational musings

Non-second-order-ish mathematics exhibits a number of interesting
phenomena that are ‘miniature’ versions of well-known
observations in set theory, including:Introduction

The Biggest Five of Reverse Mathematics

The abyss

Foundational musings

Non-second-order-ish mathematics exhibits a number of interesting
phenomena that are ‘miniature’ versions of well-known
observations in set theory, including:the mercurial nature of the cardinality of R,
basic properties of the Lebesgue measure and integral,
the special role of the Axiom of Choice,the asymmetry between measure and category.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Foundational musings
Non-second-order-ish mathematics exhibits a number of interesting
phenomena that are ‘miniature’ versions of well-known
observations in set theory, including:Introduction

The Biggest Five of Reverse Mathematics

The abyss

Foundational musings
Non-second-order-ish mathematics exhibits a number of interesting
phenomena that are ‘miniature’ versions of well-known
observations in set theory, including:the mercurial nature of the cardinality of R:

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Foundational musings
Non-second-order-ish mathematics exhibits a number of interesting
phenomena that are ‘miniature’ versions of well-known
observations in set theory, including:the mercurial nature of the cardinality of R:
ZFC cannot prove the Continuum Hypothesis.
RCAω
0 + Z2 cannot prove: there is no injection from R to N.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Foundational musings
Non-second-order-ish mathematics exhibits a number of interesting
phenomena that are ‘miniature’ versions of well-known
observations in set theory, including:the mercurial nature of the cardinality of R:
ZFC cannot prove the Continuum Hypothesis.
RCAω
0 + Z2 cannot prove: there is no injection from R to N.

basic properties of the integralR
ZF cannot prove that [0,1] f dλ = 0 implies f (x) = 0 a.e. forf : [0, 1] → [0, 1] for the Lebesgue integral.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Foundational musings
Non-second-order-ish mathematics exhibits a number of interesting
phenomena that are ‘miniature’ versions of well-known
observations in set theory, including:the mercurial nature of the cardinality of R:
ZFC cannot prove the Continuum Hypothesis.
RCAω
0 + Z2 cannot prove: there is no injection from R to N.

basic properties of the integralR
ZF cannot prove that [0,1] f dλ = 0 implies f (x) = 0 a.e. forf : [0, 1] → [0, 1] for the Lebesgue integral.
R1
RCAω
0 + Z2 cannot prove 0 f (x)dx = 0 implies f (x) = 0 a.e.
for f : [0, 1] → [0, 1] for the Riemann integral.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Foundational musings
Non-second-order-ish mathematics exhibits a number of interesting
phenomena that are ‘miniature’ versions of well-known
observations in set theory, including:the mercurial nature of the cardinality of R:
ZFC cannot prove the Continuum Hypothesis.
RCAω
0 + Z2 cannot prove: there is no injection from R to N.

basic properties of the integralR
ZF cannot prove that [0,1] f dλ = 0 implies f (x) = 0 a.e. forf : [0, 1] → [0, 1] for the Lebesgue integral.
R1
RCAω
0 + Z2 cannot prove 0 f (x)dx = 0 implies f (x) = 0 a.e.
for f : [0, 1] → [0, 1] for the Riemann integral.

the special role of the Axiom of Choice: countable AC versus
NCC (see arxiv https://arxiv.org/abs/2006.01614 or JLC).

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Foundational musings
Non-second-order-ish mathematics exhibits a number of interesting
phenomena that are ‘miniature’ versions of well-known
observations in set theory, including:the mercurial nature of the cardinality of R:
ZFC cannot prove the Continuum Hypothesis.
RCAω
0 + Z2 cannot prove: there is no injection from R to N.

basic properties of the integralR
ZF cannot prove that [0,1] f dλ = 0 implies f (x) = 0 a.e. forf : [0, 1] → [0, 1] for the Lebesgue integral.
R1
RCAω
0 + Z2 cannot prove 0 f (x)dx = 0 implies f (x) = 0 a.e.
for f : [0, 1] → [0, 1] for the Riemann integral.

the special role of the Axiom of Choice: countable AC versus
NCC (see arxiv https://arxiv.org/abs/2006.01614 or JLC).
basic properties of measure (zero) and category.

Introduction

The Biggest Five of Reverse Mathematics

The abyss

Thanks!
Questions?
Funded by the Klaus Tschira Foundation, German DFG, and RUB
Bochum.