VIII. 自然演繹（その２）

前章に引き続いて自然演繹による形式化を扱う．前半では NKの完全性を命題論理の場合に証明する．後半では 自然演繹における述語論理の取り扱いを説明する．

目次

1. 命題論理の形式化の完全性
2. 述語論理の形式化
3. 理論・モデル・完全性定理

総目次に戻る

1. 命題論理の形式化の完全性

この節の目標はNKの完全性を命題論理の場合に証明すること である．証明は二つの部分からなる．前半では，論理式の 真理値と演繹可能性の関係についての補助定理を証明する． 後半では，この補助定理を排中律と組み合わせて完全性の 証明を完成する．なお，ここで示す証明は前原昭二 「記号論理学入門」（日本評論社，1967）の付録IIIに基づく．

1.1 補助定理と完全性定理

補助定理
論理式φは m+n 個の命題記号 p1, ..., pm, q1, ..., qn 以外の命題記号を含まないとする． さらに， M[pi] = T (i = 1, ..., m), M[qj] = F (i = 1, ..., n) という真理値割り当て M および Γ = {p1,...,pm,¬q1,...,¬qn} という論理式の集合 Γ を考える．このとき次のことが成立する：
  1. M[φ] = T ならば Γ |- φ ．
  2. M[φ] = F ならば Γ |- ¬φ ．

完全性定理
任意の論理式φに対して |= φ ならば |- φである． すなわち，任意の恒真論理式はNKにおいて証明できる．

【注意】

  1. これらはいずれも「正しいものは証明できる」という主張である． 補助定理は，特定の真理値割り当て M のもとで真あるいは偽になること （意味論の記法では M |= φ あるいは M |= ¬φ）から， それに対応する演繹関係（Γ |- φあるいは Γ |- ¬φ） が従うことを主張している．Γが真理値割り当て M に対応する条件である ことに注意されたい．

  2. 以下に示す補助定理の証明は排中律を用いないので， 補助定理は実はNJの中で成立する主張である．ただし， {T,F} という２値真理値集合について述べているだけなので， 直観主義論理としての完全性の主張にはなっていない． 完全性定理は補助定理と排中律を組み合わせることによって 証明される．

  3. NJは直観主義論理の形式化であるから， その完全性を議論するにはハイティング代数 （たとえば３値真理値集合 {T,M,F}） による意味解釈を考えなければならない． 恒真性 |=φ の意味も古典論理と異なり， すべてのハイティング代数とその上の任意の真理値割り当てに対して φの真理値が T であること，と定義される． たとえば排中律φ∨¬φはその意味では恒真ではない． NJはこのような直観主義論理の意味解釈に関して 健全かつ完全である（詳しくは， 前章の最後の節で紹介した参考書などを参照されたい）．

  4. 述語論理の場合のNKの完全性は内容も証明も命題論理の場合に比べて はるかに大掛かりなものになる．これについては後の節で説明する．

1.2 補助定理の証明

証明はφに含まれる論理結合子（∧，∨，¬，→）の個数についての 数学的帰納法による．

【注意】これは典型的な「構造帰納法」の証明である． 要は，与えられた論理式φを ψ1∧ψ2，ψ1∨ψ2， ¬ψ，ψ1→ψ2の四つの場合に分けて， 問題を部分論理式に還元して行くことにある．なお，ここでは 論理結合子として↔を含めていないが，↔を含む形に定式化し直す こともできる（その場合にはNKの推論規則にも↔に関するものを 用意しておかなければならない）．

第１段：まずφが論理記号を含まない場合を考える． これには次の三つの場合がある．

  1. φ = ⊥
  2. φ = pi
  3. φ = qj
φ = ⊥の場合には M[φ] = F だから補助定理の主張２に 該当するが，
[⊥]
¬⊥		 （¬導入）
という推論（これは¬導入の特別な形で，⊥を前提に置いてから， それを帰結とみなしてただちに仮定として落としている） によって |- ¬⊥ = ¬φ がわかる． φ = pi の場合には M[φ] = T だから 主張１に該当するが，明らかにΓ |- pi であるから，主張１は確かに成立する． φ = qj の場合には M[φ] = F だから 主張２に該当するが，この場合も Γ |- ¬qj から主張２が成立することがわかる．

第２段：論理結合子の個数が n 未満の場合に補助定理が 成立すると仮定して，n の場合にも成立することを示す． これは次の四つの場合に分かれる．

  1. φ = ψ1∧ψ2
  2. φ = ψ1∨ψ2
  3. φ = ¬ψ
  4. φ = ψ1→ψ2
