|||
数理逻辑用严谨的方式研究语法、语义,涉及语言的局限性。先略加解释要用到的概念、术语和符号。
用个体变元、个体常元、函数符号、关系符号(或称谓词符号),以及与∧、或∨、非¬、蕴涵→等命题连接词,加上“存在∃”和“一切∀”两种量词构成了谓词逻辑语言。语言中,用符号表的字符,按照形成规则组成的字符串叫公式。不含有自由变量的公式叫句子(sentence)。如果量词“存在”和“一切”只允许对个体使用,不允许对集合或谓词等使用,叫一阶语言【1】,它是描写形式公理化系统的标准语言。逻辑语言和这语言中一组句子(称为公理)组成了理论。在一阶语言里如果包含有谓词演算的所有公理、非逻辑公理和谓词演算的所有推理规则,叫一阶理论。如果一阶理论里包含有算术公理,这理论叫一阶算术。
在理论S里一个句子ψ为真,指的是语义(semantic),它解释的客观事件是真的。用模型论【2】的术语说:ψ在模型M里是真的,记为M ⊨ψ. 哥德尔完备性定理说:一阶理论中的句子ψ在S的所有模型中都是真的,等价于ψ在S里成立,记为 S ⊢ ψ。说句子ψ按照真理T的定义是真的,指在S中证明T<ψ>是真的。这里所说:定义为真的,可以形式逻辑推导出来,被证明,都是同一个意思,记为S ⊢φ<ψ>.谓词φ是理论里的一个公式,它用来定义某种属性,包括真理。作为定义要求它对所有的ψ,理论都能证明其真假,也就是可判定的。
一个理论S是相容的(consistent)说;ψ和¬ψ(表示一对相反的命题)至少有一个不能在S里被证明。完全的(complete)的意思是,ψ和¬ψ至少有一个能在S里被证明。所以在相容且完全的理论里,能够对任何命题证明其真伪,能够定义任何属性,能够判定任何命题。反过来,这些性质也都要求理论是相容且完全的才行。
设ψ是谎言悖论的句子,这样的句子无法判断其真伪。在(包含一阶算术的)形式语言里无法定义真理。它表示的命题或反命题,在一阶算术理论里都不能被证明。这说明一阶算术理论不可能是相容且完全的。从这就不难理解塔斯基定理和哥德尔定理的结论。计算机是实现一阶算术理论的逻辑运算工具,所以图灵停机问题也是不可判定的。这些结论的严谨数学证明,在于怎么用形式语言表达出谎言悖论的句子来,这是哥德尔的主要贡献。
下面勾画出这个轮廓,更深入地剖析这些局限的本质和这几个定理间的关系。
当自我指涉的悖论撼动数学基础时,康托尔在之前,就曾经用它创造了对角线法的技巧。这个方法通过假定要证明的反命题成立,来构造出自我指涉的悖论。这从此成为一个数学的利器,证明了许多令人惊异的重要定理。受到康托尔对角线法技巧的启发,Carnap (1934)在哥德尔编码的基础上,证明了如下的“对角线引理”【3】:
设S是包含着一阶算术的理论,对任给公式φ(x)存在一个句子ψ,有 S ⊢ ψ↔φ<ψ>.
这里 S ⊢的意思是:理论S能够证明右边的式子成立。右边式子里的意思是:句子ψ语义的真假与ψ是否具有属性φ是等价的。这里φ<ψ>是φ(<ψ>)的简写,是评判句子ψ具有φ性质的谓词表达式,<ψ>是句子ψ的哥德尔数,看作是对句子的指称。
这个引理说:对于任给一个属性,可以构造出这样一个句子ψ,用自然语言来说是“这句子具有属性φ”。当然这里的ψ是用形式语言表达的,在理论S里证明它是这个意思。前面章节里用它构造个谎言悖论ψ↔ ¬T <ψ> 证明了塔斯基定理。
塔斯基定理:任何包含着一阶算术的理论,也包含了T模式,则是不相容的。(Any theory extending first-order arithmetic and containing schema T is inconsistent.)
在一阶算术里构造一个公式φ,φ<ψ>的意思为“命题ψ不能在理论里得到证明”,则可以推出哥德尔定理。我在《哥德尔定理的证明》系列里介绍了这个经典的证明。下面介绍怎么从塔斯基定理,推出哥德尔第一不完全性定理的梗概。以此可以理解:哥德尔定理揭露出来形式公理化数学系统的局限性,其实是由语言的局限所决定的。
哥德尔第一不完全性定理(Gödel's first incompleteness theorem):
假如一阶算术理论是ω-相容的(ω-consistent),则它是不完全的。
这ω-相容【4】的意思是:对于任何公式φ(x),如果系统里对于每个自然数n,φ(n)都不成立,则不能推出存在着一个x让φ(x)成立。用符号记为:⊢¬φ(n) for all n∈Z,则⊬∃x φ(x). 这个ω-相容性比相容性的强,可以推出后者来(J Barkley Rosser在1936年证明这定理对较弱的“相容”条件也成立)。哥德尔证明了可以用形式算术语言构造出公式Dem(n, <φ>),有:
⊢Dem(n, <φ>) 当且仅当 n是证明句子φ的形式语言符号串的哥德尔数
如果理论是ω-相容的且完全的,不难从定义中推出,⊢∃xDem(x, <φ>) 等价于对给定的φ,有个具体的n 使得⊢ Dem(n, <φ>),根据上面元语言的解释即是,对所有的句子(命题)有:
⊢∃xDem(x, <φ>) ↔φ,forall sentence φ
公式∃xDem(x, <φ>) 是用形式语言表达了命题φ在理论里可以得到证明的意思,也就是符合“句子φ在这理论里被证明为真”的定义。所以我们可以把它缩写成指称为真的谓词T,即有:
⊢ T<φ> ↔φ, forall sentence φ.
这就是T模式。这证明一阶算术如果是ω-相容的和完备的,则包含了T模式。从塔斯基定理得知,它是不相容的。这个矛盾证明了哥德尔定理。上面T模式产生了矛盾的直接解读是:一阶算术理论中的有些真理,不可能在一阶算术理论中得到证明。这个矛盾产生的原因是语言的局限性:在一阶算术里,不能定义形式逻辑的推导(证明)作为判定命题真假的谓词。
停机问题是数理逻辑中可计算性理论的重要问题【5】。图灵的停机问题不可判定性定理(Undecidability of the Halting Problem)说:“不存在着图灵机能够确定停机问题。”用现代的计算机概念来说是:没有一个程序能够通过检验输入的计算机程序,来判断它是否会在有限的时间内完成计算。这个定理原来是通过用图灵机模仿对角线法来证明,下面是程序版的证明,可以让了解C编程的人,对这问题有个直观的理解。
假设上帝程序God_tell通过检查program和data,告诉我们true还是false,对应着program(data)能否在有限时间内完成运算。
bool God_tell (char* program, char* data)
{
if ( program with data will not run forever) //check program to get the answer
return true;
return false;
}
构造一个魔鬼程序Satan_tell和上帝唱反调,会完成的程序让它进入死循环,否则就完成它。
bool Satan_tell (char* program)
{
if ( God_tell (program, program) ) {
//God tell us program(program) will finish and return.
while(1); // loop forever!
return false; // can never get here!
} else
//God tell us program(program) will not stop
return true; //let’s exit
}
现在问Satan_tell (Satan_tell) 会在有限的时间内完成计算吗?相当于问图灵机会停机吗?
这是个自我指涉的问题,它的逻辑类同于Grelling悖论,在那悖论里问:“异质”是异质的吗?Satan_tell就是那个异质形容词,它与形容的对象program的表现相反,所以也陷入Grelling悖论。我们再分析一下它为什么是悖论。Satan_tell (Satan_tell)的结果不外乎两种,一是进入死循环,不能完成,一是完成计算后返回。假如能完成,从上帝程序的设计知道God_tell(Satan_tell, Satan_tell)将返回true,这样在魔鬼程序里便进入死循环不停机,与假设矛盾。假如不能停机,God_tell(Satan_tell, Satan_tell)将返回false,在魔鬼程序里则返回true,却是完成返回。又是一个矛盾。这说明上帝程序God_tell不可能存在,否则就会产生悖论。也就是说不可能有个程序能够判断给定程序的停机问题。
哥德尔不完备性定理、塔斯基不可定义性定理和图灵停机问题不可判定性定理,是上个世纪数理逻辑里最亮丽的风景线,它们紧密相连。分别表达了数学形式证明能力的局限性,形式语言表达能力的局限性和机器计算能力的局限性。它们都是用自我指涉的悖论来证明的。
为什么自我指涉悖论动摇了数学和语言理解的基础,大家因此制定规则来阻止它,我们却又可以用它来证明定理呢?
(待续)
【参考资料】
【1】Wikipedia,First-orderlogic http://en.wikipedia.org/wiki/First-order_logic
【2】科学网博文,理解数学——模型(3)http://blog.sciencenet.cn/blog-826653-717208.html
【3】Wikipedia,Diagonallemma http://en.wikipedia.org/wiki/Diagonal_lemma
【4】Wikipedia,ω-consistenttheory http://en.wikipedia.org/wiki/%CE%A9-consistent_theory
【5】SEP,Turing Machines http://plato.stanford.edu/entries/turing-machine/
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-12-23 21:14
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社