A logical view at Tao's finitization of principles in analysis
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:
These points are then illustrated in a case study: the almost finitization of the infinite pigeonhole principle.
- 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.
This is joint work with Ulrich Kohlenbach.
- 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.