⟐ 数学の作り方 How to make Mathematics

第16章 型理論・構成的数学

証明は、プログラムである

これまで論理（証明）と計算（プログラム）を別々に見てきました。第10章の直観主義論理では、 「証明とは構成である」（BHK解釈）という見方が出ました。この見方を突き詰めると、驚くべき等式に至ります—— 証明とプログラムは、同じものの二つの呼び名だった。命題は型、証明はその型をもつプログラム、 証明の簡約はプログラムの実行。これがカリー–ハワード対応です。

この対応は、集合論とは別の数学の土台（型理論）を可能にし、コンピュータによる証明の機械検証 （Coq, Lean, Agda）を現実にしました。さらにホモトピー型理論は、型を「空間」とみなして幾何と論理を融合します。 章の後半では視点を変え、「各定理を証明するのにどれだけの公理的強さが必要か」を測る逆数学を扱い、 第13章のゲンツェン以来の「証明強度」という主題を締めくくります。

カリー–ハワード対応：命題＝型、証明＝プログラム、証明の正規化＝プログラムの実行。論理と計算は一つ。

単純型付きλ計算から System F へ

第11章のλ計算に型を付けます。型は「関数の入出力の種類」を制約し、計算の暴走を防ぎます。

定義 単純型付きλ計算（STLC）

型を A::=o∣A→AA::= o\mid A\to A（基底型と関数型）で定める。項に型付け規則を課す：変数は文脈の型、 λx:A. M:A→B\lambda x{:}A.\,M:A\to B（x:Ax{:}A のもとで M:BM:B）、適用 (M N):B(M\,N):B（M:A→B, N:AM:A\to B,\ N:A）。

定理 正規化定理

STLC の型付き項は強正規化する：どんな順序でβ簡約しても有限回で正規形（それ以上簡約できない形）に至る。

型が付くだけで「計算が必ず止まる」——第11章の型なしλ計算では停止しない項（YY コンビネータ等）があったのに、 型が無限ループを排除します。ただし停止を保証する代償に、STLC は全計算可能関数を表せません（チューリング完全でない）。 表現力を上げる方向が2つあります。System F（Λα. M\Lambda\alpha.\,M で型そのものに抽象＝多相性。「任意の型 α\alpha について」を プログラムに入れる。第10章の二階論理に対応）と、依存型です。

定義 依存型（Martin-Löf型理論）

型が項に依存してよい：Πx:AB(x)\Pi_{x:A}B(x)（xx に応じて返り型が変わる関数型、∀\forall に対応）、 Σx:AB(x)\Sigma_{x:A}B(x)（対の型、∃\exists に対応）、等号型 IdA(a,b)\mathrm{Id}_A(a,b)（a=ba=b の証明の型）などをもつ。 これがMartin-Löf型理論で、構成的数学の基礎理論となる。

依存型により「nn 次元ベクトル」のように値に依存する型が書け、仕様（命題）と実装（プログラム）を一つの言語で扱えます。

カリー–ハワード対応

論理と型理論の規則を並べると、完全に一致します。これが偶然でないことを述べるのが対応です。

定理 カリー–ハワード対応

命題と型、証明と項が対応する： φ→ψ↔A→B,φ∧ψ↔A×B,φ∨ψ↔A+B,\varphi\to\psi \leftrightarrow A\to B,\quad \varphi\land\psi\leftrightarrow A\times B,\quad \varphi\lor\psi\leftrightarrow A+B, ∀x φ↔Πx:AB(x),∃x φ↔Σx:AB(x).\forall x\,\varphi\leftrightarrow\Pi_{x:A}B(x),\quad \exists x\,\varphi\leftrightarrow\Sigma_{x:A}B(x). 「φ\varphi が証明可能」  ⟺  \iff「型 AA をもつ項（プログラム）が存在」。しかも証明の正規化＝プログラムの簡約が対応する。

例：φ→φ\varphi\to\varphi の証明は恒等関数 λx.x:A→A\lambda x.x:A\to A。→\to導入（第2章）が関数抽象 λ\lambda、 →\to除去（MP）が関数適用にぴたり対応します。この視点だと証明を書く＝正しいプログラムを書くであり、 逆に型検査＝証明の検証。だからコンピュータが証明を機械的にチェックできる（証明支援系）。直観主義論理が舞台なのは、 BHK解釈（証明＝構成）そのものだからで、排中律は「任意の型の項を作る一般手続き」に対応せず、標準の型理論には入りません。

ホモトピー型理論

21世紀の展開。等号型 IdA(a,b)\mathrm{Id}_A(a,b) を「aa から bb への道」とみなすと、型が空間、等式の証明がホモトピーになります （位相幾何学との融合）。

定義 univalence 公理

ホモトピー型理論（HoTT）では型を空間、IdA(a,b)\mathrm{Id}_A(a,b) を道の空間とみなす。ヴォエヴォツキの univalence 公理は「型の同値（同型）と型の等しさを同一視する」——(A≃B)≃(A=B)(A\simeq B)\simeq(A=B)。 数学者が暗黙にやっている「同型なものは同じとみなす」を、公理として正式化する。

univalence により「同型を除いて考える」が言語のレベルで正当化され、証明の機械検証と現代数学の実践が噛み合います。 型理論は、集合論（∈\in ベース）とは異なる、構成的で計算的な数学の土台を与えるのです。

