⟐ 数学の作り方 How to make Mathematics

第2章 証明体系 — ヒルベルト系と自然演繹

「真偽」を見ずに、「正しさ」を組み立てる

前章の ⊨\models は、あらゆる付値を調べる意味論的な正しさでした。でも数学者が実際に証明を書くとき、 真理値表を埋めてはいません。公理から出発し、決められた推論規則で一歩ずつ式を導く—— 純粋に記号の操作だけで進みます。

この「記号操作としての証明」を厳密に定義するのが、この章の目標です。真偽の意味を一切参照せず、 機械的に適用できる規則だけで「導ける（⊢\vdash）」を定める。すると証明そのものが数学的対象になり、 「証明とは有限の記号列だ」と言い切れます。この対象化こそ、後にゲーデルが証明を数に変換して 不完全性定理を証明する（第13章）ための土台です。まずは公理の少ないヒルベルト系から始めます。

⊢\vdash は「公理から推論規則で機械的に導ける」という構文的な正しさ。意味 ⊨\models とは独立に定義する。

ヒルベルト系

結合子を →\to と ¬\lnot に絞り（他は略記 φ∨ψ:≡¬φ→ψ\varphi\lor\psi:\equiv\lnot\varphi\to\psi 等）、公理は3つの公理図式、 推論規則はただ一つ モーダス・ポネンス（MP） だけにします。

定義 ヒルベルト系 H

任意の論理式 φ,ψ,χ\varphi,\psi,\chi に対する次の3つを公理図式とする： (A1) φ→(ψ→φ),(A2) (φ→(ψ→χ))→((φ→ψ)→(φ→χ)),\text{(A1)}\ \varphi\to(\psi\to\varphi),\quad \text{(A2)}\ (\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi)), (A3) (¬ψ→¬φ)→(φ→ψ).\text{(A3)}\ (\lnot\psi\to\lnot\varphi)\to(\varphi\to\psi). 推論規則はモーダス・ポネンスのみ：φ\varphi と φ→ψ\varphi\to\psi から ψ\psi を導いてよい。

定義 証明と導出可能性

Γ\Gamma からの証明とは、各項が「公理」「Γ\Gamma の要素」「先行する2項からの MP」のいずれかであるような 有限列 φ1,…,φn\varphi_1,\dots,\varphi_n のこと。φn=φ\varphi_n=\varphi のとき Γ⊢φ\Gamma\vdash\varphi（φ\varphi は Γ\Gamma から導出可能）と書く。 ∅⊢φ\varnothing\vdash\varphi は ⊢φ\vdash\varphi と略す。

公理がわずか3図式、規則が1つ。これで本当に論理が尽くせるのか——尽くせます（次章の完全性）。 まずは体系の“動き”を、いちばん基本的な定理 ⊢φ→φ\vdash\varphi\to\varphi の証明で体感しましょう。 一見自明なこの式すら、公理と MP だけで導くには工夫が要ります。

例 ⊢ φ→φ の形式的証明

次の5行がヒルベルト系での完全な証明である（ψ\psi は任意、例えば φ\varphi 自身でよい）：

  1. (φ→((φ→φ)→φ))→((φ→(φ→φ))→(φ→φ))\big(\varphi\to((\varphi\to\varphi)\to\varphi)\big)\to\big((\varphi\to(\varphi\to\varphi))\to(\varphi\to\varphi)\big) — (A2) で ψ:=φ→φ, χ:=φ\psi:=\varphi\to\varphi,\ \chi:=\varphi
  2. φ→((φ→φ)→φ)\varphi\to((\varphi\to\varphi)\to\varphi) — (A1) で ψ:=φ→φ\psi:=\varphi\to\varphi
  3. (φ→(φ→φ))→(φ→φ)(\varphi\to(\varphi\to\varphi))\to(\varphi\to\varphi) — 1,2 に MP
  4. φ→(φ→φ)\varphi\to(\varphi\to\varphi) — (A1) で ψ:=φ\psi:=\varphi
  5. φ→φ\varphi\to\varphi — 3,4 に MP

