第 1 章

命題は型である

定理証明器は証明が正しいかどうかを判定しなければならないが、自然言語で書かれた証明は計算機には検査できないので、プログラムが調べられる形で証明を表現する必要がある。本章では、以降のすべてを可能にする考えを導入する。証明はプログラムであり、命題はその型であり、証明の検査は型検査である。

証明はプログラムである

命題「 $A$ ならば $B$ 」の証明を、ふつうの数学の文章で書くとこうなる。

$A$ を仮定する。すると……（何らかの議論）……ゆえに $B$ が成り立つ。

この証明の形は関数であり、何か、つまり $A$ を信じる根拠を受け取って、別の何か、つまり $B$ を信じる根拠を作り出す。これを文字どおりに受け取って「 $A$ を信じる根拠」を型 $A$ の値とみなせば、 $A \to B$ の証明は $A$ から $B$ への関数であり、命題 $A \to B$ はその関数の型である。

この観察が Curry-Howard 対応（Curry-Howard correspondence）である。それによれば、

命題は型であり、
その命題の証明はその型の項であり、
命題 $A$ が真であるのは、型 $A$ の項 $t$ が存在するとき、そのときに限る。これを $t : A$ と書く。

これだけでどこまで行けるかを、三つの例で示す。左が命題、中央が関数として書いたその証明、右が証明の考えを言葉にしたものである。ここで $\lambda x.\,e$ は、 $x$ を受け取って $e$ を返す関数を表す。

命題	証明	言葉で言えば
$P \to P$	$\lambda p.\,p$	仮定をそのまま返す。
$A \to B \to A$	$\lambda a.\,\lambda b.\,a$	二つ目の仮定を無視する。
$(A \to B) \to (B \to C) \to A \to C$	$\lambda f.\,\lambda g.\,\lambda a.\,g\,(f\,a)$	二つの含意を合成する。

三行目をもう一度見てほしい。含意が推移的であることを証明するには、 $A \to B$ と $B \to C$ を仮定し、 $A$ が与えられたら、一つ目の仮定を適用して $B$ を得て、二つ目を適用して $C$ を得る。証明項はまさにそれを言っており、 $f$ と $g$ が仮定、 $a$ が $A$ の証明で、 $g\,(f\,a)$ がそれらを順に適用する。仮定を使うことは関数を適用することである。これこそが、仮定を言い直すだけの作業と本当の推論を分ける一歩であり、第 3 章で再び取り上げる。

量化子は依存関数になる

同じ考えは「すべての」にも広がる。すべての $x : A$ について $B(x)$ が成り立つことを証明するには、どんな $x$ を渡されても $B(x)$ の証明を作り出す方法を与えればよい。これもやはり関数だが、返り値の型が引数に依存するというひとつのひねりがある。 $x = 3$ なら $B(3)$ の証明を返し、 $x = 7$ なら $B(7)$ の証明を返す。結果の型が引数に言及してよい関数型を依存関数型（dependent function type）または $\Pi$ 型と呼び、次のように書く。

\Pi(x : A).\,B(x).

ふつうの関数型 $A \to B$ は、 $B$ が $x$ に言及しない特別な場合である。

たとえば「すべての命題は自分自身を含意する」は命題の上の量化である。 $\Sort{0}$ を命題の型とすれば、この主張は

\tPi{P}{\Sort{0}}{P \to P},

であり、その証明は、命題 $P$ を受け取り、次に $P$ の証明 $p$ を受け取って、 $p$ を返す関数である。

\tLam{P}{\Sort{0}}{\tLam{p}{P}{p}}.

束縛子に型が付いていることに注意してほしい。 $\lambda(P : \Sort{0})$ は $P$ が命題の範囲を動くことを言い、 $\lambda(p : P)$ は $p$ が渡されたその $P$ の証明であることを言う。型検査器にはこの注釈が必要になる。

カーネルの仕事

ここから定理証明器の中心となる考えが得られる。

定理を証明するとは要求された型の項を構成することであり、証明を検証するとはその項を型検査することである。

カーネルは真偽について推論するのではなく、項がいつ型を持つかを定める型付け規則を実装し、与えられた項が与えられた型をその規則のもとで持つことを機械的に検査するだけである。それが証明の検査と呼べるかどうかは、型付け規則がある論理を忠実に実装しているかどうかにかかっており、それは第 4 章の主題である。規則が健全（sound）であるか、すなわち偽の命題の型に住む項が存在しないかは、第 13 章と第 14 章の主題である。

この分業が、本格的な証明器の設計を方向づける。タクティクや自動化、決定手続き、さらには大規模言語モデルが証明を探す役を担い、そこにバグがあっても、出力された項はカーネルが検査する。正しさが求められるのはカーネルだけなので、できるだけ小さく保つことが設計目標になり、本書のカーネルはコメントを含めても千五百行に満たない Rust である。

本書の計画

第 I 部の各章では、論理として使えるぎりぎりの大きさの型理論に対するカーネルを作る。

第 2 章で言語を固定する。宇宙、変数、 $\Pi$ 型、 $\lambda$ 抽象、適用である。
第 3 章で型付け規則を与える。項の種類ごとに一つと、型の内部で計算を許すための一つである。
第 4 章でこれらの規則がある論理の規則であることを示し、整合性を定義する。
第 5 章で規則をアルゴリズムに変え、Rust の実装と突き合わせる。
第 6 章で、正しい証明、誤った証明、計算を必要とする証明に対して、アルゴリズムを手で動かす。

二つの操作、代入と定義的等価は、第 III 部まで意図的にブラックボックスとして扱う。どちらも述べるのは簡単で、間違えるのも簡単であり、カーネルの正しさはこの二つにかかっている。

覚えておくこと

命題は型、証明は項であり、 $t : A$ は $t$ が $A$ を証明することを意味する。
含意は関数型であり、仮定を使うことは関数を適用することである。
全称量化は依存関数型 $\Pi(x : A).\,B(x)$ である。
定理証明器のカーネルは型検査器であり、それ以外のすべては、カーネルが検査する項を作るだけである。