それぞれの場合について考える．

1. φ = ψ1∧ψ2の場合

2. φ = ψ1∨ψ2の場合

3. φ = ¬ψ の場合

4. φ = ψ1→ψ2 の場合

こうして四つの場合のいずれについても補助定理の主張が成立する ことが示された．（補助定理の証明終わり）

1.3. 完全性定理の証明

論理式φが恒真である（|= φ）とする．φに含まれる命題記号を p1, ..., pn とする．以下， ψ1, ..., ψnはそれぞれ

ψi = pi または ψi = ¬pi

のいずれかをあらわすものとする．任意の真理真理値割り当て M に対して φの真理値は T であるから，補助定理からの帰結として， ψ1, ..., ψn の 2n 通りの 選び方のすべてにわたって

{ψ1, ..., ψn} |- φ

が成立することになる．これを

{ψ1, ..., ψn-1,pn} |- φ,      {ψ1, ..., ψn-1,¬pn} |- φ

というように二組に分けて，排中律の特別な場合 pn∨¬pn と組み合わせれば， ∨除去を用いる推論

pn∨¬pn（排中律）     
[pn]1
：
φ		    [¬pn]1
：
φ
1（∨除去）
φ
によって

{ψ1, ..., ψn-1} |- φ

が得られる．これを再び

{ψ1, ..., ψn-2,pn-1} |- φ,      {ψ1, ..., ψn-2,¬pn-1} |- φ

というように二組に分けて上と同様の議論を行えば

{ψ1, ..., ψn-2} |- φ

が得られる．これを繰り返せば最後に

|- φ

が得られる．これが証明すべきことだった．（完全性定理の証明終わり）

2. 述語論理の形式化

自然演繹による述語論理の形式化（命題論理の場合と同様， これも「NK」および「NJ」と呼ばれる）は， 新たに量化子∀，∃に関する推論規則が加わることを除けば， 命題論理の場合と見かけ上ほとんど変わらない．

古典論理の形式的体系 NK 直観主義論理の形式的体系 NJ
公理系 排中律 なし
推論規則 論理記号の導入・除去の規則と⊥の規則 論理記号の導入・除去の規則と⊥の規則

2.1 論理式

自然演繹による述語論理の形式化では 次のものからなる論理式を扱う．

論理式の構成要素

命題論理の場合の命題記号に代わるものが述語論理の原子論理式である． 命題論理の命題記号は内部構造をもたない文字通りの「原子」 （atom --- 本来は「分割不可能」を意味する）だが， 述語論理では（現実の原子が電子と原子核からできているように） そこに内部構造を持ち込む．述語論理の原子論理式については 意味論の解説の中で詳しく説明したが，その要点は次の通りである．

量化子も命題論理から述語論理への移行に伴って加わる 新たな要素である．量化子は ∀x, ∃x というように変数記号を修飾する ものであるが，その使い方や意味は意味論の解説の中で説明したので ここでは繰り返さない．注意しなければならないのは次の二種類の 変数の区別である．

たとえば，∀x∃yP(x,y,z) という論理式 --- これは ∀x(∃yP(x,y,z)) を略記したものである --- では x, y が束縛変数で z が自由変数である． これはわかりやすい例だが，一つの論理式の中で同じ変数記号が 別の役割を演じる場合も起こり得る． たとえば，(∀x∃yP(x,y,z))∧Q(x,z) という論理式を考えると， 最初の (∀x∃yP(x,y,z)) の部分の x は束縛変数だが， 次の Q(x,z) の部分の x は自由変数である．要するに， ある変数記号が束縛変数であるか自由変数であるかは， 一般にはその論理式全体で決まらず，変数記号の出現位置あるいは 視野に依存する．

なお，ゲンツェンは自由変数と束縛変数を

というように記号上区別している．これに習えば，上で採り上げた 例は (∀x∃yP(x,y,a))∧Q(b,c) というようにかなりわかりやすくなる （a,b,c が自由変数）．これは便利な記法なので以下でも利用する． もちろんこの記法のもとでも ∀x(∀x∃yP(x,y,a))∧Q(x,c)) というように，変数の束縛の関係が複雑に入り組んでいる場合には 注意が必要である．

2.2 公理系と推論規則

公理系と推論規則を示す．
公理系
NKの場合：φ∨¬φ（排中律）（φは任意の論理式）
NJの場合：なし

