更改
跳到导航
跳到搜索
第501行：
第501行： − + − + − + − + − + − + − + + − + − + − + − + − + − + − + − |- − | 示例 || 示例 || 示例
无编辑摘要
! 比较条目 !! 图灵停机问题 !! 哥德尔定理
! 比较条目 !! 图灵停机问题 !! 哥德尔定理
|-
|-
| 示例 || 示例 || 示例
| 基本符号 || 程序设计语言的基本符号，诸如“if then, for, loop...” || 谓词逻辑符号:“~,∧,∨,∃,∀”,算 数运算符:“+,×,=”,数字,变量等等
|-
|-
| 示例 || 示例 || 示例
| 基本单元 || 基本符号拼接出的完整的计算机程序，例如“Print("hello world");” || 基本符号拼接出的合法的命题语句,诸 如:“∀a: ~(a+1)=0”
|-
|-
| 示例 || 示例 || 示例
| 计算 || 计算机程序对字符串操作产生新的字符串 || 命题语句根据公理和规则推导产生新的命题语句
|-
|-
| 示例 || 示例 || 示例
| 单元编码 || 程序的源代码（字符串） || 命题的哥德尔编号
|-
|-
| 示例 || 示例 || 示例
| 层次混淆 || 程序P去读另一个程序S的源代码s，并进行运算P(s) || 将一个命题的哥德尔编号n输入给包含自由变元的命题,并完成运算f(n)
|-
|-
| 示例 || 示例 || 示例
| 单元意义 || 程序是否停机(停或不停) || 命题是否正确(真或假)
|-
|-
| 示例 || 示例 || 示例
| 有意义的单元集合 || 所有的停机的计算机程序，数据对：(x,y)。即当x作用到y上面的时候X(y)停机 || 所有的定理,即根据公理和推理规则推 单元集合 导出的命题语句。我们希望所有的定理 都是真的(一致性),并且所有的真命题
都是定理(完备性)
|-
|-
| 示例 || 示例 || 示例
| 系统自身给出的意义判断 || H(x,y)函数：判断源代码为x的计算机程序作用到数据y上面是否停机 || 语句“∃m:T(m,n)”,即“存在一个自然数m,使得m和n构成证明对”,也就是“n所代表的命题是一个定理”
|-
|-
| 示例 || 示例 || 示例
| 蒯恩函数 || 计算机程序Q(x)，定义为：让程序X读入自己的源代码，即Q(x)="X(x)" || 函数Q(n),定义为:将一个包含自由变元的语句N的编号n代入其自身的自由变元中,即 Q(n)=N(n)
|-
|-
| 示例 || 示例 || 示例
| “我” || Q(q)，就是将蒯恩函数Q的源代码q（字符串）喂给函数Q它自己的代码。Q(q)为一个字符串，Q(q)="Q(q)" || Q(q)，将函数Q自己的哥德尔编号q喂给函数Q。Q(q)得到的数就是它自己的哥德尔配数。Q(q)=c(Q(q))。
|-
|-
| 示例 || 示例 || 示例
| 悖论函数 || 程序D(z)，他是蒯恩程序与判断程序H(x,y)的结合，即D(z)=H(z,z)=H(Q(z))，其中z为输入的参数 || 函数Q<u>о</u>T,也就是蒯恩函数Q(x)与意义判断语句的结合: Q<u>о</u>T(n)=“~∃m: T(m,Q(n))”,其中 n 为一个自由变元
|-
|-
| 示例 || 示例 || 示例
| 悖论单元 || 当程序D作用到它自己的源代码上，即D(d)，表示“我不停机”。 || G,当函数Q<u>о</u>T作用到它自己的哥德尔编码q<u>о</u>t上所产生的哥德尔语句即G=“~∃m:T(m,Q(q<u>о</u>t))”,表示“我不是定理”。注意,Q(q<u>о</u>t)得到的就是G的编码
|-
|-
| 示例 || 示例 || 示例
| 二律背反 || 当H(d,d)判断D(d)停机的时候，D(d)自己的表现为不停机；而当H(d,d)判断不停机的时候，D(d)又会停机 || 当G是一个定理的时候，根据G自己的意思，G不是一个定理(破坏了一致性)；当G不是一个定理的时候，我们知道G是一个真句子(破坏了完备性)
|-
|-
| 示例 || 示例 || 示例
| 结论 || 判断一切函数X作用到数据y上是否停机的计算机程序H(x,y)不存在 || 公理系统的一致性和完备性不能同时被满足
|}
|}