単純型理論 = HOL — 高階論理の土台

Q: 単純型理論とは何か

単純型理論は、Church (1940) が与えた型付きラムダ計算に基づく体系である。すべての項に型を割り当て、関数 $f$ を型 $\sigma \to \tau$、その引数を型 $\sigma$ にそろえることで、自己適用のような危険な式を文法の段階で排除する。この型付きラムダ計算の上に、真理値型 $o$ と等号・量化子を加えたものが高階論理 (HOL) である。

Q: 一階論理と高階論理はどう違うのか

一階論理は個体だけを量化できる（「すべての $x$ について」の $x$ は個体）。高階論理は、述語や関数そのものも量化できる（「すべての性質 $P$ について」「すべての関数 $f$ について」）。たとえば数学的帰納法の原理「すべての性質 $P$ が成り立つ」は高階の量化で素直に書ける。表現力は高いが、完全性などの性質は一階論理より弱くなる。

Q: なぜ証明アシスタントは HOL を土台にするのか

HOL は、型付きラムダ計算という機械的に扱いやすい構文の上に、ごく少数の公理（等号、選択、無限）だけを置いて多くの数学を展開できる。型検査が決定可能で、推論規則が単純なため、小さな信頼カーネルとして実装しやすい。HOL Light や Isabelle/HOL はこの単純型理論版の HOL を基盤にしている。

型付きラムダ計算の上に論理を立てる

このページの目標

単純型（基底型と関数型）と型付きラムダ計算を理解し、その上に等号と量化子を載せた高階論理 (HOL) が、述語や関数まで量化できる体系であることをつかむ。これが HOL Light / Isabelle の基盤であることを知る。

1. なぜ型が要るか

素朴に「何でも関数に適用してよい」とすると、$x\,x$（$x$ を自分自身に適用する）のような式が書けてしまう。素朴集合論で矛盾を生んだ Russell のパラドックス「自分自身を含まない集合の集合」も、本質はこの無制限な自己適用である。

Church は、すべての項に型を割り当て、関数とその引数の型を一致させることで、この危険を文法の段階で断つことにした。型の合わない式は「そもそも書けない」。これが単純型理論（単純型付きラムダ計算、1940）である。

2. 単純型 — 基底型と関数型

型は、ごく少数の基底型から関数型を組み立てて作る。HOL では基底型を二つ置く。

$\iota$（イオタ）：個体の型（対象。たとえば自然数や点）
$o$（オミクロン）：真理値の型（命題。真・偽の二値）

そして、型 $\sigma, \tau$ から関数型 $\sigma \to \tau$（$\sigma$ を受け取り $\tau$ を返す関数の型）を作る。$\to$ は右結合で読み、$\sigma \to \tau \to \rho$ は $\sigma \to (\tau \to \rho)$ を表す。

型付けの規則（要点）

項 $t$ が型 $\tau$ をもつことを $t : \tau$ と書く。基本は二つだけである。

適用：$f : \sigma \to \tau$ と $a : \sigma$ なら $f\,a : \tau$。
抽象：$x : \sigma$ のもとで $t : \tau$ なら $\lambda x{:}\sigma.\, t : \sigma \to \tau$。

$$\dfrac{f : \sigma \to \tau \quad a : \sigma}{f\,a : \tau} \qquad \dfrac{x:\sigma \;\vdash\; t : \tau}{\lambda x{:}\sigma.\,t : \sigma \to \tau}$$

適用は「引数の型 $\sigma$ がぴたり合うときだけ許される」。だから $x\,x$ は、$x$ が $\sigma \to \tau$ かつ同時に $\sigma$ でなければならず、$\sigma \neq \sigma \to \tau$ ゆえ型がつかない。自己適用は文法で弾かれる。

述語は、個体を受け取って真理値を返す関数 $\iota \to o$ として表す。たとえば「$x$ は素数である」は $\iota \to o$ 型の項である。二項関係は $\iota \to \iota \to o$ 型になる。

3. 高階の量化

一階論理では、量化できるのは個体だけである（「すべての $x$ について」の $x$ は型 $\iota$）。高階論理では、述語や関数そのもの、つまり $\iota \to o$ や $\iota \to \iota$ のような高い型の対象も量化できる。