推論規則
推論規則はNK・NJ共通である．命題論理の場合と同じ形の推論規則 （論理結合子∧，∨，¬，→に関する導入・除去の規則と⊥の規則）に加えて， 述語論理では量化子に関する以下のような導入・除去の規則を用意する （φ，ψは任意の論理式）．
φ[a / x] （a：自由変数）
（∀導入）
∀xφ
    
∀xφ
（∀除去）
φ[t / x] （t：項）
φ[t / x] （t：項）
（∃導入）
∃xφ
    
　
∃xφ      [φ[a / x]]
：
ψ		 （a：自由変数）
（∃除去）
ψ
ただし， ∀導入と∃除去の規則に現れる自由変数 a は次のような条件 （固有変数条件）を満たさなければならない．

  1. ∀導入の場合： a はφ[a / x] が依存する前提に自由変数として現れない．
  2. ∃除去の場合： a は，ψが依存するφ[a / x] 以外の前提に自由変数として現れない．

[φ[a / x]] は前提として置いたφ[a / x] が仮定として落ちることを示している．

【注意】
  1. φ[a / x], φ[t / x] はそれぞれφの中の x を a と t に 置き換えたものである．上の推論規則はφをφ(x)，φ[a / x] をφ(a)， φ[t / x] をφ(t) とあらわして次のように書き直す方が少し見やすくなる （これは一種の簡略記法で，正式の書き方とは言えないが）．
    φ(a) （a：自由変数）
    		（∀導入）
    ∀xφ(x)
    		    
    ∀xφ(x)
    		（∀除去）
    φ(t) （t：項）
    φ(t) （t：項）
    		（∃導入）
    ∃xφ(x)
    		    
    ∃xφ(x)      [φ(a)]
    ：
    ψ    		 （a：自由変数）
    		（∃除去）
    ψ
  2. 固有変数条件の意味については，このあとすぐに説明する．

2.3 推論規則の意味・妥当性

量化子の除去・導入規則以外は命題論理の場合と同じものなので 説明は省く．量化子の除去・導入規則について説明する．

1. ∀除去と∃導入はわかりやすい．ここに現れている項 t は 一つの「例」と考えればよい．

もちろん何れも妥当な推論である．

2. ∀導入と∃除去では固有変数条件という煩わしいものを 考慮しなければならないが，これらも次のような意味で ごく自然な推論である．

以上の説明から∀導入と∃除去の妥当性もわかるだろう（正式には 意味論的枠組に基づいてきちんと確かめるべきだが，ここでは省略する）．

2.4 証明・演繹の簡単な例

【例１】次は束縛変数の「α変換」（述語論理の意味論の章参照） に他ならない．
  1. ∀xφ |- ∀yφ[y / x]
  2. ∃xφ |- ∀yφ[y / x]
１は次のように導出できる：
1: ∀xφ（前提）
2: φ[a / x] （1∀除去，a は自由変数）
3: ∀yφ[y / x] （2∀導入）
２行目を導出するときには自由変数 a を項とみなして∀除去を適用している． ３行目を導出するときには a を変数 y に置き換える形で∀導入を適用している． このとき固有変数条件は明らかに満たされている．

２は次のように導出できる：

1: ∃xφ（前提）
2: [φ[a / x]]4 （前提，a は自由変数）
3: ∃yφ[y / x] （2∃導入）
4: ∃yφ[y / x] （1, 3∃除去）
４行目に移るときに a の固有変数条件が満たされていることに注意されたい．

【例２】∀x(φ→ψ)∧φ[t / x] |- ψ[t / x] （t は項）

これは「人はみな死ぬ．ソクラテスは人である．したがって ソクラテスは死ぬ．」という有名な三段論法のもじりである． なお，量化子は¬と同じ優先順位をもつので（述語論理の意味論の章を 参照されたい）∀x(φ→ψ)∧φ[t / x] は(∀x(φ→ψ))∧φ[t / x] の意味である．導出は次のとおり：

1: ∀x(φ→ψ)∧φ[t / x] （前提）
2: ∀x(φ→ψ) （1∧除去）
2: φ[t / x] → ψ[t / x] （2∀除去）
3: φ[t / x] （1∧除去）
4: ψ[t / x] （2,3→除去）

【例３】∀x(φ→ψ)∧∀x(ψ→χ) |- ∀x(φ→χ)

基本的な考え方は例２と同様である：

