「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾壱「デカルト積の応用」(予習編)
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コンビネータの型はヒルベルト流命題論理の公理である。なのでもちろん自然演繹で証明できるはず。 をすべて項に依存しないものとすると
とみなせるので命題論理の論理式が得られる。