结城浩所著《数学女孩3：哥德尔不完备定理》读书笔记

一、哥德尔编码的奥秘

哥德尔编码建立了自然数与形式系统的映射关系，形式系统可以引用这些映射的自然数参与形式系统计算，从而在看似牢不可破的形式系统中引入了自我指涉的隐患。

#mermaid-svg-T2uSSdAawETArmUd {font-family:"trebuchet ms",verdana,arial,sans-serif;font-size:16px;fill:#333;}#mermaid-svg-T2uSSdAawETArmUd .error-icon{fill:#552222;}#mermaid-svg-T2uSSdAawETArmUd .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-T2uSSdAawETArmUd .edge-thickness-normal{stroke-width:2px;}#mermaid-svg-T2uSSdAawETArmUd .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-T2uSSdAawETArmUd .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-T2uSSdAawETArmUd .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-T2uSSdAawETArmUd .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-T2uSSdAawETArmUd .marker{fill:#333333;stroke:#333333;}#mermaid-svg-T2uSSdAawETArmUd .marker.cross{stroke:#333333;}#mermaid-svg-T2uSSdAawETArmUd svg{font-family:"trebuchet ms",verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-T2uSSdAawETArmUd defs #statediagram-barbEnd{fill:#333333;stroke:#333333;}#mermaid-svg-T2uSSdAawETArmUd g.stateGroup text{fill:#9370DB;stroke:none;font-size:10px;}#mermaid-svg-T2uSSdAawETArmUd g.stateGroup text{fill:#333;stroke:none;font-size:10px;}#mermaid-svg-T2uSSdAawETArmUd g.stateGroup .state-title{font-weight:bolder;fill:#131300;}#mermaid-svg-T2uSSdAawETArmUd g.stateGroup rect{fill:#ECECFF;stroke:#9370DB;}#mermaid-svg-T2uSSdAawETArmUd g.stateGroup line{stroke:#333333;stroke-width:1;}#mermaid-svg-T2uSSdAawETArmUd .transition{stroke:#333333;stroke-width:1;fill:none;}#mermaid-svg-T2uSSdAawETArmUd .stateGroup .composit{fill:white;border-bottom:1px;}#mermaid-svg-T2uSSdAawETArmUd .stateGroup .alt-composit{fill:#e0e0e0;border-bottom:1px;}#mermaid-svg-T2uSSdAawETArmUd .state-note{stroke:#aaaa33;fill:#fff5ad;}#mermaid-svg-T2uSSdAawETArmUd .state-note text{fill:black;stroke:none;font-size:10px;}#mermaid-svg-T2uSSdAawETArmUd .stateLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.5;}#mermaid-svg-T2uSSdAawETArmUd .edgeLabel .label rect{fill:#ECECFF;opacity:0.5;}#mermaid-svg-T2uSSdAawETArmUd .edgeLabel .label text{fill:#333;}#mermaid-svg-T2uSSdAawETArmUd .label div .edgeLabel{color:#333;}#mermaid-svg-T2uSSdAawETArmUd .stateLabel text{fill:#131300;font-size:10px;font-weight:bold;}#mermaid-svg-T2uSSdAawETArmUd .node circle.state-start{fill:#333333;stroke:#333333;}#mermaid-svg-T2uSSdAawETArmUd .node .fork-join{fill:#333333;stroke:#333333;}#mermaid-svg-T2uSSdAawETArmUd .node circle.state-end{fill:#9370DB;stroke:white;stroke-width:1.5;}#mermaid-svg-T2uSSdAawETArmUd .end-state-inner{fill:white;stroke-width:1.5;}#mermaid-svg-T2uSSdAawETArmUd .node rect{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-T2uSSdAawETArmUd .node polygon{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-T2uSSdAawETArmUd #statediagram-barbEnd{fill:#333333;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-cluster rect{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-T2uSSdAawETArmUd .cluster-label,#mermaid-svg-T2uSSdAawETArmUd .nodeLabel{color:#131300;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-cluster rect.outer{rx:5px;ry:5px;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-state .divider{stroke:#9370DB;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-state .title-state{rx:5px;ry:5px;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-cluster.statediagram-cluster .inner{fill:white;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-cluster.statediagram-cluster-alt .inner{fill:#f0f0f0;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-cluster .inner{rx:0;ry:0;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-state rect.basic{rx:5px;ry:5px;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-state rect.divider{stroke-dasharray:10,10;fill:#f0f0f0;}#mermaid-svg-T2uSSdAawETArmUd .note-edge{stroke-dasharray:5;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-note rect{fill:#fff5ad;stroke:#aaaa33;stroke-width:1px;rx:0;ry:0;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-note rect{fill:#fff5ad;stroke:#aaaa33;stroke-width:1px;rx:0;ry:0;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-note text{fill:black;}#mermaid-svg-T2uSSdAawETArmUd .statediagram-note .nodeLabel{color:black;}#mermaid-svg-T2uSSdAawETArmUd .statediagram .edgeLabel{color:red;}#mermaid-svg-T2uSSdAawETArmUd #dependencyStart,#mermaid-svg-T2uSSdAawETArmUd #dependencyEnd{fill:#333333;stroke:#333333;stroke-width:1;}#mermaid-svg-T2uSSdAawETArmUd :root{--mermaid-font-family:"trebuchet ms",verdana,arial,sans-serif;}

