更改

跳到导航 跳到搜索
删除2字节 、 2026年9月17日 (星期四)
第576行: 第576行:  
* '''不动点引理''':设 <math>T</math> 是任何足够强的可公理化理论,则对任何含一个自由变量的公式 <math>\theta(v)</math>,都存在句子 <math>\sigma</math>,使 <math>T</math> 可证 "<math>\sigma\iff\theta</math>(⌜<math>\sigma</math>⌝)"(⌜<math>\sigma</math>⌝ 是 <math>\sigma</math> 的哥德尔数)。即:'''任何性质 <math>\theta</math>,都存在一个句子 <math>\sigma</math>,在 <math>T</math> 可证的意义下恰好谈论"自己是否具有 <math>\theta</math>"'''<ref name="moschovakis2010" />。
 
* '''不动点引理''':设 <math>T</math> 是任何足够强的可公理化理论,则对任何含一个自由变量的公式 <math>\theta(v)</math>,都存在句子 <math>\sigma</math>,使 <math>T</math> 可证 "<math>\sigma\iff\theta</math>(⌜<math>\sigma</math>⌝)"(⌜<math>\sigma</math>⌝ 是 <math>\sigma</math> 的哥德尔数)。即:'''任何性质 <math>\theta</math>,都存在一个句子 <math>\sigma</math>,在 <math>T</math> 可证的意义下恰好谈论"自己是否具有 <math>\theta</math>"'''<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" />。
+
* 证明:取 <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.3]]),从而是 r.e.-完备的<ref name="moschovakis2010" />.

导航菜单