- 在线时间
- 2 小时
- 最后登录
- 2015-6-25
- 注册时间
- 2015-3-26
- 听众数
- 10
- 收听数
- 1
- 能力
- 0 分
- 体力
- 4 点
- 威望
- 0 点
- 阅读权限
- 20
- 积分
- 16
- 相册
- 0
- 日志
- 0
- 记录
- 0
- 帖子
- 29
- 主题
- 5
- 精华
- 0
- 分享
- 0
- 好友
- 1
升级   11.58% TA的每日心情 | 难过 2015-3-27 16:59 |
|---|
签到天数: 1 天 [LV.1]初来乍到
- 自我介绍
- 哈利路亚
|
大概有以下几种可能:
+ p/ Q: Q7 s1 U! j- {因为任何一个数学系统都至少强于一阶系统。同时,一个系统的表达能力越强,那么它的优良属性就越少。因此对于部分系统来说,其中的定理证明是不可停机的。这种不可停机性并不标志着这个定理无法证明,而是标志着这个定理没有一个机械的证明方式,一个证明必然需要自己构造一种方式,但是这类证明应该很少会作为习题出现。
/ n P/ Y8 _ a0 w而对于那些稍稍强于一阶系统的数学系统,或者是,在证明过程中并没有用到超出一阶系统所需要的工具和推理规则的系统,证明不出来的原因在于证明步骤的长度以及可能的证明方式的数量。证明就和在迷宫中走棋一样,你就是在按照一定的规则将你的棋子挪动到指定的位置上,如果需要移动的步数很多,你就有可能因为看不到路径而迷失方向,而另一方面,即便是一个很近的目标,你也有可能因为可以选择的手段太多(而其中只有为数不多的正确途径)而使得你找不到出路。(计算机不会遇到这样的困难,但是它可能要花很长时间才能完成一个形式证明。)! b1 x: u; U0 }4 G- e! b E
当然还剩下一种可能就是证明本身是 trivial 的,但是你并没有真正地理解。
; Q! z& V) H+ B3 x/ g3 l
, T8 Z% O3 {0 U* J最后送你一句话:知道国际象棋的下棋规则和会下国际象棋是两回事。* J s. V2 Q3 {, C) I7 ?( ?4 F
|
|