※ 引述《noctem (noctem)》之铭言： : Hmm... 我不是很确定懂了buganini的意思啦。讲些可能相关的好了。 : 不过对於这些东西，我知道的大概也是多看几遍 wikipedia 的程度 : 而已。请先进指正。 : 首先是 Church-Turing Thesis. 一般的版本是: : 任何可计算的(computable)函数都可用 Turing machine 算出来。 : 但其实「可计算」这个概念本来就是模糊的，现在我们其实是用 : Turing machine 当作它的定义: 「可计算的函数」的定义就是 : 「Turing machine 可以模拟的。」Church-Turing thesis 其实是 : 说：这样的定义是合理的，和我们的直觉相符。人类可以计算出来 : 的东西，就是有个演算法、在有限的步数里面，用 Turing machine : 可以算的东西。使用参禅等等方式得到的就不算了。 :) : (有比 Turing machine 更强的计算 model 吗？有的，比如说 : 如果我们可以有真正的 real number, 或着每一步可以得到一些 : oracle 等等。但这些都是假想中才存在的机器。即使是量子电脑， : 也仅能比较快地解出一些问题，而不能解出 Turing machine 解 : 不出的问题。） 有的， 可以参考一下这篇 paper http://www-2.cs.cmu.edu/~lblum/PAPERS/TuringMeetsNewton.pdf 试着将 TM 拓展到一般的 ring 结构上，这样使得对复数以及实数等系统， 也有相对应的计算模型。这篇是很有趣，但是书看起来就很闷了 ... : Turing machine 还是有些无法解的问题。哲学上我们就相信这是 : 人类理性的限制了。不过也有人还是说，剩下的东西就是禅啦， : 或着是神的力量等等的... : * * * : 这一系列研究是跟在 Godel 的 incompleteness theorem 之後而来的。 : Hilbert 等等数学家为了解决悬宕已久的一些数学矛盾，决定把 : 数学以严谨的方式重建起来，希望有一套方法能告诉我们任何一个 : 陈述是真或假。Godel 告诉我们不可能。 这点有人以为只有人造（？）的问题，才会遇到这种问题， 实际产生的问题不会遇到。但很可惜的是，在比较抽象的代数理论， 就会遇到了。参见 Whitehead problem： http://en.wikipedia.org/wiki/Whitehead_problem : 但这要看你决定用什麽样的抽象方式来看世界。如果你关心的问题 : 只用 propositional logic 就可以描述，那没问题。（有些朋友知 : 道逻辑有很多套时蛮惊讶的。其实数学逻辑也是人发明的，在什麽 : 情境，哪套逻辑合用，就用那套。）Propositional logic : 确实是完备的，任何陈述要不然就有个证明要不然就有个反证。 : 如果你想描述「对所有的x」、「存在某个 y」等等，你就得用 : predicate logic. 那麽情形就没那麽完美了。所有为真的陈述还是 : 有证明（这其实也是从 Godel 的「完备」定理来的。Godel 有个 : 不完备定理，也有个完备定理 :)）。但这个证明不见得能在有限时 : 间内找得到。你如果一直找某个陈述的证明找不到，你也无法知道它 : 倒底是真是假。 : 如果你需要表达能力更强一点的系统，那情形就更遭。Godel 告诉我 : 们的是，如果一个（consistent的）理论系统强到可以描述算术，那 : 麽它就注定是不完备的。一定会有些陈述是真的，但却没有证明。 : （Consistency 是一个要注意的要求。通常不管什麽逻辑，我们会 : 要求 p 和 not p 不可以同时有证明。否则他就 inconsistent。通 不希望 inconsistent 有一个理由是， 在 natural deduction 系统下， 同时存在 p 跟 not p 会使得，会推得 absurdity, \bot， 而这可以推出任何的陈述。就算从语意来看，也就是用真值表来看也是， 一旦前提为否，接下来的任何陈述不管是什麽，都是真。 : 常这时候我们会觉得是这个系统设计有问题了。前一篇我便提到， : 如果加入 (a -> a) -> a 这个公设，任何东西都证得出来。） : 有了这样的基础之後，Turing 等人继续定义所谓可计算是什麽意思， : 想知道数理系统的限制在哪里。 : 但不完备定理也不能过度引申。有些东西没有证明，但并不表示 : 有证明的东西会是错的。也不表示这个系统不 consistent : (这可能有点回应到 buganini 的一些句子。「因果」如果理解成 : 前提对，结果就会对，那因果还是在的。） : 此外，有些定理没有证明。但这些定理重不重要呢？早期我们能举 : 出的没有证明的定理，其实大多是尝试「自己讲自己」的定理。 : 他们结构都很像，唯一的用处好像也只是当反例而已。直到後来终 : 於有了几个有趣的例子，例如「polymorphic lambda calculus 会 : 终止」这件事情。 : 而同时我们为了各种需要，也仍在使用各种更复杂的逻辑。可以 : 描述先後的逻辑（p 为真，直到 xxx 时候）啦，可以描述资源 : 使用的逻辑啦（所有前提只能被使用一次），等等... modal logic 吗？ --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 123.193.218.153