[FOM] Transfinite Recursion in Functional Analysis and Measure Theory

[Sam Sanders]

Dear Adam,

> I would appreciate examples of proofs in FA and MT where Transfinite Recursion was used.
> 
> Also "sensible" formulations of TR  in ZF set theory  would be welcome.

Borel’s original proof of the (countable) open-cover compactness of intervals seems to qualify:

https://www.maa.org/press/periodicals/convergence/an-analysis-of-the-first-proofs-of-the-heine-borel-theorem-borels-proof

Note that later proofs (including those by Borel himself) do not use TR, but the more familiar ‘divide and conquer’ technique.  


Some people have mentioned TR for arithmetical formulas, embodied by the system ATR_0 in reverse math.  

As it happens, ATR_0 can be derived from the combination of the following basic higher-order theorems:

1) existence of a discontinuous function on R.  

2) the open-cover compactness (for uncountable covers) of [0,1].  

Perhaps this is why one does not see TR that much in analysis: what can be done via ATR_0
can also be done via the combination of 1) and 2), which are much more elementary than TR.

I hope this is what you mean by “sensible”, though there is no reversal there.   

Best,

Sam

PS: Replacing 2) by the (weak) Lindoef property for Baire space, one even obtains Pi11-CA_0, 
and hence Pi11-TR_0 is almost within reach.