我在斯坦福大学提供的在线逻辑介绍开放课程中遇到了这个疑问。
在这本教科书的第 9.4 节下：http: //logic.stanford.edu/intrologic/secondary/notes/chapter_09.html
它说：
这里显示的公理用 0 和 s 定义了相同的关系。（其中下面的函数常数字母 s 表示后继函数，例如 s(0)=1, s(1)=2, s(2)=3 ）
∀x.same(x,x)
∀x.(¬same(0,s(x)) ∧ ¬same(s(x),0))
∀x.∀y.(¬same(x,y) ⇒ ¬same(s(x),s(y)))
据我了解，：
第一句话说两个相同的数字是相同的。第二句和第三句用于定义不同之处。
第二个说没有任何数字的后继与0相同。
第三个说如果两个数字不相同，那么它们的继任者就不一样。例如，如果 1≠3，则 2≠4。
但是，我认为第三句话应该是双条件的，因为如果我没记错的话，定义没有涵盖被证明的数字小于给定数字的情况，否则可以说如果2≠ 4，则 1=3。
所以我想知道这是教科书上的错误还是我的推理有问题。
这本教科书没有错误。虽然该陈述确实在两个方向上都成立，但没有必要将其声明为公理，因为另一个方向来自后继函数的功能属性和教科书中列出的三个公理。
正式证明将涉及定义后继函数的公理。更习惯于使用自动证明器的人或者只是一个逻辑学的好学生可能能够完成这样一个正式的证明。
这里只是一个证明的草图。它使用符号“=”来表示术语相等，即u = v表示 u 和 v 是使用符号 0 和 s() 编写的语法相同的术语。此外，“ u < v ”意味着 u 和v都是基本术语，并且 u 对s ()的应用严格少于v。
认为
∀x.∀y.(¬same(s(x),s(y)) ⇒ ¬same(x,y))
不成立，则存在一些项 x0 和 y0 使得
相同（x0，y0）和¬相同（s（x0），s（y0））。
由于 s(x0) 是一个函数，因此从 ¬same(s(x0),s(y0)) 和 ∀x.same(x,x) 可以得出 x0 和 y0 是两个不同的项。首先让我们考虑当 x0 < y0，然后 y0 = s(...s(x0)) 的情况，其中有n个 s() 和n > 0 的应用。当 y0 < x0 的另一种情况可以类似地处理。
将 s(...s(x0)) 替换为 same(x0,y0) 中的 y0，我们得到 same(x0,s(...s(x0)))。
还有 x0 = s(...s(0)) ，其中s() 对某些非负整数m有m次应用。在提供的方向上使用第三个公理，我们可以说如果相同（s（u），s（v））那么相同（u，v）。因此，从 same(x0,s(...s(x0))) 我们可以“剥离” s() 的m个应用程序以获得
same(0,s(...s(0))) 其中第二个参数中有n个 s() 应用。这与第二个公理相矛盾。量子点