# [FOM] Higher types, LEM, and Reverse Mathematics

sasander at cage.ugent.be sasander at cage.ugent.be
Mon Mar 19 16:12:30 EDT 2018

```Dear All,

I would like to share a powerful application in Reverse Math of higher
types and LEM (=law of excluded middle), namely that the combination
of the aforementioned gives rise to much shorter/easier proofs in the
system WKL_0.

The following three easy steps lead to the conclusion:

1) Two-sentence history:

has mostly been developed in the framework of second-order arithmetic.
Kohlenbach has proposed *higher-order* RM which makes use of the
language of finite types, but the higher-order RM development lags
behind.

2) A strange equivalence involving higher types:

Kohlenbach?s base theory RCA_0^omega of higher-order RM proves that

WKL_0 <=> [ACA_0 V HBU] (*)

where the first two axioms in (*) are well-known, and the third one
deserves to be better known:

HBU is ?Heine-Borel theorem for Uncountable covers?, i.e. any
uncountable open cover of the unit interval has a finite sub-cover.
HBU is a statement of third-order arithmetic and requires full
second-order arithmetic (as given by 3E) for a proof (See PPS below
for references).

3) A nice observation regarding (*) is as follows:

Thanks to (*), to prove a theorem T in WKL_0, it suffices to provide
two ?much easier? proofs as follows:

a) a proof of T in ACA_0, which is much easier than a proof in WKL_0.

b) a proof of T in RCA_0^omega + HBU; this proof probably already
exists in the literature: Robert Bartle and many others have
redeveloped analysis (from the undergrad level up) based on HBU, as
the latter plays a central role in the development of the gauge
integral, a generalisation of Lebesgue?s integral and a (the?) direct
formalisation of Feynman?s path integral (See PPS below for references).

In any case, HBU is orders of magnitude more powerful than WKL_0, i.e.
any proof using the former should be much easier than a proof using
the latter, esp. if no RM codes are available.

Conclusion: the development of math in WKL_0 using (*) provides a huge
shortcut, and we even no longer have to actually *use* the minimal
axiom WKL_0: we can ?do the RM of WKL" using two much stronger axioms,
i.e. ACA_0 and HBU.
Such is the power of higher types and LEM.

Best,

Sam

PS: One of course needs LEM to prove (*), and the proof is left to the reader.

https://arxiv.org/abs/1711.08939

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

```