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

Suppose the function $$$$h(x,y) = \frac{\sin\sqrt{1-x^2-2y^2}}{\sqrt{1-x^2-2y^2}}$$$$ is defined on $$\left\{(x,y)\vert x^2 + 2y^2 < 1\right\}$$. We need to prove that $$$$\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$$$$

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

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{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} 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.

• Very few (if any) people have in mind the kind of formal argument that you've written. Instead we train our intuition to spot the kinds of mistakes that might happen, and to be comfortable knowing what arguments CAN be written in a formal system, at least in theory. Of course, everyone makes mistakes, and the push towards computer systems like LEAN, Agda, etc is to eventually have computers actually turn a human readable proof into a completely formal one, which we KNOW is correct. Of course, this future is still somewhat far off for a variety of reasons. Dec 25, 2020 at 3:24
• I'm leaving this as a comment because it doesn't strictly answer your question. Indeed, as you've noticed, Fitch style proofs (and other formal systems too) are EXTREMELY tedious. You're struggling to see how anyone trains themself to think this way, and the simple answer is "we don't" Dec 25, 2020 at 3:27
• @HallaSurvivor I am very anxious to know how mathematicians are trained in math deduction. I am only an engineer with a deep interest in math. Dec 25, 2020 at 3:28
• We learn in the same way everyone learns everything: practice practice practice. Dec 25, 2020 at 3:31
• It's helpful to have other people practicing with you, so you can ask each other questions, point out each others blind spots and mistakes, and generally have fun doing math together. But at the end of the day, the only way to improve is to spend some time doing math. You'll make mistakes, cuz that's how learning works. But over time you'll improve, just like everyone else ^_^ Dec 25, 2020 at 3:33

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.

• Very instructive. When I review real analysis right now, I find a lot of difficulties when I learned the material the first time were from my inability to follow the logic flow. My focus was on labelled equations, instead of propositions made with the equations. I guess this is why most students feel it difficult to learn pure math. In my opinion, math classes should be redesigned, and especially, rigorous logic should be introduced in earlier stages, if any exists. As you said, people may not write proofs in a formal way, but they have to know what happens now and then. Jan 4, 2021 at 15:44
• Glad I could help! Although I don't think it's generally a good idea to teach proof writing in this way, because the purpose of mathematics is to communicate arguments in a convincing way. A completely formal proof is not convincing to me because I have to check every detail and still not get the idea of the proof. I'm sure a few of us appreciate the intricacies of logic, but many people are very happy without. Jan 4, 2021 at 16:17
• @ZiqiFan You may find formal proofs in metamath interesting, for example the intermediate value theorem. Jan 5, 2021 at 11:09