表示定理

哥德尔编码

可代入计算

原始递归谓词成立

在形式系统P中存在形式证明

必然对应一些自然数

二、证明过程

Q ( m , n ) = ¬ P r o v e s ( m , S u b s t ( n , y 1 , n ‾ ) ) {Q(m,n)=\neg Proves(m,Subst(n,\boxed{y_1},\overline n))} Q(m,n)=¬Proves(m,Subst(n,y1,n))
- Q ( m , n ) Q(m,n) Q(m,n)明显是一个原始递归谓词
- 这里 m , n m,n m,n均是任意的自然数，没有任何限定
- 这里 m , n m,n m,n均是任意的自然数，没有任何限定：
  - n n n可能是逻辑公式也可能不是
  - 同样 m m m可能是逻辑公式序列也可能不是
  - 只有 n n n是逻辑公式且 m m m是逻辑公式序列时， P r o v e s ( m , S u b s t ( n , y 1 , n ‾ ) ) Proves(m,Subst(n,\boxed{y_1},\overline n)) Proves(m,Subst(n,y1,n))才有可能为 0 0 0
- 当 n n n其不是逻辑公式时，必然有 P r o v e s ( m , S u b s t ( n , y 1 , n ‾ ) ) = 0 Proves(m,Subst(n,\boxed{y_1},\overline n))=0 Proves(m,Subst(n,y1,n))=0
- n n n为逻辑公式时，可能包含自由的变量 y 1 y_1 y1也可能没有，但这必然会加大 S u b s t ( n , y 1 , n ‾ ) ) Subst(n,\boxed{y_1},\overline n)) Subst(n,y1,n))成为语句（即没有自由变量的逻辑公式）的可能性

1、种子——从含义的世界到形式的世界

A1: P r o v e s ( m , n ⟨ n ‾ ⟩ ) ⇒ ¬ Q ( m , n ) ⇒ I s P r o v a b l e ( n o t ( q ⟨ m ‾ , n ‾ ⟩ ) ) Proves(m,n\langle \overline n \rangle)\Rightarrow\neg{Q(m,n)} \Rightarrow IsProvable(not(q\langle\overline m, \overline n \rangle)) Proves(m,n⟨n⟩)⇒¬Q(m,n)⇒IsProvable(not(q⟨m,n⟩))
- 后面一个推理用到了表示定理，正如第一部分《哥德尔编码的奥秘》中所示
- 其中 q q q是形式系统 P P P原始递归谓词 Q ( m , n ) Q(m,n) Q(m,n)对应的逻辑公式，包含两个自由的变量
B1: ¬ P r o v e s ( m , n ⟨ n ‾ ⟩ ) ⇒ Q ( m , n ) ⇒ I s P r o v a b l e ( q ⟨ m ‾ , n ‾ ⟩ ) \neg Proves(m,n\langle\overline n\rangle) \Rightarrow Q(m,n) \Rightarrow IsProvable(q\langle \overline m,\overline n\rangle) ¬Proves(m,n⟨n⟩)⇒Q(m,n)⇒IsProvable(q⟨m,n⟩)
- 后面一个推理同样用到了表示定理

2、绿芽—— p p p的定义

