Per Martin-Löfの"Intuitionistic Type Theory"(1984)の勉強会の記録。他の回はこちらから。
今回は「デカルト積の応用」の節のみ。
登場する論理規則は以下の画像を参照。比較のために等号規則を除いた規則も載せた。
含意の定義
これは が に依存しない(つまり、 という集合族ではない)ときに成り立つ。これが の定義となる。
全称量化
規則を "propositions as sets" 解釈で見ると、
と定義できて、 の規則が得られる。
形成則
これはつまり、全称量化が命題を形成するということ。 というのは、全称量化の範囲が集合であるということを意味する。なので とはしない。 形成則は 形成則のただのインスタンスであることに注意。
導入則
これは 導入則から証明(proof, construction) を隠す(suppressing)ことで得られる。 を命題とみなし、その証明がなんであるかが重要でない場合は一般に、なんらかの を使って とするのではなく と書く。
より一般的に、複数の仮定付きだと以下のようになる。
から と は にしか依存していない。 の真理のみを考えるならば、 の要素を書くのは本質的ではない。なので
と略す。同じように
は
とする。
しかし集合族と要素の関数のインデックスの数が違うというケースは今まで出てこなかった気がする。ちょっと妙な感じがした。
除去則
という の証明を持ってくると、Apは の証明となる。 の証明は任意の の要素を の証明にうつすメソッドである。これは直観主義の全称量化の解釈と一致する。
含意
が に依存しないとして
と定義すると、 規則から含意の規則が得られる。
形成則
ここで言っている generalization の意味がよくわからなかった。
通常は と が命題のとき も命題と定義すると思う。しかし実際には も必要だろうということが述べられている。これはコルモゴロフの立場と相性が良い。コルモゴロフの命題を問題と見る解釈では、 が問題であると判断するのに問題 が解けることを仮定する必要がある場合に となる。
導入則と除去則
導入則は証明を隠している。除去則も同様。
例:SKIコンビネータ
いわゆるSKIコンビネータがこれまでの規則で構成できる証明であることを示す。証明は以下の画像を参照。
Iコンビネータ
は命題 の証明であり、それはなんらかの の証明を同じ証明にうつすメソッドである。これは によらず という形のどのような集合にもあてはまる。 という形のどのような命題も真となる。
Kコンビネータ
ここでは本文にλ抽象と書かれているのをすべて 導入則と置き換えている。
Kコンビネータは、 のどんな証明 に対しても から への関数で のどの要素 も にうつすものを与えるメソッドである。 は の証明なので は真である。
Sコンビネータ
Sコンビネータはやや複雑なのでそれがどのようなメソッドかというのはIやKほど直観的に言えないかも。
ヒルベルト流
KコンビネータとSコンビネータの型はヒルベルト流命題論理の公理である。なのでもちろん自然演繹で証明できるはず。 をすべて項に依存しないものとすると とみなせるので命題論理の論理式が得られる。