⟐ 数学の作り方 How to make Mathematics

第6章 一階の証明体系と健全性

量化子を、規則で動かす

第2章で命題論理の証明体系を作りました。一階述語論理でも同じ精神——公理と推論規則で ⊢\vdash を定める—— ですが、量化子 ∀,∃\forall,\exists を扱う新しい規則が要ります。難しさは前章で見た代入にあります。 「∀x φ\forall x\,\varphi が成り立つなら φ[x:=t]\varphi[x:=t] も成り立つ」を規則にするには、capture を避ける条件が不可欠。

この章では一階の証明体系を立て、命題論理と同じく健全性（⊢⇒⊨\vdash\Rightarrow\models）を証明します。 健全性の証明で、前章の代入補題・一致補題がまさに使われ、「構文の規則が意味論を裏切らない」ことが確認されます。 完全性（逆向き）は次章のゲーデルに委ね、ここは足場固めです。

量化子の推論は代入を伴い、capture 回避の条件が命。健全性の証明で前章の補題が効く。

ヒルベルト系（一階）

命題論理の公理 (A1)–(A3) に、量化子と等号の公理を追加します。推論規則は MP と一般化の2つ。

定義 一階ヒルベルト系

公理図式：(A1)–(A3)（命題論理、φ,ψ,χ\varphi,\psi,\chi は一階の論理式）に加えて (A4) ∀x φ→φ[x:=t](t は x に代入可能),\text{(A4)}\ \forall x\,\varphi\to\varphi[x:=t]\quad(t\ \text{は}\ x\ \text{に代入可能}), (A5) ∀x (φ→ψ)→(φ→∀x ψ)(x∉FV(φ)),\text{(A5)}\ \forall x\,(\varphi\to\psi)\to(\varphi\to\forall x\,\psi)\quad(x\notin\mathrm{FV}(\varphi)), 等号公理：x=xx=x、および x=y→(φ→φ′)x=y\to(\varphi\to\varphi')（φ′\varphi' は φ\varphi の一部の xx を yy に置換）。 推論規則：MP、および一般化（φ\varphi から ∀x φ\forall x\,\varphi を導いてよい）。

(A4) が「全称の除去（具体化）」、(A5) が「全称の導入」を、代入可能性・自由変数の条件つきで担います。 条件を外すと不健全になる：(A4) で tt が代入可能でないと前章の capture 事故が起き、(A5) で x∈FV(φ)x\in\mathrm{FV}(\varphi) だと 「φ\varphi が特定の xx について成り立つ」から「すべての xx で」へ不当にすり替わります。

注意 一般化と演繹定理の注意

一般化があるため、演繹定理はそのままでは成り立たない（φ⊢∀x φ\varphi\vdash\forall x\,\varphi だが ⊢φ→∀x φ\vdash\varphi\to\forall x\,\varphi は 一般には偽）。正しくは「仮定 φ\varphi に自由な xx を含まない限りで一般化してよい」という制限つきで演繹定理が成り立つ。 この微妙さを自動的に処理してくれるのが、次の自然演繹の固有変数条件。

自然演繹の量化子規則

自然演繹では、量化子にも導入・除去規則を対で与えます。核心は ∀\forallI と ∃\existsE に付く固有変数条件です。

定義 量化子の自然演繹規則

∀\forallE（除去）：∀x φ\forall x\,\varphi から φ[x:=t]\varphi[x:=t]（tt 代入可能）。 ∀\forallI（導入）：φ[x:=a]\varphi[x:=a] から ∀x φ\forall x\,\varphi。ただし固有変数条件——aa は結論や 解消されていない仮定に自由に現れない新しい変数。 ∃\existsI：φ[x:=t]\varphi[x:=t] から ∃x φ\exists x\,\varphi。 ∃\existsE：∃x φ\exists x\,\varphi と「φ[x:=a]\varphi[x:=a] を仮定して導いた ψ\psi」から ψ\psi。ただし aa は φ,ψ\varphi,\psi や他の未解消仮定に自由に現れない新しい変数（固有変数条件）。

固有変数条件の意味は「任意に選んだ代表 aa」。∀\forallI は「aa について何の前提も置かずに φ(a)\varphi(a) を示せたなら、 aa は本当に任意だったのだから ∀x φ\forall x\,\varphi」。aa が仮定に現れていたら「任意」ではなくなるので禁止。 ∃\existsE は「∃x φ\exists x\,\varphi の証人を aa と名づけ、その aa について（aa の素性を使わずに）ψ\psi を導けば ψ\psi」。 例として ∀x(P(x)→Q(x))→(∀x P(x)→∀x Q(x))\forall x(P(x)\to Q(x))\to(\forall x\,P(x)\to\forall x\,Q(x)) を導きます。

[∀x(P(x)→Q(x))]2[\forall x(P(x)\to Q(x))]_2
∀E
P(a)→Q(a)P(a)\to Q(a)
[∀x P(x)]1[\forall x\,P(x)]_1
∀E
P(a)P(a)
→E
Q(a)Q(a)
∀I
∀x Q(x)\forall x\,Q(x)
→I, 1
∀x P(x)→∀x Q(x)\forall x\,P(x)\to\forall x\,Q(x)
→I, 2
∀x(P(x)→Q(x))→(∀x P(x)→∀x Q(x))\forall x(P(x)\to Q(x))\to(\forall x\,P(x)\to\forall x\,Q(x))

∀\forallE で代表 aa について P(a)→Q(a)P(a)\to Q(a) と P(a)P(a) を取り出し、MP で Q(a)Q(a)。ここで aa は未解消仮定 ∀x(P(x)→Q(x)), ∀x P(x)\forall x(P(x)\to Q(x)),\ \forall x\,P(x) に自由に現れない（どちらも xx を束縛）ので、固有変数条件を満たし ∀\forallI で ∀x Q(x)\forall x\,Q(x)。最後に →\toI を2回。**「任意の代表で示す→一般化」**という数学の日常的な論法が、 そのまま規則になっているのが分かります。

健全性定理

定理 健全性定理（一階）

Γ⊢φ⇒Γ⊨φ\Gamma\vdash\varphi \Rightarrow \Gamma\models\varphi。

証明

ヒルベルト系で示す。Γ⊢φ\Gamma\vdash\varphi の証明の各項が、Γ\Gamma の任意のモデル M\mathcal M と任意の付値 ss で 「M⊨Γ[s]\mathcal M\models\Gamma[s] ならば当該項が [s][s] で真」を満たすことを、証明の長さの帰納法で示す （正確には、自由変数を許すため「Γ\Gamma を全付値で真にする M\mathcal M では、証明の各項も全付値で真」を示す）。

公理が妥当であることを各図式について確認する。命題論理由来 (A1)–(A3) はトートロジーゆえ妥当。

  • (A4) ∀x φ→φ[x:=t]\forall x\,\varphi\to\varphi[x:=t]：M⊨∀x φ[s]\mathcal M\models\forall x\,\varphi[s] なら、定義よりすべての aa で M⊨φ[s[x:=a]]\mathcal M\models\varphi[s[x:=a]]。特に a=tM,sa=t^{\mathcal M,s} ととり、代入補題（前章）で M⊨φ[x:=t][s]\mathcal M\models\varphi[x:=t][s]。ここで tt の代入可能性が代入補題の適用に必須。
  • (A5) ∀x(φ→ψ)→(φ→∀x ψ)\forall x(\varphi\to\psi)\to(\varphi\to\forall x\,\psi)（x∉FV(φ)x\notin\mathrm{FV}(\varphi)）：前件と φ\varphi を仮定。 任意の aa について M⊨(φ→ψ)[s[x:=a]]\mathcal M\models(\varphi\to\psi)[s[x:=a]]。x∉FV(φ)x\notin\mathrm{FV}(\varphi) ゆえ一致補題で M⊨φ[s[x:=a]]  ⟺  M⊨φ[s]\mathcal M\models\varphi[s[x:=a]]\iff\mathcal M\models\varphi[s]（真）。よって M⊨ψ[s[x:=a]]\mathcal M\models\psi[s[x:=a]] が すべての aa で成り立ち、M⊨∀x ψ[s]\mathcal M\models\forall x\,\psi[s]。
  • 等号公理は =M=^{\mathcal M} が真の同一性であることから従う。

推論規則が妥当性を保つこと：MP は →\to の真理値規則から（命題論理と同じ）。一般化は、 M⊨φ[s′]\mathcal M\models\varphi[s'] がすべての付値 s′s' で成り立つなら、特にすべての aa で s′=s[x:=a]s'=s[x:=a] ととれ、 M⊨∀x φ[s]\mathcal M\models\forall x\,\varphi[s]。よって全付値で真が保たれる。

以上より証明の各項は妥当性を保ち、Γ⊨φ\Gamma\models\varphi。∎

健全性の証明で、前章の代入補題が (A4) を、一致補題が (A5) と一般化を支えているのが要点です。 量化子の公理・規則に付いた条件（代入可能性・x∉FV(φ)x\notin\mathrm{FV}(\varphi)・固有変数条件）は、まさにこれらの補題が 適用できるための条件で、構文の細かい制約が意味論の健全性に直結していることが見えます。飾りではなかったのです。

つまずきポイント

注意 よくある誤解

  • 一般化は仮定つきでは自由に使えない。 φ⊢∀x φ\varphi\vdash\forall x\,\varphi は「φ\varphi が仮定なしに（または xx を自由に含まない仮定から）導けた」ときのみ妥当。固有変数条件がこの制約を明示化する。
  • (A4) の代入可能性を落とすと不健全。 capture が起きると (A4) は妥当でなくなる。前章の代入可能性はここで効く。
  • 健全性は易しい、完全性は難しい。 一階でも健全性は素直な帰納法。逆向き（妥当なら導ける）が次章ゲーデルの大仕事。

この章のまとめ

  • 一階ヒルベルト系は命題公理＋(A4) 全称除去・(A5) 全称導入・等号公理、規則は MP と一般化。量化子の公理には代入可能性・自由変数の条件が必須。
  • 自然演繹の ∀\forallI・∃\existsE には固有変数条件（任意の代表を表す新変数）が付く。「任意の代表で示して一般化」という数学の論法の形式化。
  • 健全性（⊢⇒⊨\vdash\Rightarrow\models）は証明の長さの帰納法で示せ、(A4) には代入補題、(A5)・一般化には一致補題が効く。構文の制約が意味論の健全性を保証する。

次章は、この分野の頂点——ゲーデルの完全性定理（⊨⇒⊢\models\Rightarrow\vdash）を、ヘンキンの構成で完全に証明します。