1: ∀x(φ→ψ)∧∀x(ψ→χ) （前提）
2: [φ[a / x]]9 （前提）
3: ∀x(φ→ψ) （1∧除去）
4: φ[a / x]→ψ[a / x] （3∀除去，a は自由変数）
5: ∀x(ψ→χ) （1∧除去）
6: ψ[a / x]→χ[a / x] （5∀除去）
7: ψ[a / x] （2, 4→除去）
8: χ[a / x] （6, 7→除去）
9: φ[a / x]→χ[a / x] （2,8 →導入）
10: ∀x(φ→χ) （9∀導入）
最後の段階で∀導入を行うため固有変数条件に注意しなければならない．

【注意】この例はアリストテレスの定言三段論法 （「定言言明」という形の言明に関する三段論法）と呼ばれる ものの一つである．定言言明には A, I, E, O と略記される 次の４つの型がある

A（全称肯定）：すべての S は P である．
I（特称肯定）：ある S は P である．
E（全称否定）：すべての S は P でない．
O（特称否定）：ある S は P でない．
アリストテレスは三つの性質（S, M, P）を含む定言三段論法の あらゆる可能な形（全部で２５６通りある）を調べて，そのうち １９通りが正しい推論であると結論した．また，定言言明の間の 直接的演繹関係も調べたが，アリストテレスが正しいと判断した 演繹の中には今日の視点から見て間違っているものが含まれている．

2.5 基本的な定理・演繹

以下，NJあるいはNKの中で証明できる基本的な論理式をいくつか示す． 右端に NJ と書いたものは NJ の中で（すなわち排中律を用いずに） 証明できる．A↔B は (A→B)∧(B→A) を略記したものと解釈されたい．

例として，∃x¬φ→¬∀xφ とその逆 ¬∀xφ→∃x¬φ の 証明を示す．

|- ∃x¬φ→¬∀xφ の証明：