C1: p ⟨ y 1 ⟩ = d e f F o r A l l ( x 1 , q ⟨ x 1 , y 1 ⟩ ) p\langle y_1\rangle\overset{def}{=}ForAll(\boxed{x_1},q\langle \boxed {x_1},\boxed {y_1}\rangle) p⟨y1⟩=defForAll(x1,q⟨x1,y1⟩)
- 这个逻辑公式 p p p的定义中表明其并非原始递归的谓词，因为变量 x 1 x_1 x1虽然受 F o r A l l ForAll ForAll限制，但其并无上限规定。
- 逻辑公式 p p p只含一个自由变量 y 1 y_1 y1
C2: p ⟨ p ‾ ⟩ = F o r A l l ( x 1 , q ⟨ x 1 , p ‾ ⟩ ) p\langle \overline p\rangle=ForAll(\boxed{x_1},q\langle \boxed{x_1},\overline p \rangle) p⟨p⟩=ForAll(x1,q⟨x1,p⟩)
- 逻辑公式 p p p中的自由变量 y 1 y_1 y1已经被 p ‾ \overline p p所替代，成为了一个语句

3、树杈—— r r r 的定义

C3: r ⟨ x 1 ⟩ = d e f q ⟨ x 1 , p ‾ ⟩ r\langle \boxed{x_1} \rangle\overset{def}{=}q\langle\boxed{x_1},\overline p\rangle r⟨x1⟩=defq⟨x1,p⟩
C4: $r\langle\overline m\rangle=q\langle \overline m,\overline p \rangle $

4、叶子——从 A1 往下走

A1: P r o v e s ( m , n ⟨ n ‾ ⟩ ) ⇒ I s P r o v a b l e ( n o t ( q ⟨ m ‾ , n ‾ ⟩ ) ) Proves(m,n\langle \overline n\rangle)\Rightarrow IsProvable(not(q\langle \overline m, \overline n \rangle)) Proves(m,n⟨n⟩)⇒IsProvable(not(q⟨m,n⟩))
A2: P r o v e s ( m , p ⟨ p ‾ ⟩ ) ⇒ I s P r o v a b l e ( n o t ( q ⟨ m ‾ , p ‾ ⟩ ) ) Proves(m,p\langle \overline p \rangle)\Rightarrow IsProvable(not(q\langle \overline m, \overline p\rangle)) Proves(m,p⟨p⟩)⇒IsProvable(not(q⟨m,p⟩))
- 单纯的逻辑公式代换，因为：
  - 逻辑公式 n n n只含一个自由变量 y 1 y_1 y1，且没有任何其它限定
  - 特定逻辑公式 p p p也含一个自由变量 y 1 y_1 y1
- 这种逻辑公式的代换本质上是一个哥德尔数带入了原始递归谓词，这正是第一部分《哥德尔编码的奥秘》中所示
A3: P r o v e s ( m , F o r A l l ( x 1 , q ⟨ x 1 , p ‾ ⟩ ) ) ⇒ I s P r o v a b l e ( n o t ( q ⟨ m ‾ , p ‾ ⟩ ) ) Proves(m,ForAll(\boxed{x_1},q\langle \boxed{x_1},\overline p \rangle))\Rightarrow IsProvable(not(q\langle \overline m, \overline p\rangle)) Proves(m,ForAll(x1,q⟨x1,p⟩))⇒IsProvable(not(q⟨m,p⟩))
- 这是单纯的逻辑公式代换，根据逻辑公式 p p p的定义
A4: P r o v e s ( m , F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) ) ⇒ I s P r o v a b l e ( n o t ( q ⟨ m ‾ , p ‾ ⟩ ) ) Proves(m,ForAll(\boxed{x_1},r\langle \boxed{x_1}\rangle))\Rightarrow IsProvable(not(q\langle \overline m, \overline p\rangle)) Proves(m,ForAll(x1,r⟨x1⟩))⇒IsProvable(not(q⟨m,p⟩))
- 这是单纯的逻辑公式代换，根据逻辑公式 r r r的定义
A5: P r o v e s ( m , F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) ) ⇒ I s P r o v a b l e ( n o t ( r ⟨ m ‾ ⟩ ) ) Proves(m,ForAll(\boxed{x_1},r\langle \boxed{x_1}\rangle))\Rightarrow IsProvable(not(r\langle\overline m\rangle)) Proves(m,ForAll(x1,r⟨x1⟩))⇒IsProvable(not(r⟨m⟩))
- 这是单纯的逻辑公式代换，根据逻辑公式 r r r的定义

5、蓓蕾——从 B1 开始往下

