集合論の公理

• 集合論の公理。
• ファイルは、a1Axset.v
• 集合論においては、何かの集まりがすぐ集合となるわけではない。何かの集まりはまずクラスと呼ばれる。集合論の公理から「集合であることが証明され」てはじめて集合であることがわかる。集合ではないと証明されるクラスももちろんある。

Require Export Nota.

(*公理1　集合の相等*)
Definition Set_eq := forall (a b:Set), (a /= b) -> a = b.

• 逆の(a = b) -> (a /= b)は、集合論の公理とは無関係に論理的に証明できる。

(*空集合の存在*)
Definition ExEmp := exists y:Set, forall x:Set, ~ (x /e y).

• yはどんなxも要素に持たないのである。そんなyが存在すると主張しているのである。

(*対集合の存在*)
Definition SPair := forall a b:Set, exists y:Set, forall x:Set,
 (x /e y) <-> ((x = a) \/ (x = b)).

• yの要素は、a、bのいずれかであるし、a、bのいずれかであれば、yの要素である、と言っている。つまり、yはa、bのみを要素に持つ集合である。

(*和集合の存在*)
Definition SSum := forall x:Set, exists y:Set, forall z:Set,
 (z /e y) <-> exists u:Set, ((z /e u) /\ (u /e x)).

(*冪集合の存在*)
Definition SPow := forall x:Set, exists y:Set, forall z:Set,
 (z /e y) <-> (z /c= x).

(*置換公理図式*)
(*変数条件　Pの中にuがあるのはかまわないが、vはあってはならない*)
Definition SRepl := forall P:Set -> Set -> Prop,
 (forall x y z:Set, (P x y) -> (P x z) -> y = z) ->
    forall u:Set, exists v:Set, forall y:Set,
      (y /e v) <-> exists x:Set, ((x /e u) /\ (P x y)).

• P x yが成立するようなyは、xに対して高々1つしかないというのが、Pの条件である。関数（写像）のような条件である。

(*分出公理図式または内包性公理図式*)
(*変数条件　Pの中にuがあるのはかまわないが、vはあってはならない*)
Definition SCom := forall P:Set -> Prop,
 forall u:Set, exists v:Set, forall y:Set,
  (y /e v) <-> ((y /e u) /\ (P y)).

• uが集合なら、uの要素だけで得られるvも集合である、と主張している。

(*選択公理*)
Definition AC :=
 forall z:Set,
  (forall x:Set, (x /e z) -> exists w:Set, w /e x) ->
  (forall x y:Set, (x /e z) -> (y /e z) -> (exists w:Set, (w /e x) /\ (w /e y)) -> x = y) ->
   exists u:Set, forall x:Set, exists a:Set, (x /e z) -> (u /a x)=({` a }).

(*選択公理2 選択関数版*)
Definition ACf :=
 forall x:Set, (forall w:Set, (w /e x) -> exists v:Set, v /e w) ->
  exists f:Set, forall y:Set, (y /e x) -> ((f ` y) /e y).

Definition ACfm :=
 forall x:Set, (forall w:Set, (w /e x) -> exists v:Set, v /e w) ->
  exists f:Set, (Func f) /\ ((Dom f) = x) /\ forall y:Set, (y /e x) -> ((f ` y) /e y).

(*正則性公理。基礎の公理*)
Definition SReg :=
 forall x:Set, (exists y:Set, y /e x) ->
  exists y:Set, (y /e x) /\ forall z:Set, ~ ((z /e x) /\ (z /e y)).

もどる