1: [∃x¬φ]8 （前提）
2: [∀xφ]7 （前提）
3: [¬φ[a / x]]6 （前提，a は自由変数）
4: φ[a / x] （2∀除去）
5: ⊥ （3,4¬除去）
6: ⊥ (1,3,5∃除去）
7: ¬∀xφ （2,6¬導入）
8: ∃x¬φ→¬∀xφ （1,7→導入）

ここでは確かに排中律を使っていない．ちなみに， ６行目で∃除去を適用するときに a について固有変数条件が 満たされていることに注意されたい．５の論理式が依存する前提は １，２，３であるが，その中で a を含むのは３だけである． ４は a を含むが，これは前提ではなくて前提から導かれた ものだから問題ないのである．

|- ¬∀xφ→∃x¬φ の証明：

1: [¬∀xφ]12 （前提）
2: [¬∃x¬φ]10 （前提）
3: [¬φ[a / x]]6 （前提，a は自由変数）
4: ∃x¬φ （3∃導入）
5: ⊥ （2,4¬除去）
6: ¬¬φ[a / x] （3,5¬導入）
7: φ[a / x] （6二重否定除去）
8: ∀xφ （7∀導入）
9: ⊥ （1,8¬除去）
10: ¬¬∃x¬φ （2,9¬導入）
11: ∃x¬φ （10二重否定除去）
12: ¬∀xφ→∃x¬φ

この証明は非常に技巧的である．これ以外の証明もあり得るが， やはりかなりの技巧を要するだろう．なお，以下の点には特に 注意されたい．

  1. 証明の見通しをよくするため途中で二重否定除去 ¬¬φ|-φ を 推論規則として使っている．正式には二重否定除去の証明 （ここで排中律を使う）
    1: ¬¬φ （前提）
    2: φ∨¬φ （排中律）
    3: [¬φ]7 （前提）
    4: ⊥ (1,3¬除去）
    5: φ （4⊥）
    6: [φ]7 （前提）
    7: φ （2,3,5,6 ∨除去）
    に相当するものを挿入する必要がある．結果として， 本当の証明はかなり長くなる．

  2. ∀導入で８行目を導くには７行目の論理式が依存する前提 において固有変数条件が満たされていなければならないが， これは確かにそうなっている．実際．７行目の論理式が依存する 前提は１行目と２行目だけで，それは a を含んでいないからである． ３行目に置いた前提は６行目で¬導入を適用した際に仮定として 落ちているので，ここでは考えなくてよい．

【演習問題】この二つ以外の場合についても証明を与えよ （すべてNJの範囲で証明できる）．

３. 理論・モデル・完全性定理

述語論理は，元々，自然数論を始めとする数学の諸理論を 論理構造に注目して記述し直す枠組として生まれた． そこでは，数学的な言明や主張は論理式に記号化され， 数学的推論・証明も論理式で表現される．同様の考え方は 数学以外の知識体系にも当てはまる．これまでの議論は そのような知識体系から「推論」や「証明」の仕組のみを 抽出して論じたものということができる．実際には， 数学の理論をはじめとするさまざまな知識体系は その体系固有の「公理」（排中律などの「論理的公理」 と区別する意味で「非論理的公理」と呼ばれる） とそこから導出される「定理」をもっている．この節では， このような知識体系固有の公理や定理（その集まりを一般的に 「理論」と呼ぶ）の取り扱いを議論する． なお，意味論的側面も考えなければならないので， 以下では議論を古典述語論理に限定する．

3.1 意味論的演繹と形式的演繹

一般に閉論理式の集合を「理論」という．論理式を構成する （論理記号以外の）記号の集合Ｌを明示するときには「Ｌ上の理論」 ともいう．閉論理式のみを考えるのは，閉論理式が一つの完成した 「文」とみなせるからである．このように一般的に捉えた「理論」には， 数学の理論の公理系のようなものを指す場合もあれば， その公理系から導かれるすべての定理の集まりを考える場合もある． その中間の，公理系と既に証明された定理の集まりを指す場合もある．

このような理論Ｔからある閉論理式φを論理的に導出すること （すなわち「演繹」）には，意味論的な考え方と 形式的・構文論的な考え方とがある． この二つはどのような関係にあるのだろうか．

意味論的な論理の考え方では，普通の数学と同様に， 論理式の中に含まれる定数記号・関数記号・述語（関係）記号 に対して集合・写像に基づく意味解釈を与え， それに基づいて推論や証明を進める． その詳細は述語論理の意味論の章で説明した． その要点を要約すれば次のようになる．

他方，形式化された論理の考え方では，演繹は論理式に対する 純然たる記号的操作として定式化され，そこに含まれている 記号の意味解釈には立ち入らない． この意味でφがＴから演繹されることを Ｔ|-φ と表わす． 「健全性」と「完全性」は形式化された論理体系の 演繹能力に関する概念であり，次のように定式化される：

また，命題論理の場合と同様に，Ｔを空にして 証明可能性 |-φ と恒真性 |=φ の関係に関する主張 として定式化することもある．述語論理の応用の観点から見れば， 理論Ｔを明示する形で定式化する方が自然であるが， 実際にはこれらは同等の主張である．

述語論理（正確には「１階述語論理」）に対するヒルベルト流・ 自然演繹のいずれの形式化も上の意味で健全かつ完全である， ということが知られている．このうち，健全性を確かめることは それほど難しくない（本質的には推論規則の妥当性からの帰結である）が， 完全性を証明するには高度な技法が必要になる．実際には， ヘンキン（Leon Henkin）に従って，上の主張をさらに強めた形で 完全性を定式化して証明することが多い．次節では そのような形に定式化された完全性定理を紹介する．

【注意】ここで考えているのは「論理体系の完全性」であるが， これと言葉が似ていて混同しやすい概念として「理論の完全性」がある． Ｌ上の任意の論理式φに対してT|-φあるいはＴ|-¬φのいずれかが成立するとき， 「理論Ｔは完全である」という．この二つの完全性は内容的にも概念的にも まったく異なるものなので注意されたい．たとえば， 「ゲーデルの完全性定理」はヒルベルト流の述語論理の形式化の 上の意味での完全性を主張するものであるが，同じゲーデルの 「（第一）不完全性定理」は自然数論（言い換えればペアノ算術の公理系） を含む（後述の意味で無矛盾な）理論の不完全性を主張するものである．

3.2 無矛盾性とモデルの存在

ヘンキンが示した強い形の完全性（ならびにそれと対をなす健全性）は 理論の「無矛盾性」の概念を用いて定式化される．

【定義】理論Ｔに対してＴ|-⊥が成立するとき， Ｔは「矛盾する」という．そうでないとき Ｔは「無矛盾である」という．

【注意】自然演繹は矛盾を表わす特殊記号⊥を用意しているので 矛盾・無矛盾性をこのように定義できる． このような記号を用意していない形式化では⊥の代わりに φ∧¬φという形の論理式が演繹されることを「矛盾する」 と定義すればよい．

強い形の完全性定理（ならびにそれにあわせて書き直した健全性定理） の主張は次のようになる．

強い形の完全性・健全性
ヒルベルト流・自然演繹のいずれによる述語論理の形式化も この強い意味での完全性・健全性をもつことが知られている． また，後で説明するように，前節の意味での完全性・健全性が これから従うことも容易に確かめられる．

ちなみに，強い形の健全性の内容は「Ｔが矛盾すればモデルは存在しない」 という対偶の形に書き直してみればほとんど明らかなことである． （実際，Ｔが矛盾すればＴ|-⊥となるが，素朴な形の健全性を使えば これからＴ|=⊥が従うから，ＴのモデルＭは⊥を充足しなければならない． しかし⊥は意味解釈上恒偽だから，それを充足するモデルは存在しない．） これとは対照的に，ヘンキン流の完全性定理の証明は抽象的でやや難解である． ヘンキン流の完全性定理の証明については

などを参照されたい．また，述語論理の完全性を示すには， 定式化の違いも含めて，この他にもいろいろな方法がある． それらについては などを参照されたい．

最後に，強い形の完全性から前述の素朴な形の完全性が従う， ということを確かめておこう．準備として，まず次のことを示す．

【補題１】Ｔを任意の理論，φを任意の閉論理式とする． このときNKにおいて次の二つの主張は同値である．

  1. Ｔ|-φである．
  2. Ｔ∪{¬φ}は矛盾する．

【注意】これは要するに一種の背理法である． 計算機による定理証明の分野で「反駁法」と呼ばれる考え方にも通じる．

【証明】１から２が従うこと：　 Ｔ|-φならばＴ∪{¬φ}からφと¬φの両方が導びかれる． したがって¬除去によって⊥が導出される．つまりＴ|-⊥．

２から１が従うこと：　 Ｔ∪{¬φ}が矛盾する，つまりＴ∪{¬φ}|-⊥とする． これはＴを大前提として¬φから⊥が導かれることを意味するから， ¬導入によって¬¬φが導かれる．つまりＴ|-¬¬φが成立する． これと二重否定除去¬¬φ|-φを組み合わせるとＴ|-φがわかる． （証明終わり）

【補題２】Ｔを任意の理論，φを任意の閉論理式とする． このときNKにおいて次の二つの主張は同値である．

  1. Ｔ|=φである．
  2. Ｔ∪{¬φ}のモデルは存在しない．
【証明】１から２が従うこと：　 Ｔ|=φとする．Ｔ∪{¬φ}のモデルが存在すれば， それはＴと¬φをともに充足しなければならないが， Ｔ|=φだからＴの任意のモデルＭはφも充足するので， ¬φを充足することができない．つまりＴ∪{¬φ} のモデルは存在し得ない．

２から１が従うこと：　 Ｔ∪{¬φ}のモデルが存在しないとする．このとき 任意のＬ構造Ｍに対してＭ|=ＴとＭ|=¬φは両立しない． 特にＭ|=Ｔが成立すればＭ|=¬φは成立しない． ところで，φは閉論理式だから，Ｍによる意味解釈のもとで 真理値Ｍ[¬φ]は T（真）, F（偽）のいずれかに確定する． したがって，「Ｍ|=¬φでない」は Ｍ[¬φ] = F と同値， 言い換えれば「Ｍ|=φ」は Ｍ[φ] = T と同値である． このようにして，Ｍ|=ＴからＭ|=φ が従うことがわかる． （証明終わり）

以上の準備の下で，強い形の完全性から素朴な形の完全性を導ける． 補題１によって「Ｔ|-φ」は「Ｔ∪{¬φ}は矛盾する」と同値である． また補題２によって「Ｔ|=φ」は「Ｔ∪{¬φ}はモデルをもたない」と同値である． したがって素朴な形の完全性の主張「Ｔ|=φならばＴ|-φ」は 「Ｔ∪{¬φ}がモデルをもたないならば，Ｔ∪{¬φ}は矛盾する」と同値になる． その対偶は「Ｔ∪{¬φ}が無矛盾ならばＴ∪{¬φ}はモデルをもつ」となる． これは強い形の完全性の特別な場合である．したがって， 強い形の完全性が成立すればこの主張も成立することになる． これが示したいことだった．

キーワード

完全性定理，構造帰納法，原子論理式，述語記号，項， 定数記号，変数記号，函数記号，量化子，束縛変数，自由変数， 量化子の導入・除去規則，固有変数条件，仮の変数， 論理的公理・非論理的公理，意味論的演繹・形式的演繹， 理論，モデル，論理体系の完全性・健全性，理論の完全性， 矛盾・無矛盾，強い形の完全性・健全性