量化子 $\forall$ は、述語（型 $\iota \to o$）を受け取って真理値（型 $o$）を返す高階の関数とみなせる。個体上の全称量化は型 $(\iota \to o) \to o$ をもつ。

図 1: 高階の量化。述語 $P$ は型 $\iota \to o$ をもち、全称量化子 $\forall$ はその述語を受け取って真理値 $o$ を返す型 $(\iota \to o) \to o$ をもつ。述語そのものを量化できる（$\forall P.\,\dots$）のが高階論理の特徴である。

図 1 の内容をテキストで読む

述語 $P$ は個体 $\iota$ を受け取り真理値 $o$ を返すので型は $\iota \to o$。全称量化子 $\forall$ はその述語 $P$ を引数として受け取り、真理値 $o$ を返すので型は $(\iota \to o) \to o$。一階論理は個体 $x$ だけを量化するが、高階論理は述語 $P$ のような高い型の対象も量化できる。

高階の量化があると、数学的帰納法のような「すべての性質 $P$ について」という原理を、メタな注釈ではなく体系内の一つの論理式として書ける。表現力は大きいが、その代償として、一階論理がもつ完全性（妥当な論理式はすべて証明できる）は標準意味論のもとでは成り立たない（上級編の不完全性と関係する）。

4. HOL — 少数の公理から

単純型付きラムダ計算に、真理値型 $o$ と等号 $=$、そして論理結合子・量化子を加えたものが高階論理 (HOL) である。注目すべきは、HOL では等号を最も基本的なものとし、他の結合子をそこから定義できる点である（たとえば「真」は $(\lambda x.\,x) = (\lambda x.\,x)$ などとして導入できる）。

HOL Light や Isabelle/HOL は、この体系をごく少数の公理の上に立てる。代表的には次の三つである。

等号の公理（反射性・置換など、等しいものは置き換えてよい）
選択（Hilbert の $\varepsilon$：性質 $P$ を満たすものが存在すれば一つ選び出せる。公理は $(\exists x.\,P\,x) \Rightarrow P(\varepsilon\,P)$ で、$\varepsilon\,P$ は「$P$ を満たすもの（あれば）」を表す）
無限（個体の型 $\iota$ が無限であることを保証し、自然数を構成できる）

この小さな出発点から、自然数・実数・集合論的な構成までを定義し、多くの数学を機械検証可能な形で展開できる。型検査が決定可能で推論規則も単純なので、小さな信頼カーネルとして実装しやすい。これが、HOL が証明アシスタントの土台に選ばれる理由である（証明アシスタント概観・LCF）。

まとめ

この章のポイント

単純型理論：基底型 $\iota$（個体）・$o$（真理値）と関数型 $\sigma \to \tau$ で型を組み立てる
型を合わせることで $x\,x$ のような自己適用を文法の段階で排除する
述語は $\iota \to o$、二項関係は $\iota \to \iota \to o$ で表す
高階の量化：述語や関数そのものを量化できる（$\forall P.\,\dots$）
HOL＝型付きラムダ計算＋等号・量化子。少数の公理（等号・選択・無限）から数学を展開し、HOL Light / Isabelle の土台になる

よくある質問

単純型理論とは何か

Church (1940) が与えた型付きラムダ計算に基づく体系である。すべての項に型を割り当て、関数 $f$ を $\sigma \to \tau$、その引数を $\sigma$ にそろえることで、自己適用のような危険な式を文法の段階で排除する。この型付きラムダ計算の上に真理値型 $o$ と等号・量化子を加えたものが高階論理 (HOL) である。

一階論理と高階論理はどう違うのか

一階論理は個体だけを量化できる。高階論理は述語や関数そのものも量化できる（「すべての性質 $P$ について」）。数学的帰納法の原理を体系内の一つの論理式として書けるなど表現力は高いが、完全性などの性質は一階論理より弱くなる。

なぜ証明アシスタントは HOL を土台にするのか

型付きラムダ計算という機械的に扱いやすい構文の上に、ごく少数の公理（等号・選択・無限）だけで多くの数学を展開でき、型検査が決定可能で推論規則も単純なため、小さな信頼カーネルとして実装しやすい。HOL Light や Isabelle/HOL はこの HOL を基盤にしている。