# 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く > マーティン＝レーフ型理論の Π 型・Σ 型・恒等型・宇宙・帰納型を規則として述べ、型理論版の選択公理、等号の対称性と輸送、0≠1 を規則から証明する。CIC の Prop と Type の区別、関数外延性と UIP の独立性まで、Lean 4 のコードと対応させて解説する。 > https://rikai.mugen-giken.com/mathematics/logic-and-type-theory/dependent-type-theory ## 0. この記事の要点 「すべての自然数 $n$ について $n+0=n$ が成り立つ」という主張を、計算機に検査させられる形で書くには、どうすればよいでしょうか。この記事では、命題も証明も数も、すべてを「型」と「その型の値」として書く体系を学びます。読み終えると、「すべての」「存在する」「等しい」といった論理の言葉が、型の作り方の規則として書けることが分かり、Lean というソフトで書かれた証明を読むための土台ができます。 - **依存型**とは、値に依存して決まる型のことです。「各 $n$ に $P(n)$ の証明を返す関数」の型 $\Pi_{(n:\mathbb{N})}P(n)$ は $\forall n\,P(n)$ を、「$a$ と $P(a)$ の証明の組」の型 $\Sigma_{(x:A)}P(x)$ は $\exists x\,P(x)$ を表します。前章の[カリー＝ハワード対応](/mathematics/logic-and-type-theory/simple-types-curry-howard)（命題を型、証明をその型の値と読む対応）が述語論理（「すべての」「存在する」を含む論理）まで広がります。 - **マーティン＝レーフ型理論** (MLTT) は、Π 型・Σ 型・恒等型 $\mathrm{Id}_A(a,b)$・宇宙 $\mathcal{U}$・帰納型（自然数など）を、それぞれ形成・導入・除去・計算の 4 種類の規則で与える体系です。 - 規則だけから、**型理論版の選択公理**（）、等号の対称性・推移性・輸送（）、自然数の帰納法による $0+n=n$（）、そして宇宙を使った $0\ne1$（）を証明します。 - Lean の論理は **構成の計算 (CIC)** の一種で、命題の宇宙 `Prop` と型の宇宙 `Type` を区別します。`Prop` の証明は区別されない（証明の無関係性）代わりに、`∃` から証人を取り出すことはできず、そこに `Classical.choice` が要ります（）。 - 関数外延性と「等号の証明の一意性」(UIP) は MLTT から証明も反証もできません（主張として述べます）。Lean はこの二つを、公理と `Prop` の性質で成り立たせています。 ## 1. 動機：「すべての $n$ について」を型で書く ### 1.1. 単純型の限界 前章の [単純型付きラムダ計算とカリー＝ハワード対応](/mathematics/logic-and-type-theory/simple-types-curry-howard) では、命題 $A\to B$ を関数の型と読みました。$A\to B$ の証明は、$A$ の証明を受け取って $B$ の証明を返す関数です。 では「すべての自然数 $n$ について $n+0=n$」はどうでしょう。BHK 解釈（）に従えば、その証明は「各 $n$ に $n+0=n$ の証明を対応させる方法」、つまり関数です。けれどもこの関数は、入力 $n=3$ には $3+0=3$ の証明を、入力 $n=5$ には $5+0=5$ の証明を返します。**出力の型が入力の値によって変わる**のです。単純型の $A\to B$ では、$B$ は $x$ によらない一つの型なので、こういう関数の型を書けません。 これを書けるようにしたのが**依存型**です。$\Pi_{(n:\mathbb{N})}\,(n+0=n)$ は「$n:\mathbb{N}$ を受け取り、型 $n+0=n$ の値を返す関数」の型です。Lean では `∀ n : Nat, n + 0 = n` と書き、実はこれは `(n : Nat) → n + 0 = n` と同じものです。 ### 1.2. 依存型はプログラミングでも便利 依存型は論理のためだけの道具ではありません。「長さ $n$ のベクトル」の型 $\mathrm{Vec}(A,n)$ は自然数 $n$ に依存する型で、これを使うと「長さの合わないベクトルの内積」はコンパイル時点で型エラーになります。 ```lean def Vec (α : Type) : Nat → Type | 0 => Unit | n + 1 => α × Vec α n example : Vec Nat 2 := (1, 2, ()) ``` `Vec Nat 2` は `Nat × (Nat × Unit)` に計算され、`(1, 2, ())` はその値です。型 `Vec α n` は値 `n` で決まり、型の計算に値の計算が入り込んでいます。 ### 1.3. 集合論との違い [公理的集合論 ZFC](/mathematics/logic-and-type-theory/axiomatic-set-theory) では、一階述語論理という「論理」の上に、$\in$ についての公理を置いて「数学の対象」を作りました。論理と対象は別の層です。依存型理論では、**命題も対象も型であり、証明も元も項**です。論理を別に用意せず、型の規則だけで論理と数学の両方を書きます。等号さえも「$a$ と $b$ が等しいことの証明の型」$\mathrm{Id}_A(a,b)$ という型になります。 この一体性が、計算機による証明検査と相性がよいのです。証明の検査は「この項がこの型をもつか」という型検査になり、型検査は（適切に設計すれば）アルゴリズムで決定できます。Lean はこの設計の上に立っています（[証明支援系 Lean の仕組み](/mathematics/logic-and-type-theory/lean-kernel)）。 ## 2. 判断と規則の形 型理論の基本単位は**判断**です。 文脈 $\Gamma=x_1{:}A_1,\ldots,x_n{:}A_n$（各 $A_i$ は前の変数に依存してよい）のもとで、次の 4 種類の判断を考える。 - $\Gamma\vdash A\ \mathsf{type}$：$A$ は型である。 - $\Gamma\vdash a:A$：$a$ は型 $A$ の項である。 - $\Gamma\vdash A\equiv B$：型 $A$ と $B$ は**定義的に等しい**。 - $\Gamma\vdash a\equiv b:A$：項 $a$ と $b$ は型 $A$ の項として定義的に等しい。 定義的等しさは、定義の展開と計算（[β 簡約](/mathematics/logic-and-type-theory/lambda-calculus#def-beta)など）で互いに移り合うことを表す。$\Gamma\vdash a:A$ かつ $\Gamma\vdash A\equiv B$ なら $\Gamma\vdash a:B$ とする（**変換規則**）。 なぜ二種類の「等しい」を使い分けるのかを先に述べると、機械が自動で確かめられる等しさ（計算で一致する）と、人が証明して初めて言える等しさを、規則の上で区別するためです。 定義的等しさ $\equiv$ は**判断**であり、型 $\mathrm{Id}_A(a,b)$（§5）は**命題**です。前者は計算すれば確かめられる等しさ、後者は証明を要する等しさです。たとえば $n+0\equiv n$ は加法の定義から計算で従いますが、$0+n=n$ は帰納法で証明しなければなりません（）。この区別は Lean で `rfl` が通るかどうかの区別として、日常的に現れます。 各型は次の 4 種類の規則で導入されます。**形成**（型を作る）、**導入**（その型の項を作る）、**除去**（その型の項を使う）、**計算**（導入した直後に除去したときの値）。前章の導入・除去と β 簡約の組をそのまま一般化したものです。 ## 3. Π 型 $$ \frac{\Gamma\vdash A\ \mathsf{type}\quad \Gamma,x{:}A\vdash B(x)\ \mathsf{type}}{\Gamma\vdash\Pi_{(x:A)}B(x)\ \mathsf{type}}\ (\text{形成})\qquad \frac{\Gamma,x{:}A\vdash b(x):B(x)}{\Gamma\vdash\lambda x.b(x):\Pi_{(x:A)}B(x)}\ (\text{導入}) $$ $$ \frac{\Gamma\vdash f:\Pi_{(x:A)}B(x)\quad\Gamma\vdash a:A}{\Gamma\vdash f\,a:B(a)}\ (\text{除去})\qquad (\lambda x.b(x))\,a\equiv b(a)\ (\text{計算}),\qquad f\equiv\lambda x.f\,x\ (\eta) $$ $B$ が $x$ に依存しないとき $\Pi_{(x:A)}B$ を $A\to B$ と書く。 除去規則で、結果の型が $B(a)$、つまり**引数の値を代入した型**になっていることが単純型との違いです。命題として読むと、$\Pi_{(x:A)}P(x)$ は $\forall x{:}A,\ P(x)$ で、除去規則は「全称命題を個別の $a$ に適用する」推論です。
通常の関数 ℕ → ℕ 入力 3 入力 5 出力の型は ℕ どの入力でも 同じ型 依存関数 Π (n : ℕ), n+0=n 入力 3 入力 5 型 3+0=3 の値 型 5+0=5 の値
## 4. Σ 型と型理論版の選択公理 形成：$\Gamma\vdash A\ \mathsf{type}$ と $\Gamma,x{:}A\vdash B(x)\ \mathsf{type}$ から $\Gamma\vdash\Sigma_{(x:A)}B(x)\ \mathsf{type}$。 導入：$\Gamma\vdash a:A$ と $\Gamma\vdash b:B(a)$ から $\Gamma\vdash(a,b):\Sigma_{(x:A)}B(x)$。 除去：$\Gamma,z{:}\Sigma_{(x:A)}B(x)\vdash C(z)\ \mathsf{type}$、$\Gamma,x{:}A,y{:}B(x)\vdash c(x,y):C((x,y))$、$\Gamma\vdash p:\Sigma_{(x:A)}B(x)$ から $\Gamma\vdash\mathrm{split}(c,p):C(p)$。 計算：$\mathrm{split}(c,(a,b))\equiv c(a,b)$。 除去規則で、目標の型 $C(z)$ が対 $z$ そのものに依存してよいことが重要です。これにより射影 $\mathrm{pr}_1(p):\equiv\mathrm{split}((x,y)\mapsto x,\,p):A$ だけでなく、$\mathrm{pr}_2(p):\equiv\mathrm{split}((x,y)\mapsto y,\,p):B(\mathrm{pr}_1(p))$ も定義できます（$C(z):\equiv B(\mathrm{pr}_1(z))$ ととると、$C((x,y))\equiv B(x)$ なので $y$ が型に合う）。 命題として読むと、$\Sigma_{(x:A)}P(x)$ の証明は「証人 $a$ と $P(a)$ の証明の組」で、BHK 解釈の $\exists x\,P(x)$ そのものです。$B$ が $x$ に依存しなければ $\Sigma_{(x:A)}B$ は直積 $A\times B$、命題としては $A\wedge B$ です。 次の定理のねらいは、「各 $x$ に対して条件を満たす $y$ がある」という証明から、「$x$ を $y$ に送る一つの関数」を取り出せることを、規則だけで示すことです。証明の方針は、Σ の証明が持っている証人を射影で取り出して関数にすることです。 型 $A,B$ と型族 $R(x,y)$（$x:A$, $y:B$）について、次の型の閉項が存在する。 $$ \Bigl(\Pi_{(x:A)}\Sigma_{(y:B)}R(x,y)\Bigr)\to\Sigma_{(f:A\to B)}\Pi_{(x:A)}R(x,f(x)). $$ $h:\Pi_{(x:A)}\Sigma_{(y:B)}R(x,y)$ を仮定する。$f:\equiv\lambda x.\,\mathrm{pr}_1(h\,x):A\to B$ とおく。$x:A$ について $\mathrm{pr}_2(h\,x):R(x,\mathrm{pr}_1(h\,x))$ であり、Π の計算規則により $f(x)\equiv\mathrm{pr}_1(h\,x)$ なので、変換規則によって $\mathrm{pr}_2(h\,x):R(x,f(x))$。よって $g:\equiv\lambda x.\,\mathrm{pr}_2(h\,x):\Pi_{(x:A)}R(x,f(x))$ で、$(f,g)$ が求める型の項である。全体は $\lambda h.(f,g)$。 集合論の選択公理（）は ZF から証明できない独立な公理でした（）。ところが型理論では、同じ形の命題が数行で**定理**になります。からくりは、$\Sigma$ の証明が証人 $\mathrm{pr}_1(h\,x)$ を**中に持っている**ことです。「各 $x$ に $y$ が存在する」ことの証明がすでに $y$ の選び方を含んでいるので、選ぶ作業は要りません。Lean でもそのまま書けます。 ```lean def ac {A B : Type} {R : A → B → Type} (h : (x : A) → (y : B) × R x y) : (f : A → B) × ((x : A) → R x (f x)) := ⟨fun x => (h x).1, fun x => (h x).2⟩ ``` `(y : B) × R x y` が $\Sigma_{(y:B)}R(x,y)$、`.1` と `.2` が射影です。ところが、同じことを Lean の `∃`（`Prop` の存在量化）で書くとこの証明は通りません。その理由は §8 で説明します。 ## 5. 恒等型 「$a$ と $b$ が等しい」も命題なので、型として表します。マーティン＝レーフの恒等型は、等号の導入規則を反射律だけにし、除去規則を「反射律の場合に示せば十分」という形にしたものです。 形成：$\Gamma\vdash a:A$ と $\Gamma\vdash b:A$ から $\Gamma\vdash\mathrm{Id}_A(a,b)\ \mathsf{type}$。$a=_Ab$ とも書く。 導入：$\Gamma\vdash a:A$ から $\Gamma\vdash\mathsf{refl}_a:\mathrm{Id}_A(a,a)$。 除去（**J 規則**）：型族 $\Gamma,x{:}A,y{:}A,p{:}\mathrm{Id}_A(x,y)\vdash C(x,y,p)\ \mathsf{type}$ と、$\Gamma,z{:}A\vdash d(z):C(z,z,\mathsf{refl}_z)$ が与えられたとき、$\Gamma\vdash a,b:A$ と $\Gamma\vdash q:\mathrm{Id}_A(a,b)$ に対して $\Gamma\vdash J(d,a,b,q):C(a,b,q)$。 計算：$J(d,a,a,\mathsf{refl}_a)\equiv d(a)$。 J 規則は「等号についての帰納法」です。$\mathrm{Id}_A$ を $\mathsf{refl}$ だけで生成された型族と見て、性質 $C$ を $\mathsf{refl}$ の場合に確かめれば、すべての等号の証明について成り立つ、と主張しています。 次の命題のねらいは、J 規則だけから、等号について普段使う性質（対称性・推移性など）が導けることを確かめることです。J 規則の使い方は、示したい性質を表す型族 $C$ と、$x=y$ が $\mathsf{refl}$ の場合（両辺が同じ $z$ の場合）の証明 $d$ を指定する、という二つの選択に尽きます。推移性の (2) で $C$ に「$\Pi_{(w:A)}$」が付くのは、$b$ と $c$ の等号の証明を後から受け取れるように、その部分を先に量化しておくためです。 任意の $a,b,c:A$ について、次の型の項が J 規則から構成できる。 1. （対称性）$\mathrm{Id}_A(a,b)\to\mathrm{Id}_A(b,a)$。 2. （推移性）$\mathrm{Id}_A(a,b)\to\mathrm{Id}_A(b,c)\to\mathrm{Id}_A(a,c)$。 3. （輸送）型族 $P(x)$（$x:A$）について $\mathrm{Id}_A(a,b)\to P(a)\to P(b)$。 4. （合同）関数 $f:A\to B$ について $\mathrm{Id}_A(a,b)\to\mathrm{Id}_B(f\,a,f\,b)$。 いずれも J 規則の $C$ と $d$ を指定すればよい。 1. $C(x,y,p):\equiv\mathrm{Id}_A(y,x)$、$d(z):\equiv\mathsf{refl}_z:\mathrm{Id}_A(z,z)\equiv C(z,z,\mathsf{refl}_z)$。$q:\mathrm{Id}_A(a,b)$ について $J(d,a,b,q):\mathrm{Id}_A(b,a)$。 2. $C(x,y,p):\equiv\Pi_{(w:A)}\,\mathrm{Id}_A(y,w)\to\mathrm{Id}_A(x,w)$、$d(z):\equiv\lambda w.\lambda r.\,r$。$C(z,z,\mathsf{refl}_z)\equiv\Pi_{(w:A)}\mathrm{Id}_A(z,w)\to\mathrm{Id}_A(z,w)$ なので型が合う。$J(d,a,b,q)$ を $c$ と $\mathrm{Id}_A(b,c)$ の証明に適用する。 3. $C(x,y,p):\equiv P(x)\to P(y)$、$d(z):\equiv\lambda u.u$。 4. $C(x,y,p):\equiv\mathrm{Id}_B(f\,x,f\,y)$、$d(z):\equiv\mathsf{refl}_{f\,z}$。 輸送 (3) は、ライプニッツの「等しいものは同じ性質をもつ」の型理論版です。Lean では J 規則は `Eq.rec` で、tactic `cases p` は等号の証明 `p : a = b` に J 規則を適用して $b$ を $a$ に置き換えます。 ```lean theorem my_symm {A : Type} {a b : A} (p : a = b) : b = a := by cases p rfl def transport {A : Type} (P : A → Type) {a b : A} (p : a = b) (x : P a) : P b := p ▸ x ``` `cases p` の後の目標は `a = a` になり、`rfl`（$\mathsf{refl}$）で閉じます。`p ▸ x` は輸送の記法です。 MLTT（Π・Σ・Id・ℕ・宇宙をもつ内包的型理論）では、次の二つはどちらも証明も反証もできない。 1. （UIP：等号の証明の一意性）$\Pi_{(a,b:A)}\Pi_{(p,q:\mathrm{Id}_A(a,b))}\mathrm{Id}(p,q)$。 2. （関数外延性）$f,g:\Pi_{(x:A)}B(x)$ について $\bigl(\Pi_{(x:A)}\mathrm{Id}(f\,x,g\,x)\bigr)\to\mathrm{Id}(f,g)$。 主張だけを述べます。UIP については、ホフマンとシュトライヒャー (1998) が型を亜群（すべての射が可逆な圏）で、恒等型を射の集合で解釈するモデルを作り、そこでは同じ 2 点の間に異なる射があるので UIP が偽になることを示しました。UIP が成り立つモデル（集合によるモデル）もあるので、UIP は独立です。関数外延性も、成り立つモデルと成り立たないモデルの両方があります。 J 規則から UIP が出ないことは、一見すると欠陥に見えますが、ここから**ホモトピー型理論**が生まれました。$\mathrm{Id}_A(a,b)$ を「$a$ から $b$ への道」と読むと、J 規則は道に沿った輸送、UIP の失敗は「同じ 2 点を結ぶ道が本質的に異なりうる」ことにあたります。一方、Lean は `Prop` の証明の無関係性（§8）によって UIP を、商型の公理 `Quot.sound` によって関数外延性を、それぞれ定理として成り立たせています（[証明支援系 Lean の仕組み](/mathematics/logic-and-type-theory/lean-kernel)）。 ## 6. 帰納型：自然数 形成：$\vdash\mathbb{N}\ \mathsf{type}$。導入：$\vdash0:\mathbb{N}$、$n:\mathbb{N}\vdash\mathrm{succ}(n):\mathbb{N}$。 除去：型族 $\Gamma,n{:}\mathbb{N}\vdash C(n)\ \mathsf{type}$、$\Gamma\vdash c_0:C(0)$、$\Gamma\vdash c_s:\Pi_{(n:\mathbb{N})}C(n)\to C(\mathrm{succ}(n))$ から、$\Gamma,n{:}\mathbb{N}\vdash\mathrm{ind}(c_0,c_s,n):C(n)$。 計算：$\mathrm{ind}(c_0,c_s,0)\equiv c_0$、$\mathrm{ind}(c_0,c_s,\mathrm{succ}(n))\equiv c_s\,n\,\mathrm{ind}(c_0,c_s,n)$。 除去規則は、$C$ を命題と読めば**数学的帰納法**（）、$C$ を定数の型 $\mathbb{N}$ と読めば**原始再帰による関数の定義**です。集合論では再帰的定義の原理（）を定理として証明しましたが、型理論ではそれが規則そのものです。ここでは $\mathbb{N}=\{0,1,2,\ldots\}$ です。 加法を $m+n:\equiv\mathrm{ind}(m,\ \lambda k.\lambda r.\mathrm{succ}(r),\ n)$（$C(n):\equiv\mathbb{N}$）で定めます。計算規則から $m+0\equiv m$、$m+\mathrm{succ}(n)\equiv\mathrm{succ}(m+n)$。したがって $n+0=n$ は $\mathsf{refl}_n$ で証明できます（定義的に等しい）。 $0+n=n$ は定義的には成り立たず、帰納法が要ります。$C(n):\equiv\mathrm{Id}_{\mathbb{N}}(0+n,n)$ とおくと、$c_0:\equiv\mathsf{refl}_0:C(0)$（$0+0\equiv0$）。帰納段階では $p:\mathrm{Id}(0+n,n)$ から $\mathrm{Id}(0+\mathrm{succ}(n),\mathrm{succ}(n))\equiv\mathrm{Id}(\mathrm{succ}(0+n),\mathrm{succ}(n))$ の証明を作ればよく、 (4) で $\mathrm{succ}$ を両辺に施せば得られます。Lean で自分の自然数型を定義すると、除去規則がそのまま自動生成されます。 ```lean inductive MyNat where | zero : MyNat | succ : MyNat → MyNat #check @MyNat.rec -- @MyNat.rec : {motive : MyNat → Sort u_1} → -- motive MyNat.zero → ((a : MyNat) → motive a → motive a.succ) → (t : MyNat) → motive t def MyNat.add (m : MyNat) : MyNat → MyNat | .zero => m | .succ n => .succ (m.add n) theorem MyNat.zero_add (n : MyNat) : MyNat.zero.add n = n := by induction n with | zero => rfl | succ k ih => simp [MyNat.add, ih] ``` `MyNat.rec` の型が上の除去規則そのもので、`motive` が $C$ です。`induction n with` はこの `MyNat.rec` を適用する tactic で、`zero` と `succ k ih` の二つの場合（$c_0$ と $c_s$。`ih` が帰納法の仮定 $C(k)$）を書かせます。`simp [MyNat.add, ih]` は、加法の定義と帰納法の仮定で目標を書き換えて閉じます。 同じ形の規則で、リスト、二分木、さらに一般の帰納型（W 型）も定義できます。Lean の `inductive` 宣言は、構成子の型を与えると形成・導入・除去・計算の 4 つの規則を自動で生成する仕組みです。 ## 7. 宇宙 型を値として扱い、型を返す関数（型族）を項として書くために、**型の型**を用意します。 宇宙の列 $\mathcal{U}_0,\mathcal{U}_1,\ldots$ を置き、$\mathcal{U}_i:\mathcal{U}_{i+1}$ とする。各 $\mathcal{U}_i$ は $\mathbb{N}$、空の型 $\mathbb{0}$、1 元型 $\mathbb{1}$（元 $\star$）を含み、Π・Σ・Id で閉じている。$A:\mathcal{U}_i$ ならば $A$ は型であり、$A:\mathcal{U}_{i+1}$ でもある（**累積性**）。 $\mathcal{U}:\mathcal{U}$（すべての型の型が自分自身を含む）とすると、ジラールのパラドックスにより矛盾が導かれることが知られています。集合論で「すべての集合の集合」が存在しない（）のと同じ事情で、宇宙を階層にするのはそのためです。Lean でも `Type : Type 1`、`Type 1 : Type 2`、… と階層になっています。
Prop = Sort 0 2 + 2 = 4、∀ n, n + 0 = n Type 0 = Sort 1 Nat、Nat → Nat、Prop Vec Nat 2、(x : A) × B x Type 1 = Sort 2 Type 0、Nat → Type 0 （型族の型） : : ⋮ Type 2, Type 3, …
宇宙は便利さのためだけにあるのではありません。宇宙がないと証明できない基本的な命題があります。 次の定理のねらいは、「$0$ は $\mathrm{succ}(n)$ と等しくない」という当たり前に見える事実を、規則から証明することです。方針は、$0$ のときは「いつでも証明できる型」$\mathbb{1}$、$\mathrm{succ}(n)$ のときは「証明が存在しない型」$\mathbb{0}$ を返す型の関数 $P$ を作り、等しいなら $P(0)$ の値が $P(\mathrm{succ}(n))$ の値に運ばれてしまう、という矛盾を作ることです。型を返す関数を作るために宇宙が必要になります。 宇宙 $\mathcal{U}$ をもつ MLTT では、$\Pi_{(n:\mathbb{N})}\bigl(\mathrm{Id}_{\mathbb{N}}(0,\mathrm{succ}(n))\to\mathbb{0}\bigr)$ の閉項が存在する。すなわち $0\ne\mathrm{succ}(n)$ が証明できる。 自然数の除去規則を $C(n):\equiv\mathcal{U}$（定数の型族）に使って、型族 $P:\mathbb{N}\to\mathcal{U}$ を $$ P(n):\equiv\mathrm{ind}(\mathbb{1},\ \lambda k.\lambda X.\,\mathbb{0},\ n) $$ で定める。計算規則から $P(0)\equiv\mathbb{1}$、$P(\mathrm{succ}(n))\equiv\mathbb{0}$。$p:\mathrm{Id}_{\mathbb{N}}(0,\mathrm{succ}(n))$ が与えられたとき、輸送（ (3)）で $\star:P(0)$ を運ぶと $P(\mathrm{succ}(n))\equiv\mathbb{0}$ の項が得られる。よって $\lambda n.\lambda p.\,\mathrm{transport}^P(p,\star)$ が求める項である。 証明の要は、**型を値とする関数** $P$ を帰納法で定義したところです（**大きな除去**）。スミス (1988) は、宇宙をもたない MLTT では $0\ne1$ が証明できないことを示しました（主張のみ）。宇宙がないと、「$0$ と $\mathrm{succ}(n)$ を区別する述語」を作る手段がないのです。Lean では同じ証明を次のように書けます。 ```lean def IsZero : Nat → Prop | 0 => True | _ + 1 => False theorem zero_ne_succ (n : Nat) : 0 ≠ n + 1 := by intro h have t : IsZero 0 := trivial rw [h] at t exact t ``` `IsZero` が $P$ で、`rw [h] at t` が輸送です。`t : IsZero (n + 1)` は定義により `False` なので、`exact t` で証明が閉じます。 ## 8. 構成の計算 (CIC) と Prop Lean の論理は、MLTT とは別の系譜である**構成の計算**（コカンとユエ 1988）に帰納型を加えた**帰納的構成の計算** (CIC) の一種です。最大の違いは、命題専用の宇宙 $\mathsf{Prop}$ を置くことです。 宇宙を $\mathsf{Prop}:\mathsf{Type}_0:\mathsf{Type}_1:\cdots$ と並べる（Lean では $\mathsf{Sort}\ 0=\mathsf{Prop}$、$\mathsf{Sort}\ (u+1)=\mathsf{Type}\ u$）。Π 型の形成規則は、$B(x):\mathsf{Prop}$ ならば、$A$ がどの宇宙にあっても $\Pi_{(x:A)}B(x):\mathsf{Prop}$ とする（**非可述性**）。さらに Lean では、$P:\mathsf{Prop}$ の任意の二つの証明 $h_1,h_2:P$ は定義的に等しい（**証明の無関係性**）。 非可述性により、$\Pi_{(X:\mathsf{Prop})}X\to X$ のように「すべての命題について」量化した命題も、また $\mathsf{Prop}$ に属します。数学で「すべての部分集合について」と量化する感覚に近く、通常の数学を書くのに便利です。証明の無関係性は「証明はどれでも同じ」という数学者の感覚を規則にしたもので、UIP はここから直ちに従います。 その代償として、$\mathsf{Prop}$ の帰納型（`∃`、`∨` など）からは、一般には $\mathsf{Type}$ の値を取り出せません。 次の命題のねらいは、`Prop` の `∃` から証人を取り出せない理由を、前の定理との矛盾として示すことです。証明の無関係性とは、同じ命題の二つの証明を区別しない、という規則です。区別しない以上、「どの証人が入っていたか」を答える関数は作れません。 証明の無関係性のもとで、`∃ n : Nat, True` の証明から自然数を取り出す関数 $w$ で、$w(\langle n,h\rangle)\equiv n$ を満たすものがあるとすると、$0=1$ が導かれる。 $\langle0,\mathsf{trivial}\rangle$ と $\langle1,\mathsf{trivial}\rangle$ はどちらも命題 `∃ n : Nat, True` の証明なので、証明の無関係性により定義的に等しい。$w$ を施すと $0\equiv w(\langle0,\mathsf{trivial}\rangle)\equiv w(\langle1,\mathsf{trivial}\rangle)\equiv1$。これは に反する。 そこで CIC では、`Prop` の帰納型を `Prop` 以外へ除去することを、構成子が高々一つで引数がすべて証明であるもの（`True`、`And`、`Eq` など）に限ります（**部分単集合除去**）。`∃` はこの条件を満たしません。その結果、§4 の型理論版の選択公理を `∃` で書くには、`Prop` の証明から証人を「選ぶ」公理 `Classical.choice` が必要になります。 ```lean theorem ac_prop {A B : Type} {R : A → B → Prop} (h : ∀ x, ∃ y, R x y) : ∃ f : A → B, ∀ x, R x (f x) := ⟨fun x => Classical.choose (h x), fun x => Classical.choose_spec (h x)⟩ #print axioms ac_prop -- 'ac_prop' depends on axioms: [Classical.choice] ``` $\Sigma$ で書けば公理なしの定理、$\exists$ で書けば選択公理が要る。この差が、型理論で選択公理を考えるときの核心です。 | | MLTT | CIC（Lean） | |---|---|---| | 命題 | 型そのもの | `Prop` の元 | | 宇宙 | $\mathcal{U}_0:\mathcal{U}_1:\cdots$（可述的） | `Prop`（非可述的）$:$ `Type 0` $:$ `Type 1` $:\cdots$ | | $\exists$ | $\Sigma$（証人を取り出せる） | `Exists`（`Prop` へしか除去できない） | | UIP | 独立 | 証明の無関係性から成り立つ | | 関数外延性 | 独立 | `Quot.sound` から定理 | | 選択 | $\Sigma$ 版は定理 | `Classical.choice` は公理 | MLTT と、公理を加えない CIC の核の部分は、型検査が決定可能であり、閉じた項が正規形をもつ（したがって $\mathbb{0}$ や `False` の閉項は存在せず、体系は[無矛盾](/mathematics/logic-and-type-theory/incompleteness-theorems#def-metaproperties)である）ことが知られています。ただし Lean 4 の実際のカーネル（商型、証明の無関係性、整礎再帰の `Acc` などを備える）では、定義的同値が決定可能とは限りません（[証明支援系 Lean の仕組み](/mathematics/logic-and-type-theory/lean-kernel) の ）。無矛盾性は ZFC と少しの大きな基数を仮定すれば示されています。それらの証明は前章の強正規化定理（）のテイトの方法を、宇宙と帰納型まで大きく拡張したもので、ここでは主張だけを述べます。もちろん、第二不完全性定理（）により、この無矛盾性の証明はその体系自身の中では行えません。 ## 9. 演習 型 $A,B,C$ について、$(A\times B\to C)\to(A\to B\to C)$ と $(A\to B\to C)\to(A\times B\to C)$ の項を作れ。（$A\times B$ は $\Sigma_{(x:A)}B$。） 前者は $\lambda f.\lambda a.\lambda b.\,f\,(a,b)$。後者は $\lambda g.\lambda p.\,g\,(\mathrm{pr}_1p)\,(\mathrm{pr}_2p)$、あるいは Σ の除去を直接使って $\lambda g.\lambda p.\,\mathrm{split}((x,y)\mapsto g\,x\,y,\ p)$。命題として読めば「$A\wedge B$ ならば $C$」と「$A$ ならば（$B$ ならば $C$）」の同値で、プログラムとしては関数のカリー化です。 $\Pi_{(m,n:\mathbb{N})}\,\mathrm{Id}(\mathrm{succ}(m),\mathrm{succ}(n))\to\mathrm{Id}(m,n)$ の項を作れ（ペアノの第 3 公理）。 前者関数 $\mathrm{pred}:\equiv\lambda n.\,\mathrm{ind}(0,\ \lambda k.\lambda r.\,k,\ n):\mathbb{N}\to\mathbb{N}$ を定める（$C(n):\equiv\mathbb{N}$）。計算規則から $\mathrm{pred}(\mathrm{succ}(k))\equiv k$。$p:\mathrm{Id}(\mathrm{succ}(m),\mathrm{succ}(n))$ に合同（ (4)）を $f=\mathrm{pred}$ で使うと $\mathrm{Id}(\mathrm{pred}(\mathrm{succ}(m)),\mathrm{pred}(\mathrm{succ}(n)))\equiv\mathrm{Id}(m,n)$ の項が得られる。こちらは宇宙なしで証明でき、 との違いは、区別に使う関数の値が $\mathbb{N}$ という「小さい」型で済むことです。 $a:A$ を固定する。J 規則を使って、$\Pi_{(y:A)}\Pi_{(p:\mathrm{Id}_A(a,y))}\,\mathrm{Id}\bigl((a,\mathsf{refl}_a),(y,p)\bigr)$ の項を作れ。ここで右側の $\mathrm{Id}$ は型 $\Sigma_{(w:A)}\mathrm{Id}_A(a,w)$ の中の等号である。 $a$ を固定したままでは J 規則が使えない（J は両端点を動かす）ので、$a$ も動かして $C(x,y,p):\equiv\mathrm{Id}_{\Sigma_{(w:A)}\mathrm{Id}_A(x,w)}\bigl((x,\mathsf{refl}_x),(y,p)\bigr)$ とおく。$C(z,z,\mathsf{refl}_z)$ は $(z,\mathsf{refl}_z)$ とそれ自身の等号なので、$d(z):\equiv\mathsf{refl}_{(z,\mathsf{refl}_z)}$ がその項である。J 規則により $J(d,a,y,p):C(a,y,p)$ で、$\lambda y.\lambda p.\,J(d,a,y,p)$ が求める項になる。「$a$ から出る道の全体」は 1 点に縮む、というホモトピー型理論の基本的な事実の一つです。UIP（$p=\mathsf{refl}_a$ そのもの）とは違い、端点 $y$ も一緒に動かしている点に注意してください。 $f:A\to B$ が「Σ の意味で全射」、すなわち $s:\Pi_{(b:B)}\Sigma_{(a:A)}\mathrm{Id}(f\,a,b)$ をもつとする。$f\circ g$ が各点で恒等写像に等しい $g:B\to A$ を構成せよ。 を $R(b,a):\equiv\mathrm{Id}(f\,a,b)$ に使うと、$g:B\to A$ と $\Pi_{(b:B)}\mathrm{Id}(f(g\,b),b)$ の組が得られる。具体的には $g:\equiv\lambda b.\,\mathrm{pr}_1(s\,b)$、証明は $\lambda b.\,\mathrm{pr}_2(s\,b)$。集合論では「全射は右逆写像をもつ」を選択公理を使って示しました（）が、Σ の意味の全射は右逆写像の情報をすでに含んでいます。 ## 参考文献 - P. Martin-Löf, *Intuitionistic Type Theory*, Bibliopolis, 1984. - B. Nordström, K. Petersson and J. M. Smith, *Programming in Martin-Löf's Type Theory: An Introduction*, Oxford University Press, 1990. - The Univalent Foundations Program, *Homotopy Type Theory: Univalent Foundations of Mathematics*, Institute for Advanced Study, 2013 — 第 1 章（型理論の規則）、第 2 章（恒等型）。 - T. Coquand and G. Huet, "The calculus of constructions", *Information and Computation* 76 (1988), 95–120. - M. Hofmann and T. Streicher, "The groupoid interpretation of type theory", in G. Sambin and J. Smith (eds.), *Twenty-Five Years of Constructive Type Theory*, Oxford University Press, 1998, 83–111. - J. M. Smith, "The independence of Peano's fourth axiom from Martin-Löf's type theory without universes", *The Journal of Symbolic Logic* 53 (1988), 840–845.