多说一句：公理系统的定理证明只是半可计算的。

公理系统中的一个命题，是不是定理，这个问题只是半可判定的，或者说半可计算的。

 

如果命题是定理，那么用图林机计算，一定会枚举出这个定理，也就是说会证明这个定理。图林机最终会停机。

 

如果命题不是定理，那么用图林机计算，只是不停地枚举定理，永远不会枚举出这个命题。图林机也永远不会停机，

 

所有跟帖： 

• Thanks! -xinliji- ♀ (0 bytes) () 10/30/2010 postreply 11:05:11