##
A logical view at Tao's finitization of principles in analysis

### Jaime Gaspar

In 2007 and 2008 Terence Tao wrote on his blog essays about the finitization of principles in analysis. His goal is to find for infinite qualitative ``soft analysis'' statements equivalent finitary quantitative ``hard analysis'' statements. These equivalences are usually proved using a contradiction and sequentially compactness argument. Tao's two prime examples are:

- a finitization of the infinite convergence principle (every bounded monotone sequence of real numbers converges);
- an almost finitization of the infinite pigeonhole principle (every colouring of the natural numbers with finitely many colours has a colour that occurs infinitely often).

We take a logical look at Tao's essays and make mainly two points:

- the finitizations can be done in a systematic way using proof theoretical tools, namely G\"odel (Dialectica) functional interpretation;
- Heine-Borel compactness arguments are preferable to sequentially compactness arguments, for reverse mathematics reasons.

These points are then illustrated in a case study: the almost finitization of the infinite pigeonhole principle.
This is joint work with Ulrich Kohlenbach.

References

- Tao2007. Terence Tao, Soft analysis, hard analysis, and the finite convergence principle. http://terrytao.wordpress.com, 2007.
- Tao2008. Terence Tao, The correspondence principle and finitary ergodic theory. http://terrytao.wordpress.com, 2008.
- GasparKohlenbach. Jaime Gaspar and Ulrich Kohlenbach, On Tao's ``finitary'' infinite pigeonhole principle. To appear in The Journal of Symbolic Logic.