φ→φ\varphi\to\varphi ですらこの手間。ヒルベルト系は「公理が少なく、体系を論じる（メタ定理を証明する）のに向く」 反面、「実際に証明を書くのは苦しい」体系です。書く苦しさを救うのが、次の演繹定理です。

演繹定理：仮定を →\to に畳み込む

前章で「Γ,φ⊨ψ  ⟺  Γ⊨φ→ψ\Gamma,\varphi\models\psi \iff \Gamma\models\varphi\to\psi」を見ました。これの構文版が成り立つことを、 証明の構造に関する帰納法で示します。これは「メタ定理」——体系そのものについての定理——の典型例です。

定理 演繹定理

Γ∪{φ}⊢ψ  ⟺  Γ⊢φ→ψ\Gamma\cup\{\varphi\}\vdash\psi \iff \Gamma\vdash\varphi\to\psi。

証明

(⇐)(\Leftarrow) は易しい：Γ⊢φ→ψ\Gamma\vdash\varphi\to\psi の証明に φ\varphi（仮定）を足し、MP で ψ\psi を得る。

(⇒)(\Rightarrow) が本題。Γ∪{φ}⊢ψ\Gamma\cup\{\varphi\}\vdash\psi の証明 θ1,…,θn=ψ\theta_1,\dots,\theta_n=\psi の各項 θk\theta_k について、 Γ⊢φ→θk\Gamma\vdash\varphi\to\theta_k を kk に関する帰納法で示す。各 θk\theta_k は次のいずれか：

(i) θk\theta_k が公理、または Γ\Gamma の要素のとき。 θk\theta_k と、(A1) の θk→(φ→θk)\theta_k\to(\varphi\to\theta_k) に MP して Γ⊢φ→θk\Gamma\vdash\varphi\to\theta_k。

(ii) θk\theta_k が仮定 φ\varphi 自身のとき。 前章の ⊢φ→φ\vdash\varphi\to\varphi より Γ⊢φ→θk\Gamma\vdash\varphi\to\theta_k。

(iii) θk\theta_k が先行する θi,θj=θi→θk\theta_i,\theta_j=\theta_i\to\theta_k からの MP のとき。 帰納法の仮定より Γ⊢φ→θi\Gamma\vdash\varphi\to\theta_i と Γ⊢φ→(θi→θk)\Gamma\vdash\varphi\to(\theta_i\to\theta_k)。(A2) の (φ→(θi→θk))→((φ→θi)→(φ→θk))(\varphi\to(\theta_i\to\theta_k))\to((\varphi\to\theta_i)\to(\varphi\to\theta_k)) に2回 MP して Γ⊢φ→θk\Gamma\vdash\varphi\to\theta_k。

k=nk=n で Γ⊢φ→ψ\Gamma\vdash\varphi\to\psi。∎

証明の3つの公理が、この帰納法の各ケースに過不足なく対応しているのが見どころです （(A1) がケース(i)、⊢φ→φ\vdash\varphi\to\varphi がケース(ii)、(A2) がケース(iii)）。ヒルベルト系の公理は、 まさに演繹定理を回すために選ばれているのです。以後は演繹定理を使ってよいので、 「φ\varphi を仮定して ψ\psi を導けば ⊢φ→ψ\vdash\varphi\to\psi」と、普通の数学の証明のように書けます。

自然演繹：推論を「木」で書く

ヒルベルト系は論じるには良いが書きにくい。逆に、人間の推論に近く書きやすい体系が ゲンツェンの自然演繹です。各結合子に「導入規則（作る）」と「除去規則（使う）」を対にして与えます。

定義 自然演繹の主な規則

仮定から結論へ木を組む。[φ][\varphi] は途中でdischarge（解消）される仮定。主な規則： →\toI（φ\varphi を仮定して ψ\psi を導いたら φ→ψ\varphi\to\psi を結論し仮定を解消）、→\toE（MP）、 ∧\landI／∧\landE、∨\lorI／∨\lorE、⊥\botE（爆発律：⊥\bot から任意の φ\varphi）、 RAA（背理法：¬φ\lnot\varphi を仮定して ⊥\bot を導いたら φ\varphi、古典論理の要）。

