主题：谈谈陈经的"预测和自由意志"的例子 -- CatOH

一个形式系统FS，如果在FS中蕴含了皮亚诺的五条关于整数公理，那么就说它可定义数论命题。这五条公理是：

· 1是自然数；

· 每一个确定的自然数a，都有一个确定的后继数a' ，a' 也是自然数；

· 如果b、c都是自然数a的后继数，那么b = c；

· 1不是任何自然数的后继数；

· 若任何集合X, 如果1属于X, 并且n属于X可以推出n'属于X，另外X不包含其他的元素，则X等同于自然数集合。

Godel证明，如果FS可定义数论命题，则FS要么是不一致的（可能有A 和非A两个命题同时存在），要么是不完备的（其中有一个用FS表述的命题，其真假性无法判定）。

所谓自指没有明确的数学定义。事实上能够定义出罗素悖论的系统可以很简单，反过来说，可以修改公理体系来避免罗素悖论，但这个体系仍然可以包含数论命题。

至于if…then…goto则属于更基本的算法描述上，它不是形式系统的组成部分。或者可以说它是一种简写，方便人们对算法的理解而存在的。