换这个号说严肃的事儿。

规则一：0是自然数。
规则二：n是自然数可以推出S(n)也是，S是后继函数。

这是大家都非常熟悉的，而且极其基本的，形式化101。

通过规则一和规则二我们可以证明「如果n是自然数，那么S(S(n))也是自然数」。但是我们却无法证明「如果S(n)是自然数，那么n也是自然数。」

这比兜圈子的哥德尔第一不完备定理简单多了，具体的说

S(n):NAT
-----------
n:NAT

是admissible规则，可以在推理中使用，但不可证。

+++++

对这个现象的直觉理解是，两条基础规则只是generating规则，不包含产生的系统的全部代数特性。而上述admissible规则的存在，恰恰说明了这个系统具有代数特性。