よく使う Coq.Logic の公理
Coq.Logic にはCoqの集合論モデルにおいて正しい公理や、それらの間の関係が記述されている。
ここではその一部を取り上げて、意味を説明する。
前提知識
公理を仮定しない状態では、
- Coqの論理は直観主義論理である。
- ある2つが「等しい」という命題が証明できる場合は限定される。
- 証明の文脈(Prop)における「AまたはB」と、値の文脈(Set/Type)における「AまたはB」は区別される。前者から情報を取り出すことはできないようになっている(マッチングの型検査で弾かれる。)
以下、公理の説明
決定性の値の取り出し (description)
「条件を満たすものが唯一存在する」という命題から、具体的にその値を取り出す。
これによって証明できることは、例えば以下の内容がある。
- 二項関係であって関数としての条件を満たしているものから、関数を取り出す。
決定性の古典論理
場所: Coq.Logic.ClassicalDescription
名前どおり、Classical と Description を組み合わせたものである。
これによって証明できることは、例えば以下の内容がある。
- ある命題が正しいかどうかによる条件分岐を、関数中に書くことができる。
ジョン・メジャーの等式 (John Major's equality)
場所: Coq.Logic.JMeq
「型Aとその値の対」について、「型も等しいし、その値も等しい」という関係を考える。
「型Aと値x」と「型Aと値y」がこの意味で等しいとき、 x = y である。しかしこれはCoqでは公理なしでは導けない。これを仮定するのが JMeq である。
関数外延性 (functional extensionality)
場所: Coq.Logic.FunctionalExtensionality
二つの関数が等しいとは、どの値を入れても等しいことである。しかしこれはCoqでは公理なしでは導けない。これを仮定するのが FunctionalExtensionality である。
命題外延性 (propositional extensionality)
二つの命題が同値(A <-> B, 互いから互いを導ける)ならば、二つの命題は等しい(A = B)とみなしてよい。これにちょうど対応する公理はなぜか Coq の標準ライブラリにはない。次を参照のこと。
部分集合についての集合外延性 (extensionality of ensembles)
Aの部分集合を、所属関係を表す関数 A -> Prop で表すことにする。二つの部分集合が等しいとは、互いに包含していることとして定義される。
Ensembles に定義されている集合外延性 Extensionality_Ensembles は、関数外延性+命題外延性 よりは弱く、関数外延性よりは強い。
非決定性の値の取り出し (indefinite description)
場所: Coq.Logic.IndefiniteDescription
「条件Pを満たす値が存在する」という命題から、具体的に値を取り出す。(一意性は要求されない。)これは明らかにDescriptionより強い公理である。
IndefiniteDescriptionで言えることは、集合論における「選択公理」から導けることとほぼ同じだと思ってよい。