How to systematically simplify deduction in formal first order logic into daily English

Question

Suppose the function \begin{equation} h(x,y) = \frac{\sin\sqrt{1-x^2-2y^2}}{\sqrt{1-x^2-2y^2}} \end{equation} is defined on $\left\{(x,y)\vert x^2 + 2y^2 < 1\right\}$. We need to prove that \begin{equation} \forall x_0 \in \mathbb{R}, \forall y_0 \in \mathbb{R}, {x_0}^2 + 2{y_{0}}^{2} = 1 \longrightarrow \lim_{(x,y)\to(x_0,y_0)}h(x,y) = 1 \end{equation}

In my proof, I assumed the existence of the following conclusions: \begin{equation} \lim_{u\to 0}\frac{\sin u}{u} = 1, \end{equation} \begin{equation} \forall u, \forall v, u^2 + 2v^2 = 1 \longrightarrow \lim_{(x,y)\to (u,v)} (1-x^2-2y^2) = 0. \end{equation}

To strictly follow the rules of first order logic, I applied the fitch style. The proof is divided into two parts. In the first part, I deduced the following proposition: \begin{equation} \begin{aligned} &\left(\forall u, \forall v, u^2 + 2v^2 = 1 \longrightarrow \lim_{(x,y)\to (u,v)} (1-x^2-2y^2) = 0\right) \longrightarrow\\ &\left(\forall u, \forall v, u^2 + 2v^2 = 1 \longrightarrow \forall \varepsilon > 0, \exists \delta > 0, \forall x, \forall y, \left(0 < \sqrt{(x-u)^2+(y-v)^2} < \delta \wedge x^2+2y^2 < 1\right) \longrightarrow \sqrt{1-x^2-2y^2} < \varepsilon\right) \end{aligned} \end{equation} The formal proof is as follows:

In the second proof, the final conclusion is deduced. The formal proof is given below:

The formal proof of this seemingly simple conclusion is very tedious. However, without proper use of first order logic, there is no systematic way to examine a deduction. Recalling my first classes in undergraduate, I feel very upset about the type of proof I learned at that time. Every deduction was based on intuitive use of math rules, especially for quantification. I am wondering how to train myself to prove in English while have a picture of first order logic in mind.

Answer 1

Actually the proof you wrote is structurally very close to what a mathematician would write, the trick is to make the right omissions, and to be conservative when expanding definitions.

For example, by making the right omissions, translating a hypothesis by "suppose", universal elimination by "let", a conclusion by "then", and existential elimination by "there exists ... such that", then your first proof almost literally translates to:

---

Suppose $$\forall u. \forall v. (u^2 + 2v^2 = 1 \longrightarrow\lim_{(x,y)\to (u,v)} (1-x^2-2y^2) = 0),$$ let $u_0,v_0$ be arbitrary, then suppose $$u_0^2 + 2v_0^2 = 1,$$ then $$\lim_{(x,y)\to (u,v)} (1-x^2-2y^2) = 0,$$ let $\epsilon_0$ be arbitrary, suppose $\epsilon_0 > 0$, then there exists $\delta_0$ such that $$\delta_0>0,$$ $$\forall x.\forall y. 0 < \sqrt{(x - u_0)^2 + (y - v_0)^2} < \delta_0\longrightarrow|1x^2-2y^2|<\epsilon_0^2,$$

let $x_0,y_0$ be arbitrary, then suppose $$0 <\sqrt{(x_0-u_0)^2+(y_0-v_0)^2}<\delta_0,$$ $$x_0^2 + 2y_0^2 < 1,$$ then $$1 - x_0^2 - 2y_0^2 > 0,$$ $$|1 - x_0^2 - 2y_0^2| < \epsilon_0^2,$$ $$\sqrt{1 - x_0^2 - 2y_0^2} < \epsilon_0,$$ thus $$\forall \varepsilon > 0. \exists \delta > 0. \forall x. \forall y. \left(0 <\sqrt{(x-u)^2+(y-v)^2} < \delta \wedge x^2+2y^2 < 1 \\\longrightarrow\sqrt{1-x^2-2y^2} < \varepsilon\right).$$

---

You could write this in even more natural language as

---

Suppose that $$\forall u,v. (u^2 + 2v^2 = 1 \longrightarrow \lim_{(x,y)\to (u,v)} (1-x^2-2y^2) = 0).$$ Now let $u_0,v_0$ be arbitrary, and suppose that $u_0^2 + 2v_0^2 = 1,$ then $\lim_{(x,y)\to (u,v)} (1-x^2-2y^2) = 0.$ So for $\epsilon_0 > 0$, there exists $\delta_0>0$ such that for all $x$ and $y$, $0 < \sqrt{(x - u_0)^2 + (y - v_0)^2} < \delta_0$ implies $|1x^2-2y^2|<\epsilon_0^2.$

Now let $x_0,y_0$ be arbitrary such that $0 <\sqrt{(x_0-u_0)^2+(y_0-v_0)^2}<\delta_0$ and $x_0^2 + 2y_0^2 < 1,$ then since $1 - x_0^2 - 2y_0^2 > 0,$ we know $$1 - x_0^2 - 2y_0^2 = |1 - x_0^2 - 2y_0^2| < \epsilon_0^2,$$ which implies that $\sqrt{1 - x_0^2 - 2y_0^2} < \epsilon_0$, concluding the proof.

---

So even though the natural language proof looks informal and contains omissions, the idea is that it should contain enough information to be able to recover the fully formal proof you have written. However different people write proofs with varying degree of details, depending on how much they expect the reader to be familiar with the topic.