B1: ¬ P r o v e s ( m , n ⟨ n ‾ ⟩ ) ⇒ I s P r o v a b l e ( q ⟨ m ‾ , n ‾ ⟩ ) \neg Proves(m,n\langle \overline n\rangle)\Rightarrow IsProvable(q\langle \overline m, \overline n \rangle) ¬Proves(m,n⟨n⟩)⇒IsProvable(q⟨m,n⟩)
B2: ¬ P r o v e s ( m , p ⟨ p ‾ ⟩ ) ⇒ I s P r o v a b l e ( q ⟨ m ‾ , p ‾ ⟩ ) \neg Proves(m,p\langle \overline p \rangle)\Rightarrow IsProvable(q\langle \overline m, \overline p\rangle) ¬Proves(m,p⟨p⟩)⇒IsProvable(q⟨m,p⟩)
- 单纯的逻辑公式代换，因为：
  - 逻辑公式 n n n只含一个自由变量 y 1 y_1 y1，且没有任何其它限定
  - 特定逻辑公式 p p p也含一个自由变量 y 1 y_1 y1
B3: ¬ P r o v e s ( m , F o r A l l ( x 1 , q ⟨ x 1 , p ‾ ⟩ ) ) ⇒ I s P r o v a b l e ( q ⟨ m ‾ , p ‾ ⟩ ) \neg Proves(m,ForAll(\boxed{x_1},q\langle \boxed{x_1},\overline p \rangle))\Rightarrow IsProvable(q\langle \overline m, \overline p\rangle) ¬Proves(m,ForAll(x1,q⟨x1,p⟩))⇒IsProvable(q⟨m,p⟩)
- 这是单纯的逻辑公式代换，根据逻辑公式 p p p的定义
B4: ¬ P r o v e s ( m , F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) ) ⇒ I s P r o v a b l e ( q ⟨ m ‾ , p ‾ ⟩ ) \neg Proves(m,ForAll(\boxed{x_1},r\langle \boxed{x_1}\rangle))\Rightarrow IsProvable(q\langle \overline m, \overline p\rangle) ¬Proves(m,ForAll(x1,r⟨x1⟩))⇒IsProvable(q⟨m,p⟩)
- 这是单纯的逻辑公式代换，根据逻辑公式 r r r的定义
B5: ¬ P r o v e s ( m , F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) ) ⇒ I s P r o v a b l e ( r ⟨ m ‾ ⟩ ) \neg Proves(m,ForAll(\boxed{x_1},r\langle \boxed{x_1}\rangle))\Rightarrow IsProvable(r\langle\overline m\rangle) ¬Proves(m,ForAll(x1,r⟨x1⟩))⇒IsProvable(r⟨m⟩)
- 这是单纯的逻辑公式代换，根据逻辑公式 r r r的定义

6、 g = d e f F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) g\overset{def}{=}ForAll(\boxed{x_1},r\langle\boxed{x_1}\rangle) g=defForAll(x1,r⟨x1⟩)

7、梅花—— ¬ I s P r o v a b l e ( g ) \neg IsProvable(g) ¬IsProvable(g)（反证法）

D0: 形式系统P是相容的
D1: I s P r o v a b l e ( F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) ) IsProvable(ForAll(\boxed{x_1},r\langle \boxed{x_1}\rangle)) IsProvable(ForAll(x1,r⟨x1⟩))

形式证明假设为 s s s
D2: P r o v e s ( s , F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) ) Proves(s, ForAll(\boxed{x_1},r\langle\boxed{x_1}\rangle)) Proves(s,ForAll(x1,r⟨x1⟩))
D3: P r o v e s ( s , F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) ) ⇒ I s P r o v a b l e ( n o t ( r ⟨ s ‾ ⟩ ) ) Proves(s,ForAll(\boxed{x_1},r\langle\boxed{x_1}\rangle))\Rightarrow IsProvable(not(r\langle\overline s\rangle)) Proves(s,ForAll(x1,r⟨x1⟩))⇒IsProvable(not(r⟨s⟩))
- 这是典型的含义世界的推理规则-2，即 ∀ x 1 [ r ⟨ x 1 ⟩ = 0 ] ⇒ s u b s t ( r ⟨ x 1 ⟩ , x 1 , s ‾ ) ⇔ r ⟨ s ‾ ⟩ \forall x_1[r\langle x_1\rangle=0]\Rightarrow subst(r\langle x_1\rangle,x_1,\overline s)\Leftrightarrow r\langle \overline s\rangle ∀x1[r⟨x1⟩=0]⇒subst(r⟨x1⟩,x1,s)⇔r⟨s⟩
D4: I s P r o v a b l e ( n o t ( r ⟨ s ‾ ⟩ ) ) IsProvable(not(r\langle\overline s\rangle)) IsProvable(not(r⟨s⟩))
- 这是典型的含义世界的推理规则-1，即 p ∧ ( p ⇒ q ) ⇒ q p\wedge (p\Rightarrow q)\Rightarrow q p∧(p⇒q)⇒q
D5: I s P r o v a b l e ( r ⟨ s ‾ ⟩ ) IsProvable(r\langle\overline s\rangle) IsProvable(r⟨s⟩)
- 这是典型的含义世界的推理规则-2
D6: 形式系统 P 是矛盾的
D7: ¬ I s P r o v a b l e ( F o r A l l ( x 1 , r ⟨ x 1 ) ) \neg IsProvable(ForAll(\boxed{x_1},r\langle\boxed{x_1})) ¬IsProvable(ForAll(x1,r⟨x1))