構成的数学と逆数学

視点を「証明に何が必要か」へ移します。まず、排中律・選択を制限した構成的数学では、証明が常に構成（アルゴリズム）を伴います （第10章の存在特性）。「存在する」を「作れる」に限るこの立場は、計算と相性がよい。 そのうえで「各定理はどれだけの公理的強さを要するか」を精密に測るのが逆数学です。

定義 逆数学と二階算術の部分体系

二階算術（自然数と、その集合に量化する体系）の部分体系を強さの順に並べる——ビッグファイブ： RCA0 ⊊ WKL0 ⊊ ACA0 ⊊ ATR0 ⊊ Π11-CA0.\mathrm{RCA}_0\ \subsetneq\ \mathrm{WKL}_0\ \subsetneq\ \mathrm{ACA}_0\ \subsetneq\ \mathrm{ATR}_0\ \subsetneq\ \Pi^1_1\text{-}\mathrm{CA}_0. RCA0\mathrm{RCA}_0（再帰的内包＝計算可能な集合だけ）を基準とし、定理 TT を証明するのにどの体系が必要十分かを調べる。

逆数学の名の由来は、通常「公理 ⇒\Rightarrow 定理」を示すのに対し、RCA0\mathrm{RCA}_0 上で「定理 ⇒\Rightarrow 公理」まで示して、 定理と公理体系が同値だと突き止める点にあります。すると多くの定理が、ビッグファイブのどれかにきれいに分類されます。

例 定理の証明強度による分類

  • WKL0\mathrm{WKL}_0（弱ケーニヒの補題）と同値：ハイネ–ボレルの定理（コンパクト性）、連続関数の最大値定理、 ゲーデルの完全性定理（第7章）。
  • ACA0\mathrm{ACA}_0（算術的内包）と同値：ボルツァーノ–ワイエルシュトラス、単調有界列の収束、可算体の極大イデアルの存在。
  • ATR0\mathrm{ATR}_0：可算整列順序の比較可能性。Π11-CA0\Pi^1_1\text{-}\mathrm{CA}_0：カントール–ベンディクソンの定理。

「解析学の定理が、実は弱ケーニヒの補題と同じ強さだった」——ばらばらに見える定理が、必要な公理の強さで 整然と並ぶ。これは第13章の証明論的順序数（PA\mathrm{PA} の ε0\varepsilon_0）と同じ「強さを測る」精神の、体系レベルの実現です。

定理 保存定理

WKL0\mathrm{WKL}_0 は RCA0\mathrm{RCA}_0 に対し Π20\Pi^0_2 文について保存的：WKL0\mathrm{WKL}_0 で証明できる Π20\Pi^0_2 文は RCA0\mathrm{RCA}_0 でも証明できる。ゆえに WKL0\mathrm{WKL}_0 は非構成的な弱ケーニヒの補題を使っても、計算可能な結論 （アルゴリズムの存在）については RCA0\mathrm{RCA}_0 以上を主張しない。

保存定理は「非構成的な道具を使っても、構成的な結論は損なわれない」という安全保証で、ヒルベルト計画の精神 （理想的手法で有限的結論を効率よく得る）を部分的に実現します。第13章で潰えたヒルベルトの夢が、 形を変えてここに生きています。

つまずきポイント

注意 よくある誤解

  • カリー–ハワードは古典論理では素直に成り立たない。 対応が自然なのは直観主義。排中律は「制御演算子（call/cc）」に対応し、拡張が必要。
  • 型理論は集合論の言い換えではない。 ∈\in でなく型付けを土台にする、独立な基礎。計算・機械検証と相性がよいのが利点。
  • 逆数学は「証明の難しさ」ではなく「必要な公理の強さ」を測る。 計算量とも証明論的順序数とも異なる、体系レベルの物差し。
  • 構成的に証明できない ≠ 偽。 構成的数学は排中律を使わないだけ。古典的に真でも構成的証明が無い定理はある（例：中間値定理の一部の形）。

この章のまとめ

  • カリー–ハワード対応：命題＝型、証明＝プログラム、正規化＝実行。STLC（停止するが弱い）→ System F（多相）→ 依存型（Martin-Löf、∀∃\forall\exists を ΠΣ\Pi\Sigma で）と表現力を上げ、証明支援系を可能にする。
  • ホモトピー型理論は型を空間・等号を道とみなし、univalence 公理で「同型＝等しい」を正式化。集合論と別の構成的な数学の土台。
  • 構成的数学は存在を構成に限る。逆数学は定理を二階算術のビッグファイブ（RCA0⊊WKL0⊊ACA0⊊ATR0⊊Π11-CA0\mathrm{RCA}_0\subsetneq\mathrm{WKL}_0\subsetneq\mathrm{ACA}_0\subsetneq\mathrm{ATR}_0\subsetneq\Pi^1_1\text{-}\mathrm{CA}_0）で分類し、保存定理で非構成的手法の安全性を保証する。

これで数理論理学・数学基礎論は一区切りです。命題・述語論理から完全性・不完全性、計算可能性、集合論の独立性、 型理論・逆数学まで——「数学が自分自身を調べる」営みの全景を、証明とともに辿りました。ここで培った形式化・ 自己言及・証明強度の視点は、あらゆる分野の“基礎”を問い直すときの土台になります。おつかれさまでした。