「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ拾壱「デカルト積の応用」（予習編）

　Per Martin-Löfの"Intuitionistic Type Theory"（1984）の勉強会の記録。他の回はこちらから。

　今回は「デカルト積の応用」の節のみ。

　登場する論理規則は以下の画像を参照。比較のために等号規則を除いた $\Pi$ 規則も載せた。

f:id:cut_elimination:20210612111137j:plain

含意の定義

　 $B^A \equiv A \to B \equiv (\Pi x \in A)B$

これは $B$ が $x$ に依存しない（つまり、 $B(x)$ という集合族ではない）ときに成り立つ。これが $A \to B$ の定義となる。

全称量化

　 $\Pi$ 規則を "propositions as sets" 解釈で見ると、

　 $(\forall x \in A)B(x) \equiv (\Pi x \in A)B(x)$

と定義できて、 $\forall$ の規則が得られる。

$\forall$ 形成則

　これはつまり、全称量化が命題を形成するということ。 $A \; set$ というのは、全称量化の範囲が集合であるということを意味する。なので $A \; prop$ とはしない。 $\forall$ 形成則は $\Pi$ 形成則のただのインスタンスであることに注意。

$\forall$ 導入則

　これは $\Pi$ 導入則から証明（proof, construction） $b(x)$ を隠す（suppressing）ことで得られる。 $A$ を命題とみなし、その証明がなんであるかが重要でない場合は一般に、なんらかの $a$ を使って $a \in A$ とするのではなく $A \; true$ と書く。

　より一般的に、複数の仮定付きだと以下のようになる。

$a(x_1, ..., x_n) \in A(x_1, ..., x_m)$

　 $(x_1 \in A_1, ..., x_m \in A_m(x_1, ..., x_{m-1}),$

　　 $x_{m+1} \in A_{m+1}(x_1, ..., x_m), ..., x_n \in A_n(x_1, ..., x_m))$

$A_{m-1}$ から $A_n$ と $A$ は $x_1, ..., x_m$ にしか依存していない。 $A(x_1, ..., x_m)$ の真理のみを考えるならば、 $A_{m+1}, ..., A_n$ の要素を書くのは本質的ではない。なので

$A(x_1, ..., x_m) \; true$

　 $(x_1 \in A_1, ..., x_m \in A_m(x_1, ..., x_{m-1}),$

　　 $A_{m+1}(x_1, ..., x_m) \; true, ..., A_n(x_1, ..., x_m) \; true)$

と略す。同じように

$A(x_1, ..., x_m) \; prop$

　 $(x_1 \in A_1, ..., x_m \in A_m(x_1, ..., x_{m-1}),$

　　 $x_{m+1} \in A_{m+1}(x_1, ..., x_m), ..., x_n \in A_n(x_1, ..., x_m))$

は

$A(x_1, ..., x_m) \; prop$

　 $(x_1 \in A_1, ..., x_m \in A_m(x_1, ..., x_{m-1}),$

　　 $A_{m+1}(x_1, ..., x_m) \; true, ..., A_n(x_1, ..., x_m) \; true)$

とする。

　しかし集合族と要素の関数のインデックスの数が違うというケースは今まで出てこなかった気がする。ちょっと妙な感じがした。

$\forall$ 除去則

　 $c$ という $(\forall x \in A)B(x)$ の証明を持ってくると、Ap $(c, a)$ は $B(a)$ の証明となる。 $(\forall x \in A)B(x)$ の証明は任意の $A$ の要素を $B(a)$ の証明にうつすメソッドである。これは直観主義の全称量化の解釈と一致する。

含意

　 $B$ が $x$ に依存しないとして

　 $A \supset B \equiv A \to B \equiv B^A \equiv (\Pi x \in A)B$

と定義すると、 $\Pi$ 規則から含意の規則が得られる。

$\supset$ 形成則

　ここで言っている generalization の意味がよくわからなかった。

　通常は $A$ と $B$ が命題のとき $A \supset B$ も命題と定義すると思う。しかし実際には $A \; true$ も必要だろうということが述べられている。これはコルモゴロフの立場と相性が良い。コルモゴロフの命題を問題と見る解釈では、 $B$ が問題であると判断するのに問題 $A$ が解けることを仮定する必要がある場合に $A \supset B$ となる。

$\supset$ 導入則と除去則

　導入則は証明を隠している。除去則も同様。

例：SKIコンビネータ

　いわゆるSKIコンビネータがこれまでの規則で構成できる証明であることを示す。証明は以下の画像を参照。

f:id:cut_elimination:20210604055623j:plain

Iコンビネータ

　 $I \equiv (\lambda x)x$ は命題 $A \supset A$ の証明であり、それはなんらかの $A$ の証明を同じ証明にうつすメソッドである。これは $A$ によらず $A \to A$ という形のどのような集合にもあてはまる。 $A \supset A$ という形のどのような命題も真となる。

Kコンビネータ

　ここでは本文にλ抽象と書かれているのをすべて $\Pi$ 導入則と置き換えている。

　Kコンビネータは、 $A$ のどんな証明 $x$ に対しても $B$ から $A$ への関数で $B$ のどの要素 $y$ も $x$ にうつすものを与えるメソッドである。 $K \equiv (\lambda x)(\lambda y)x$ は $A \supset (B \supset A)$ の証明なので $A \supset (B \supset A)$ は真である。