3,094
个编辑
更改
无编辑摘要
* 证明：取 <math>\theta(v)</math> = "<math>v</math> 不可证"，由不动点引理得 <math>\sigma\iff\text{"}\sigma\text{不可证"}</math>。若<math>\sigma</math> 可证，则它说的是真话（我不可证），矛盾；若 <math>\neg\sigma</math> 可证，则"<math>\sigma</math> 可证"，又矛盾。于是 <math>\sigma</math> 与 <math>\neg\sigma</math> 都不可证——不完备定理成立。把 <math>\theta</math> 换成 [[J. Barkley Rosser|Rosser]] 的精巧变体，还能去掉"<math>\omega</math>-一致性"这个额外假设，得到 [[Rosser 强化]]<ref name="godel1931" /><ref name="moschovakis2010" />。
* 证明：取 <math>\theta(v)</math> = "<math>v</math> 不可证"，由不动点引理得 <math>\sigma\iff\text{"}\sigma\text{不可证"}</math>。若<math>\sigma</math> 可证，则它说的是真话（我不可证），矛盾；若 <math>\neg\sigma</math> 可证，则"<math>\sigma</math> 可证"，又矛盾。于是 <math>\sigma</math> 与 <math>\neg\sigma</math> 都不可证——不完备定理成立。把 <math>\theta</math> 换成 [[J. Barkley Rosser|Rosser]] 的精巧变体，还能去掉"<math>\omega</math>-一致性"这个额外假设，得到 [[Rosser 强化]]<ref name="godel1931" /><ref name="moschovakis2010" />。
* '''[[Myhill定理]]（1955）'''：[[罗宾逊算术]] Q 的任何一致、可公理化扩张 <math>T</math>，其定理集都是'''[[创造集]]'''（见 [[#Myhill定理：创造集 = 完备集|§5.8.5.3]]），从而是 r.e.-完备的<ref name="moschovakis2010" />.
* '''[[Myhill定理]]（1955）'''：[[罗宾逊算术]] Q 的任何一致、可公理化扩张 <math>T</math>，其定理集都是'''[[创造集]]'''（见 [[#Myhill定理：创造集 = 完备集|§5.8.5.2]]），从而是 r.e.-完备的<ref name="moschovakis2010" />.
合起来我们可以得到一个惊人结论：所有足够强的一致公理化理论（[[皮亚诺算术]]、[[ZFC公理系统]]<math>\ldots\ldots</math>）都自动满足不动点引理的条件，因而都不完备、不可判定；而且任意两个这样的理论，其定理集在递归同构意义下完全相同<ref name="moschovakis2010" />。
合起来我们可以得到一个惊人结论：所有足够强的一致公理化理论（[[皮亚诺算术]]、[[ZFC公理系统]]<math>\ldots\ldots</math>）都自动满足不动点引理的条件，因而都不完备、不可判定；而且任意两个这样的理论，其定理集在递归同构意义下完全相同<ref name="moschovakis2010" />。
可判定、可枚举这类词只能作用于自然数集合，索引集正是那道翻译层——它把"程序行为问题"转写成 <math>\mathbb{N}</math> 的子集，之后才能问"这个性质能判定吗、能枚举吗"。两个要点：其一，此类性质必须'''只看行为、不看代码'''（同一函数的两个不同编号在 A 中必须同真同假），否则退化为平凡的代码分析。
可判定、可枚举这类词只能作用于自然数集合，索引集正是那道翻译层——它把"程序行为问题"转写成 <math>\mathbb{N}</math> 的子集，之后才能问"这个性质能判定吗、能枚举吗"。两个要点：其一，此类性质必须'''只看行为、不看代码'''（同一函数的两个不同编号在 A 中必须同真同假），否则退化为平凡的代码分析。
与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 [[#Myhill定理：创造集 = 完备集|5.8.5.3]]）。
与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 [[#Myhill定理：创造集 = 完备集|5.8.5.2]]）。
===== [[Rice定理]]（1951） =====
===== [[Rice定理]]（1951） =====