8、桃花—— ¬ I s P r o v a b l e ( n o t ( g ) ) \neg IsProvable(not(g)) ¬IsProvable(not(g))的证明（反证法，并利用ω相容）

E0: 形式系统P是ω相容的
E1: ¬ P r o v e s ( t , F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) ) \neg Proves(t, ForAll(\boxed{x_1},r\langle\boxed{x_1}\rangle)) ¬Proves(t,ForAll(x1,r⟨x1⟩))——对于任意逻辑公式的序列 t t t都成立
- 这是D7的推论：因为若有一个序列 t t t使得 P r o v e s ( t , F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) ) Proves(t, ForAll(\boxed{x_1},r\langle\boxed{x_1}\rangle)) Proves(t,ForAll(x1,r⟨x1⟩))成立，必有 I s P r o v a b l e ( F o r A l l ( x 1 , r ⟨ x 1 ) ) IsProvable(ForAll(\boxed{x_1},r\langle\boxed{x_1})) IsProvable(ForAll(x1,r⟨x1))，但这明显与D7相悖
E2: ¬ P r o v e s ( t , F o r A l l ( x 1 , r ⟨ x 1 ⟩ ) ) ⇒ I s P r o v a b l e ( r ⟨ t ‾ ⟩ ) \neg Proves(t, ForAll(\boxed{x_1},r\langle\boxed{x_1}\rangle)) \Rightarrow IsProvable(r\langle\overline t\rangle) ¬Proves(t,ForAll(x1,r⟨x1⟩))⇒IsProvable(r⟨t⟩)
- 这是 B5的直接变量代换结果
E3: I s P r o v a b l e ( r ⟨ t ‾ ⟩ ) IsProvable(r\langle\overline t\rangle) IsProvable(r⟨t⟩)
- 这是典型的含义世界的推理规则-1，即 p ∧ ( p ⇒ q ) ⇒ q p\wedge (p\Rightarrow q)\Rightarrow q p∧(p⇒q)⇒q
- 注意！此时序列 t t t是任意的，也就是任意的自然数
E4: I s P r o v a b l e ( n o t ( F o r A l l ( x 1 , r ⟨ x 1 ) ) ) IsProvable(not(ForAll(\boxed{x_1},r\langle\boxed{x_1}))) IsProvable(not(ForAll(x1,r⟨x1)))
E5: 形式系统P是ω矛盾的
E6: ¬ I s P r o v a b l e ( n o t ( F o r A l l ( x 1 , r ⟨ x 1 ) ) ) \neg IsProvable(not(ForAll(\boxed{x_1},r\langle\boxed{x_1}))) ¬IsProvable(not(ForAll(x1,r⟨x1)))

9、樱花—证明形式系统 P 是不完备的

F1： g g g和 n o t ( g ) not(g) not(g)两者都不存在形式证明
F2: 形式系统 P 是不完备的

1-9、证明流程

