User:IssaRice/Formalizing adjustment of epsilons

I want to elaborate on a thing that shows up when proving part (a) of https://taoanalysis.wordpress.com/2020/05/24/exercise-5-6-1/

Actually, a similar thing appears in Tao's original proof (Proposition 5.5.12) and the situation is simpler there (fewer variables to deal with), so let's start there.

Tao's proof

In the first part of the proof, we suppose $x^{2}<2$, and let $0<\varepsilon <1$. Then we show the bound $(x+\varepsilon )^{2}\leq x^{2}+5\varepsilon$. Now we say that since $x^{2}<2$, we can choose $0<\varepsilon <1$ small enough that $x^{2}+5\varepsilon <2$.

What's so sneaky about this? It's the fact that we say "let $0<\varepsilon <1$" and then later adjust the value of $\varepsilon$. Typically in math, when we say "let $0<\varepsilon <1$", we are allowing the value to be arbitrary, i.e. potentially adversarially chosen. We can't let the adversary choose something, then later change our mind and say "wait a minute, let me pick it instead"!

So what is going on, and why is the argument correct?

I'll use quantifiers so we can be really clear about what's bound and what's free.

We want to show $\exists \varepsilon (\varepsilon >0\wedge (x+\varepsilon )^{2}<2)$, because this will show that $x+\varepsilon \in E$, which will show that $x$ isn't an upper bound of $E$.

What we have are:

(1) $\forall \varepsilon (0<\varepsilon <1\implies (x+\varepsilon )^{2}\leq x^{2}+5\varepsilon )$
(2) $\exists \varepsilon (\varepsilon >0\wedge x^{2}+5\varepsilon <2)$

So now what we do is use (2) to obtain a particular $\varepsilon$. In order to use (1), we actually need to to show $0<\varepsilon <1$, but we only have $0<\varepsilon$.

So actually, we want to show

(3) $\exists \varepsilon (0<\varepsilon <1\wedge x^{2}+5\varepsilon <2)$

To do this, use (2) to obtain $\varepsilon >0$ such that $x^{2}+5\varepsilon <2$. If $\varepsilon <1$ then we are done. If $\varepsilon \geq 1$, then $1/2<\varepsilon$ so $x^{2}+5(1/2)<x^{2}+5\varepsilon <2$, which means we can use 1/2. In either case we have found a number that works, so we have (3).

So now, use (3) to obtain some $\varepsilon$. By (1), we have $0<\varepsilon <1\implies (x+\varepsilon )^{2}\leq x^{2}+5\varepsilon$. Since $0<\varepsilon <1$, we can apply this implication to obtain $(x+\varepsilon )^{2}\leq x^{2}+5\varepsilon$. By (3), we know $x^{2}+5\varepsilon <2$ so we have $(x+\varepsilon )^{2}\leq x^{2}+5\varepsilon <2$ which is what we wanted.

So what was the issue? It was that in the first part of the proof, we were allowing $\varepsilon$ to be arbitrary so that we could show the implication (1). Once we showed that, however, we want to close that context so that we could start a new context with some particular $\varepsilon$. In first-order logic, these aren't the same $\varepsilon$, but when writing out proofs we aren't too careful about this.