規則が結合子ごとに整理されているので、証明が木の形に自然に組めます。例として、∧\land の交換 (φ∧ψ)→(ψ∧φ)(\varphi\land\psi)\to(\psi\land\varphi) を導きます。仮定 φ∧ψ\varphi\land\psi を分解し、順序を入れ替えて組み直し、 最後に →\toI で仮定を解消する——という流れがそのまま木になります。

[φ∧ψ]1[\varphi\land\psi]_1
∧E₂
ψ\psi
[φ∧ψ]1[\varphi\land\psi]_1
∧E₁
φ\varphi
∧I
ψ∧φ\psi\land\varphi
→I, 1
(φ∧ψ)→(ψ∧φ)(\varphi\land\psi)\to(\psi\land\varphi)

葉の [φ∧ψ]1[\varphi\land\psi]_1 が仮定、最下段の →\toI,1 でその仮定が解消されて、仮定に依存しない 定理 (φ∧ψ)→(ψ∧φ)(\varphi\land\psi)\to(\psi\land\varphi) が得られています。もう一つ、二重否定の一方向 φ→¬¬φ\varphi\to\lnot\lnot\varphi を、¬α\lnot\alpha を α→⊥\alpha\to\bot とみて導きます。

[¬φ]1[\lnot\varphi]_1
[φ]2[\varphi]_2
→E
⊥\bot
→I, 1
¬¬φ\lnot\lnot\varphi
→I, 2
φ→¬¬φ\varphi\to\lnot\lnot\varphi

内側で ¬φ\lnot\varphi（=φ→⊥=\varphi\to\bot）と φ\varphi から ⊥\bot を出し、→\toI,1 で ¬φ\lnot\varphi を解消して ¬¬φ\lnot\lnot\varphi（=¬φ→⊥=\lnot\varphi\to\bot）、さらに →\toI,2 で φ\varphi を解消。仮定を立て、使い、解消する という自然演繹の呼吸が見えます。ヒルベルト系と自然演繹は「導けるもの」が完全に一致します（互いに翻訳可能）。

注意 古典と直観主義の分かれ目はここ

RAA（背理法）と二重否定除去 ¬¬φ→φ\lnot\lnot\varphi\to\varphi、排中律 φ∨¬φ\varphi\lor\lnot\varphi は互いに導出可能で、 これらを認めるか否かが古典論理と直観主義論理を分ける（第10章）。上の φ→¬¬φ\varphi\to\lnot\lnot\varphi は 直観主義でも成り立つが、逆向き ¬¬φ→φ\lnot\lnot\varphi\to\varphi は古典論理でしか成り立たない。

つまずきポイント

注意 よくある誤解

  • ⊢\vdash と ⊨\models は定義が全然違う。 ⊢\vdash は「規則で導ける」（構文・有限の手続き）、⊨\models は「全付値で真」（意味・付値の全域）。両者が一致するというのが健全性・完全性（次章）であって、定義上は無関係。
  • 公理図式は「無限個の公理」。 (A1) は φ,ψ\varphi,\psi にどんな論理式を代入してもよく、実体は無限個の公理の族。
  • discharge を忘れると仮定が残る。 →\toI で解消しない限り仮定は結論に依存し続ける。木の葉の番号と規則の番号の対応を必ず確認する。

この章のまとめ

  • ⊢\vdash は構文的な導出可能性：公理（図式）から推論規則で機械的に導ける、有限の記号列。証明そのものが数学的対象になる。
  • ヒルベルト系は公理3図式＋MP。論じるのに向くが書きにくい。演繹定理（証明の構造に関する帰納法で証明）が「仮定して導く」書き方を可能にする。
  • 自然演繹は結合子ごとの導入・除去規則で証明を木として組む。ヒルベルト系と等価。古典と直観主義の差は RAA・二重否定除去・排中律にある。

次章はいよいよ両世界を橋渡し——命題論理の健全性と完全性（⊢\vdash と ⊨\models の一致）を証明します。