[FOM] Higher types, LEM, and Reverse Mathematics

[sasander at cage.ugent.be]

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:

Traditional/classical/Friedman-Simpson-style Reverse Mathematics (RM)  
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.

PPS: The curious reader may read about higher-order RM here (jww Dag Normann):

https://arxiv.org/abs/1711.08939








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