#mermaid-svg-Ji7v5wCtzljUJxbH {font-family:"trebuchet ms",verdana,arial,sans-serif;font-size:16px;fill:#333;}#mermaid-svg-Ji7v5wCtzljUJxbH .error-icon{fill:#552222;}#mermaid-svg-Ji7v5wCtzljUJxbH .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-Ji7v5wCtzljUJxbH .edge-thickness-normal{stroke-width:2px;}#mermaid-svg-Ji7v5wCtzljUJxbH .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-Ji7v5wCtzljUJxbH .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-Ji7v5wCtzljUJxbH .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-Ji7v5wCtzljUJxbH .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-Ji7v5wCtzljUJxbH .marker{fill:#333333;stroke:#333333;}#mermaid-svg-Ji7v5wCtzljUJxbH .marker.cross{stroke:#333333;}#mermaid-svg-Ji7v5wCtzljUJxbH svg{font-family:"trebuchet ms",verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-Ji7v5wCtzljUJxbH .label{font-family:"trebuchet ms",verdana,arial,sans-serif;color:#333;}#mermaid-svg-Ji7v5wCtzljUJxbH .cluster-label text{fill:#333;}#mermaid-svg-Ji7v5wCtzljUJxbH .cluster-label span{color:#333;}#mermaid-svg-Ji7v5wCtzljUJxbH .label text,#mermaid-svg-Ji7v5wCtzljUJxbH span{fill:#333;color:#333;}#mermaid-svg-Ji7v5wCtzljUJxbH .node rect,#mermaid-svg-Ji7v5wCtzljUJxbH .node circle,#mermaid-svg-Ji7v5wCtzljUJxbH .node ellipse,#mermaid-svg-Ji7v5wCtzljUJxbH .node polygon,#mermaid-svg-Ji7v5wCtzljUJxbH .node path{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-Ji7v5wCtzljUJxbH .node .label{text-align:center;}#mermaid-svg-Ji7v5wCtzljUJxbH .node.clickable{cursor:pointer;}#mermaid-svg-Ji7v5wCtzljUJxbH .arrowheadPath{fill:#333333;}#mermaid-svg-Ji7v5wCtzljUJxbH .edgePath .path{stroke:#333333;stroke-width:2.0px;}#mermaid-svg-Ji7v5wCtzljUJxbH .flowchart-link{stroke:#333333;fill:none;}#mermaid-svg-Ji7v5wCtzljUJxbH .edgeLabel{background-color:#e8e8e8;text-align:center;}#mermaid-svg-Ji7v5wCtzljUJxbH .edgeLabel rect{opacity:0.5;background-color:#e8e8e8;fill:#e8e8e8;}#mermaid-svg-Ji7v5wCtzljUJxbH .cluster rect{fill:#ffffde;stroke:#aaaa33;stroke-width:1px;}#mermaid-svg-Ji7v5wCtzljUJxbH .cluster text{fill:#333;}#mermaid-svg-Ji7v5wCtzljUJxbH .cluster span{color:#333;}#mermaid-svg-Ji7v5wCtzljUJxbH div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:"trebuchet ms",verdana,arial,sans-serif;font-size:12px;background:hsl(80, 100%, 96.2745098039%);border:1px solid #aaaa33;border-radius:2px;pointer-events:none;z-index:100;}#mermaid-svg-Ji7v5wCtzljUJxbH :root{--mermaid-font-family:"trebuchet ms",verdana,arial,sans-serif;}

樱花

梅花

桃花

种子

叶子0-1

绿芽

蓓蕾0-1

叶子2-3

树杈

蓓蕾2-3

叶子4-5

蓓蕾4-5

三、相关问答（个人理解，不一定正确）

Q1: 为什么 Q ( m , n ) Q(m,n) Q(m,n)定义时选择 P r o v e s Proves Proves函数？

A1: 因为选取 P r o v e s Proves Proves函数有利于接下来的不可证明的判定。
Q2: 每个自然数数必然代表一个逻辑表达式或者序列的序列么？

A2: 不一定，或许不是逻辑表达式，也可能是序列的序列的序列，甚至更高级别的嵌套。
Q3: 为什么形式系统 P是不完备的就能说明其他一切可描述自然数的公理体系也是不完备的？

A3: 因为形式系统 P是最简单的可描述自然数的推导体系，其他可描述自然数的公理体系必然也能仿照形式系统 P 构造出不可证明的命题 g g g。
Q4: 哥德尔构造了那么多原始递归谓词和原始递归函数的目的是？

A4: 主要有下面几个原因：
- 这些函数、谓词都是原始递归的，说明它们必然是能通过有限步骤被计算或者证明（根据表现定理）
- 另外Proves谓词是比较复杂的递归函数，需要这么多原始递归的定义
- 这些原始递归的函数、谓词，建立了哥德尔编码和形式系统的映射关系，从而能用自然数代表形式系统，形式系统也可以引用这些这些特别的自然数，从而为构造自我指涉的矛盾建立了雄厚的基础
Q5: 为什么原始递归谓词是存在形式证明的?

A5: 因为表现定理说明了这点
Q6: 为什么找到一个不可证明的命题 g g g就说系统一定不完备，把该命题 g g g设置为公理不就可以说系统完备了？

A6: 因为当系统加入新公理后 P r o v e s Proves Proves函数必然发生改变，从而能构造出新的命题 g g g与原有命题 g g g不同，新系统仍然不完备