CoqでZFC
nyolmol各種記号を定義する
\in
述語記号として
どんなときに
Axiom In: Set -> Set -> Prop.
Infix "∈" := (In) (at level 70).
Notation "x ∉ y" := (~ x ∈ y) (at level 70).
Notation "x ∋ y" := (y ∈ x) (at level 70).
Notation "x ∌ y" := (~ x ∋ y) (at level 70).
ついでに
\subset
Definition Include (x y:Set) :Prop := forall z:Set, z∈x->z∈y.
Notation "x ⊂ y" := (Include x y) (at level 70).
Notation "x ⊃ y" := (Include y x) (at level 70).
Notation "x ⊄ y" := (~ Include x y) (at level 70).
Notation "x ⊅ y" := (~ Include y x) (at level 70).
Notation "x ⊊ y" := (Include x y/\x<>y) (at level 70).
Notation "x ⊋ y" := (~ Include y x/\x<>y) (at level 70).
ZFC
いよいよZFCを追加していきます。
外延性の公理
外延性の公理は、2つの集合が等しいとは何かを定めます。
具体的には、それぞれの集合が持つ要素が同じであれば、2つの集合は同じものだとします。
Axiom Ext: forall x y:Set, x=y <-> (forall e:Set, e∈x<->e∈y).
対の公理
対の公理は、2つの集合からそれらのみを持つような新しい集合を作り出します。
このとき、2つの集合が同じものであれば、新しく作られる集合は1点集合(Singleton)になります。
また、順序対やsuccessorも対の小売があれば定義できます。
Axiom Pair_set: Set -> Set -> Set.
Notation "'ᗭ' x , y 'ᗪ'" := (Pair_set x y) (at level 0, x at level 0, y at level 0): set_scope.
Axiom Pair: forall x y e:Set, e∈ᗭ x , y ᗪ<->(e=x\/e=y)
Notation "'ᗭ' x 'ᗪ'" := (ᗭ x , x ᗪ) (at level 0, x at level 0): set_scope.
Notation "( x , y )" := (ᗭ ᗭ x ᗪ, ᗭ x,y ᗪ ᗪ): set_scope.
Notation "'S' x" := (x∪ᗭ x ᗪ) (at level 0): set_scope.
Coqでは記号
分出公理
分出公理は、ある集合から特定の条件を満たす要素だけを集めてきて部分集合を作り出します。
Axiom Separation_set: Set -> (Set->Prop) -> Set.
Notation "'ᗭ' x ∈ X '|' P 'ᗪ'" := (Separation_set X (fun x=>P)) (at level 0, x at level 0, X at level 99, P at level 99): set_scope.
Axiom Separation_Schema: forall e X:Set, forall P:Set -> Prop, (e ∈ ᗭ x ∈ X | P x ᗪ <-> e∈X /\ P e).
和集合の公理
和集合の公理は、ある集合からその要素の要素をかき集めて新しい集合を作ります。
おそらく最初は
このとき、
より一般に、
Axiom Union_set: Set -> Set.
Notation "∪ x" := (Union_set x) (at level 45, right associativity): set_scope.
Axiom Union: forall X x:Set, x∈∪X <-> exists e:Set, e∈X/\x∈e.
Notation "x ∪ y" := (∪ᗭ x,y ᗪ) (at level 50, left associativity): set_scope.
分かりやすさと書きやすさのために、
冪集合の公理
冪集合は、ある集合からその部分集合を全て集めて作られる集合です。
Axiom Power_set: Set -> Set.
Notation "'Ƥ' x" := (Power_set x) (at level 30, right associativity): set_scope.
Axiom Power: forall x u:Set, (u∈Ƥ x<->u⊂x).
ちなみにこのƤは主にアフリカで使われるフック付きPというものです。
無限集合の公理
無限集合の公理では、"初めて"集合の存在を認めます。
上で述べてきた公理は「何か集合があれば、新しい集合が作れる」というものだったのですが、これだけでは空虚な土台の上に議論を積み重ねるだけなので、はじめに集合の存在を認めなければいけません。
Axiom Infinity_set:Set.
この無限集合が満たすべき性質(公理)を述べる前に∅の存在について確認します。
∅の存在
Definition Empty_set := ᗭ x∈Infinity_set| x<>x ᗪ.
Notation "∅" := (Empty_set): set_scope.
一つでも集合が存在すれば、分出公理のおかげでいとも簡単に∅が作れてしまいますね。
∅が作れたところで、無限集合の公理を述べられます。
Definition inductive x := ∅∈x/\forall y:Set, y∈x->S y∈x.
Axiom Infinity: inductive Infinity_set
無限集合の公理とは、上にあるようにinductiveという性質を満たす集合の存在を認める公理です。
これは一意的ではありません。(つまりinductiveを満たす集合はたくさんあります。)
正則性公理
正則性公理は、∅でない全ての集合に対して、ある性質を保証します。
この性質は「自分の要素を1つも含まない要素が存在する」というもので、言い換えれば「自分と自身の要素の共通部分を考えたとき、∅になる要素が存在する」というものです。
Axiom Regular: forall x:Set, x<>∅->exists y:Set, y∈x/\forall z:Set, z∈x->z∉y.
これにより
選択公理
選択公理のための準備
選択公理を簡単な形で述べるために、直積と関数について簡単な定義を行います。
直積
関数に関しても集合で表現したいので、
Definition cartesian_product (x y:Set):Set := ᗭ p∈Ƥ Ƥ (x∪y) | exists a b:Set, p=(a,b)/\a∈x/\b∈y ᗪ.
Notation "x × y" := (cartesian_product x y) (at level 50, left associativity): set_scope.
Definition dom (R:Set):Set := ᗭ u∈∪(∪(R))|exists v:Set, (u,v)∈R ᗪ.
Definition ran (R:Set):Set := ᗭ v∈∪(∪(R))|exists u:Set, (u,v)∈R ᗪ.
Definition function (f X Y:Set):Prop := f⊂X×Y/\dom f=X/\ran f⊂Y/\forall a b c:Set, (a,b)∈f/\(a,c)∈f->b=c.
Notation "f : X → Y" := (function f X Y) (at level 80):set_scope.
Definition substitution (f x:Set):Set := ∪ᗭ y∈ran f | (x,y)∈f ᗪ.
Notation "f ← x" := (substitution f x) (at level 50):set_scope
選択公理
いよいよ選択公理を実装します。
選択公理とは、∅を要素に持たない集合に対して、選択関数というものの存在を保証します。
Axiom Choice: forall x y:Set, y∈x /\ y<>∅ -> exists f:Set, f:x→∪x /\ f←y ∈ y.
具体的には