关于0.9循环=1，问点不一样的问题：为什么对它无论有多少严谨证明，不相信的人始终是不相信？

因为这个问题背后是对 Leibniz Equality 的理解。可惜大部分老师一辈子也意识不到 equality 的概念是需要定义和教学的。

例如：

当我们说5=5时，这里的等号指的是左右字面上相同；当我们说s(4)=5时指的是5的定义是4的后继（一般都是这么定义的），这种相等称为definition equality；

当我们说3+2=5时，指的是加法运算，要通过运算的定义对加号进行展开和reduction，经过一系列的连等式从3+2推到5，这种相等称为computation equality；

当我们说a+b=b+a时，说的是一个理论。它既不能通过定义得出，也不能通过计算得出。这种相等和上面两个相等都不一样，称作propositional equality。

以上是直觉类型论的看法。

也有别的类型论用 definition equality 和 setoid equality。不展开讲了。

0.9循环=1里这个相等不是上述任何一种。它是 Leibniz equality。具体定义是：如果任何对a成立的命题都对b成立，那么a=b。这种 equality 关注的a和b两个东西和外界相互作用，而不关心a和b具体的构成。实际上，Leibniz equality 必须作为一个公理被引入，而且也没那么直观。虽然缺少 Leibniz equality 的逻辑系统很大程度上没法做数学，但是这样的系统是成立的，并且也能得出不少有价值的结论。例如从 Coq 中去掉这条公理就得到了这样一个逻辑系统。另一方面，0.9循环等于1的问题很可能是一个人数学学习生涯中第一次接触到需要直接运用 Leibniz equality 的问题。

如果没有学过上述 equality 的区别，自然就会疑惑为什么要把0.9循环和1这两个从构造到形式上都完全不一样的东西说成一样的。这个问题下诸多讲极限，小数的定义，实分析什么的回答都是在证明它们的 Leibniz equality，或者利用了这个 equality 来构造前置的理论，比如极限就不可能绕开 Leibniz equality 来定义。但是很多讲解者没有意识到这个 equality 是需要单独引入的一个公理，而且这个公理某种程度上是反直觉的：

如果一个鸟走路起来像鸭子，游泳起来像鸭子，叫起来也像鸭子，那么就可以被称为鸭子。这种观点下建立的动态类型系统在某些计算机语言中很有用，但是放到现实生活中自然是很荒谬的。有的人意识到了这种荒谬性，但是没有人向他们提出这条公理的话可能一辈子都搞不明白这个问题。某种意义上他们可能比那些没有注意到各种 equality 区别的人更加敏感。想必 Leibniz 也是这种人之一。