LEAN解説【前集合】

数学の基本的な対象と言えば集合ですが、集合と集合の間の関係は等号や包含関係などの同じレベルの関係から、含意、べき集合などの集合と異なるレベルとしての関係等様々です。

もしこれらを集合の枠組みで二項関係を定義しようと思うと、集合の型に統一してから定義する必要があります。

また、通常の集合論的な集合では、集合の名前は全く重要ではなくその集合の要素だけが集合自体を特徴づけますが、型理論的な集合を定義しようとすると、集合の要素の型の情報が、集合の型として残っています。

これは型理論的に集合の型を定義しようとするときには余計な情報ですので、集合の方を区別しない定義を行う必要があります。

実際、LEANライブラリの集合ではまず、型と要素の型を集合への変換する関数の２組から成る前集合の型を定義し、集合の型は前集合の型から型の情報を取り除いた（即ち、型が違っても前集合として同じなら同じ集合とみなす）ものとして定義されます。

---

以下が前集合の定義です：

/-- universe `u` 上の pre-sets 型. pre-set ⟨α, A⟩ と表されるとき、
    α が pre-set を表す型で、A がbase changeを表す.

    型α を持つ対象 a: α に対し、a 自身もpre-setである. a 自身を
    pre-set として扱う場合は `A a` のようにbase型をpSetに変更する.

    ZFC の世界は pre-sets から外延性を保証した同値類として定義される. -/
inductive pSet : Type (u+1)
| mk (α : Type u) (A : α → pSet) : pSet

前集合は上から降りてくる形で帰納的に定義されます。つまり、例えばαが前集合であった場合、αの型を持つ要素も前集合であることを保証します。

これにより、前集合の枠組みで命題の証明や定義を行う場合は、外側の前集合で命題が成り立つことを仮定して、その要素について命題が成り立つを証明する流れになります。

---

例えば、集合が等しいことの定義はLEANでは以下のようにして行われます：

def equiv (x y : pSet) : Prop
:= begin

    -- 与えられた2つの集合に対し、命題を構成する
    -- -i.e. `pre-sets x, y に関する命題` を見つけたい
    -- ⟶ `pSet.rec`を用いる
    -- `pre-sets x とその要素であるpre-sets a ∈ x → pre-sets y に関する命題`
    -- -i.e. `pSet → (α → pSet → Prop) → pSet → Prop` の型を持つ論理命題を見つけたい
    -- ⟶ `(α: Type u) → (A: α → pSet) → (m: α → pSet → Prop) → pSet → Prop`
    -- ※ m は 型α を持つ対象のbese型をpSetに統一して等しいかどうか比較する命題
    -- ※ `m (a: Type(x)) (y: pSet)` = `( x の要素: Type x ) =?= ( y の要素: pSet )`
    refine pSet.rec _ x y; clear x y,

    
    -- `α`: pre-setsの型
    -- `A`: base change
    -- `m`: pre-sets の型として命題
    -- `w := ⟨β, B⟩`: もうひとつのpre-sets family
    -- `β`: pre-setsの型
    -- `B`: base change
    assume α z m w,
    cases w with β B,

    -- 任意の `要素a: α` に対しある `要素b: β` が存在して `a = b in pSet type`
    -- 任意の `要素b: β` に対しある `要素a: α` が存在して `a = b in pSet type`
    exact
        (∀(a: α), ∃(b: β), m a (B b))
            ∧
        (∀(b: β), ∃(a: α), m a (B b)),
end

pSet.recはpSetをinductiveとして定義した場合に一緒に定義されるもので、命題を、型を構成する要素の命題に置き換えます。

従って、実際に前集合のequivについて言及するときは、equivはmに置き換えて証明したりすることになります。