よく使う Coq.Logic の公理

Coq.Logic にはCoqの集合論モデルにおいて正しい公理や、それらの間の関係が記述されている。

ここではその一部を取り上げて、意味を説明する。

前提知識

公理を仮定しない状態では、

  • Coqの論理は直観主義論理である。
  • ある2つが「等しい」という命題が証明できる場合は限定される。
  • 証明の文脈(Prop)における「AまたはB」と、値の文脈(Set/Type)における「AまたはB」は区別される。前者から情報を取り出すことはできないようになっている(マッチングの型検査で弾かれる。)

以下、公理の説明

古典論理 (classical logic)

場所: Coq.Logic.Classical

古典論理で証明できることは、例えば以下の内容がある。

決定性の値の取り出し (description)

場所: Coq.Logic.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)

場所: Coq.Sets.Ensembles

Aの部分集合を、所属関係を表す関数 A -> Prop で表すことにする。二つの部分集合が等しいとは、互いに包含していることとして定義される。

Ensembles に定義されている集合外延性 Extensionality_Ensembles は、関数外延性+命題外延性 よりは弱く、関数外延性よりは強い。

非決定性の値の取り出し (indefinite description)

場所: Coq.Logic.IndefiniteDescription

「条件Pを満たす値が存在する」という命題から、具体的に値を取り出す。(一意性は要求されない。)これは明らかにDescriptionより強い公理である。

IndefiniteDescriptionで言えることは、集合論における「選択公理」から導けることとほぼ同じだと思ってよい。