受到 关于0.9循环=1，问点不一样的问题：为什么对它无论有多少严谨证明，不相信的人始终是不相信？ – 王谷谷的回答 – 知乎 的启发，醍醐灌顶。
你可能早就知道 \(\lim\limits_{x\to 1}\frac{x^2-1}{x-1}=2\) 这样的东西，并且知道如何用 \(\epsilon-\delta\) 语言严格的定义极限。但是仍然对这里的等号存有一些疑惑，这个等号好像和以前的等号不太一样？
上面那个回答里提到 computation equality 和 propositional equality，我认为这两种 equality 只是在形式上不一样，但都可以转化为最基本的 definition equality。比如我们都知道自然数可以用皮亚诺公理严格定义，而在定义了后继这个概念后，加法就可以转化成不断求后继的行为，那么从定义上就可以得知 \(1+1=2\)。
但极限定义中的等号无论如何也没法转化为 definition equality，只能看成 Leibniz equality，费劲找到 Leibniz equality 应该是这个定义：
我们暂且只考虑实数。对实数的谓词逻辑（predicate）实际上就只有判断大小关系吧（？），而只需要定义 \(<\) 就可以推出 \(>,=,\ge,\le,\ne\)。那么 \(\forall a<2\)，令 \(\delta=2-a>0\)，必然可以找到一个 \(\epsilon\) 使得 \(\frac{x^2-1}{x-1}>2-\delta=a\)。这样我们就在使用 Leibniz equality 这个前设（？）的情况下定义了 \(<\)，自然后面的其他大小关系也可以用 Leibniz equality 定义出了。
原文地址：http://www.cnblogs.com/huaruoji/p/16844319.html
