記述

• 集合を表す変数の型はSetを、クラスを表す変数の型はSet -> Propを用いることにする。
• ファイルは、Nota.v

------------------------------------------------------------------------
(*Element a bで、a∈bを表すことにしよう*)
Parameter Element : forall A:Type, Set -> A -> Prop.
Implicit Arguments Element [A].

• このImplicit命令によってElementの第1引数は、必ず省略しなければならなくなる。
  Elementの第2引数の型はSetでなければならないが、第3引数の型は第1引数と同じでなければエラーとなる。
  そして、普通の集合論の記述に少しでも記法を似せるために、次のNotation命令を行う。

Notation "a /e b" := (Element a b) (at level 50).

• Element a b（あるいはa /e b）は、aはbの要素であるという解釈をすると以降が読みやすくなる。
• 念のために言うが、a /e b(つまりElement a b)と記述した場合、aはElementの第2引数であり、bはElementの第3引数である。
  at level 50というのは、a /e b(つまりElement a b)なる記法の結合の力を指定している。 ここで、仮に次のような命令をしたとする。
  
  Parameter E2 : Set -> Set -> Prop.
  Notation "a /e2 b" := (E2 a b) (at level 30).
  
  そこで試しに次のように実行してみると良い。
  Parameter a b c : Set.
  Check (a /e (b /e2 c)).
  Check ((a /e b) /e2 c).
  
  a /e (b /e2 c)の方だけ、括弧が消えてa /e b /e2 cと表示されたと思う。つまり、levelの数が小さい/e2の方が結合力が強いということだと思う。

(* クラスの解釈 *)
Axiom IntCl : forall C:Set -> Prop, forall x:Set, (x /e C) <-> (C x).

(* ----------------------------------------------------------------------- *)

(*Subcl C Dで、C⊆Dを表すことにしよう*)
Definition Subcl (A B:Type) (a:A) (b:B) : Prop :=
 forall x:Set, (Element (A := A) x a) -> (Element (A := B) x b).
Implicit Arguments Subcl [A B].

Notation "C /c= D" := (Subcl C D) (at level 50).

• Subcl C D（あるいはC /c= D）は、CはDの部分クラスであるということを定義しているのである。
• Subclを、Elementを使って定義している。ここで、Subclの定義の中のElement (A := B) x bなる表記について。単にElement x bと表記すると、Elementの第1引数にはCoqが推論して値を入れることになる。それをCoqに推論させずに強制的にBを代入させる記法がElement (A := B) x bなのである。Element (A := B) x bの「:=」の直前がなぜAなのかについては、Elementの定義からきているのである。つまりElement (A := A) x aにおいては、 「:=」の左のAはElementの定義からきているが、右のAはa:Aからきているのである。
  
  以前次のように定義していたことがあった。
  Definition Subcl (A B:Type) (a:A) (b:B) : Prop :=
   forall x:Set, (Element x a) -> (Element x b).
  Implicit Arguments Subcl [A B].

  Notation "C /c= D" := (Subcl C D) (at level 50).
  
  Elementの第1引数はCoqが推論してくれるのだからこれでいいと思っていたら、この定義のせいで原因不明のエラーが出るようになった。仮定にH:C /c= Dがあって、subgoalがC /c= Dのとき、assumptionを実行してもエラーになるのである。さんざん調べた挙句、エラーの原因は次のようであった。このとき、C D : Setであったから、C /c= Dの中のElementの第1引数には当然Setが入っているものだと思っていた。ところが、（どこだったかは忘れたが、）SetではなくTypeが代入されているところがあったのである。そのため、subgoalのC /c= Dが仮定のH:C /c= Dと一致しなかったのである。

(*真部分集合*)
Definition Subcln (A B:Type) (a:A) (b:B) : Prop :=
 (Subcl (A := A) (B := B) a b) /\ ~ (Subcl (A := B) (B := A) b a).
Implicit Arguments Subcln [A B].

Notation "a /cc b" := (Subcln a b) (at level 50).

• Subcln C D（あるいはC /cc D）は、CはDの真部分クラスであるということの定義である。いずれ、CとDは等しくないことが証明される。

Definition Eqcl (A B:Type) (a:A) (b:B) : Prop :=
 (Subcl (A := A) (B := B) a b) /\ (Subcl (A := B) (B := A) b a).
Implicit Arguments Eqcl [A B].

Notation "C /= D" := (Eqcl C D) (at level 50).

• 「/=」は「集合として等しい」という意味の記号である。集合論的にはこれが等しいということの定義であるというべきかも知れない。斜めの線があるので「等しくない」と読み間違わないように。

(* ----------------------------------------------------------------------- *)

(* 公理に直接結びついて定義される関数記号に関しては、公理そのものと、Set_eq
に関しては、関数記号を定義する論理式には含めなくても良いこととしよう。
例えば、公理ExEmpに直接結びついて定義される関数記号がEmpだが、定理Empuniでは
仮定の部分がSet_eqとExEmpのみなので、以下のPrEmpにおいては、それを含めない
こととする。もし含めるなら
Definition PrEmp := Set_eq -> ExEmp -> forall x:Set, ~ (x /e Emp).
という定義になる。
 *)

(* a3Emp01.v Empuniより、空集合を現す定数を定義できる *)
(*空集合を現す定数*)
Parameter Emp : Set.

(*空集合を定数にしてその特徴づけ*)
Definition PrEmp := forall x:Set, ~ (x /e Emp).

• Empは、いかなる集合も要素としない集合である。
• a3Emp01.vの中のEmpuniが証明されるまで、この論理式はないものと思ってよい。
• x /e Empのところを、Element (A := Set) x Empと表記した方がいいのかもしれない。少なくとも今のところ（排中律を証明するところまでは）、エラーはでていない。

(* ----------------------------------------------------------------------- *)

(* a4Pair01.v SPairuniより、対集合を現す関数を定義できる *)
(*対集合を現す関数*)
Parameter SetPair : Set -> Set -> Set.

Notation "{ a , b }" := (SetPair a b) (at level 40).
Notation "{` a }" := (SetPair a a) (at level 40).

(*順序対の記述も定義しておこう*)
(*順序対の記述を< a , b >にしたら、エラーが出たのでやめた*)
Definition SetOrP (a b:Set) : Set := { ({` a }) , ({ a , b }) }.
Notation "[ a , b ]" := (SetOrP a b) (at level 40).

(*対集合の関数記号の公理*)
Definition SPairf :=
 forall a b x:Set, (x /e { a , b }) <-> ((x = a) \/ (x = b)).

• { a , b }は、aとbのみを要素とする集合である。
• a4Pair01.vの中のSPairuniが証明されるまで、この論理式はないものと思ってよい。

(* ----------------------------------------------------------------------- *)

(* a5Sum01.v SSumuniより、和集合を現す関数を定義できる *)
(*和集合を現す関数*)
Parameter SetUnion : Set -> Set.
Notation "/U a" := (SetUnion a) (at level 40).

(*和集合の関数記号の公理*)
Definition SSumf :=
 forall a x:Set, (x /e (/U a)) <-> exists u:Set, ((x /e u) /\ (u /e a)).

• ある集団Aをグループa、グループb、グループcの三つに分けたとしよう。ここで、B:={a,b,c}なる集合を考えるなら、A = /U Bである。
• a5Sum01.vの中のSSumuniが証明されるまで、この論理式はないものと思ってよい。

(*2つのクラスの和クラスを現す関数*)
Definition ClUni2 (A B:Type) (a:A) (b:B):Set -> Prop :=
 fun x:Set => ((x /e a) \/ (x /e b)).
Implicit Arguments ClUni2 [A B].
Notation "a /uu b" := (ClUni2 a b) (at level 40).

• aを動物全体の集まり、bを植物全体の集まりとすると、a /uu bは動植物全体の集まりである。

(*2つの集合の和集合を現す関数*)
Definition SetUni2 (a b:Set):Set := /U ({ a , b }).
Notation "a /u b" := (SetUni2 a b) (at level 40).

• a,bを集合に限定したときのa /uu bが、a /u bになるように定義しているのである。それは後で証明される。

(* ----------------------------------------------------------------------- *)

(*クラスの要素集合の和を現す関数*)
Definition ClUnia (T:Type) (A:T):Set -> Prop :=
 fun x:Set => exists u:Set, ((x /e u) /\ (u /e A)).
Implicit Arguments ClUnia [T].
Notation "/UU A" := (ClUnia A) (at level 40).

• 少し上の/U aでは、aが集合のときしか使えない。上記のように定義すれば、/UU Aは、Aがクラスのときも定義できるし、Aが集合であれば/UU A /= /U Aとなることが、いずれ証明される。

(* ----------------------------------------------------------------------- *)

(* a6Pow01.v SPowuniより、冪集合を現す関数を定義できる *)
(*冪集合を現す関数*)
Parameter SetPower : Set -> Set.
Notation "/P a" := (SetPower a) (at level 40).

(*冪集合の関数記号の公理*)
Definition SPowf :=
 forall a x:Set, (x /e (/P a)) <-> (x /c= a).

• a6Pow01.vの中のSPowuniが証明されるまで、この論理式はないものと思ってよい。

(* ----------------------------------------------------------------------- *)

(* a7Rep01.v SRepuniより、置換公理集合を現す関数を定義できる *)
(*置換公理集合を現す関数*)
Parameter SetRepl : (Set -> Set -> Prop) -> Set -> Set.
Notation "{ P ;; u }" := (SetRepl P u) (at level 40).

(*置換公理集合の関数記号の公理*)
Definition SReplf :=
 forall P:Set -> Set -> Prop,
 (forall x y z:Set, (P x y) -> (P x z) -> y = z) ->
    forall u:Set, forall y:Set,
      (y /e ({ P ;; u })) <-> exists x:Set, ((x /e u) /\ (P x y)).

• 任意のxに対して、P x yが成立するようなyは、存在するとしても1つしかない。（もちろん、存在しない場合もある。）集合uの要素xに対して、P x yが成立するようなyを集めた集合が{ P ;; u }である。
• a7Rep01.vの中のSRepuniが証明されるまで、この論理式はないものと思ってよい。

(* ----------------------------------------------------------------------- *)

(* a7Rep01.v SComuniより、分出集合を現す関数を定義できる *)
(*分出集合を現す関数*)
Parameter SetComp : Set -> (Set -> Prop) -> Set.
Notation "{ a ; P }" := (SetComp a P) (at level 40).

(*分出集合の関数記号の公理*)
Definition SComf :=
 forall P:Set -> Prop, forall a:Set,
  forall y:Set, (y /e ({ a ; P })) <-> ((y /e a) /\ (P y)).

• a7Rep01.vの中のSComuniが証明されるまで、この論理式はないものと思ってよい。

(* ----------------------------------------------------------------------- *)

(* 直積を定義するために *)
(* クラスの直積 *)
Definition Clprod (A B:Type) (a:A) (b:B):Set -> Prop :=
 fun z:Set => exists x:Set, exists y:Set,
  (x /e a) /\ (y /e b) /\ z = ([ x , y ]).
Implicit Arguments Clprod [A B].
Notation "a /xx b" := (Clprod a b) (at level 40).

• aの要素xと、bの要素yから作られる順序対[ x , y ]を全て集めたものがa /xx bである。a,bがいずれも集合のとき、a /xx bも集合になるかどうかは、証明しなければならない事柄である。

(* a7Rep01.v OPuniより、次のpprod u yを定義 *)
Definition pprod (u y:Set) : Set := {(fun x z : Set => z = [x, y]);; u}.

(* a7Rep01.v ppruniより、次のSetprod u vを定義 *)
Definition Setprod (u v:Set) : Set := /U ({fun y w : Set => w = pprod u y;; v}).
Notation "u /x v" := (Setprod u v) (at level 40).

• 集合を作る操作のみでu /x vが作られているので、「u,vがいずれも集合のとき、u /x vも集合になる」ことは自明である。が、今度は「uの要素xと、vの要素yから作られる順序対[ x , y ]を全て集めたものがu /x v」であるかどうかが自明ではない。それは後で証明される。

(* ----------------------------------------------------------------------- *)

(*2つのクラスの共通部分クラスを現す関数*)
Definition CIsec2 (A B:Type) (a:A) (b:B):Set -> Prop :=
 fun x:Set => ((x /e a) /\ (x /e b)).
Implicit Arguments CIsec2 [A B].
Notation "a /aa b" := (CIsec2 a b) (at level 40).

(*2つの集合の共通部分を現す関数*)
Definition SIsec2 (a b:Set):Set := ({ a ; (fun x:Set => (x /e b)) }).
Notation "a /a b" := (SIsec2 a b) (at level 40).

(* ----------------------------------------------------------------------- *)
Definition CDom (A:Type) (u:A):Set -> Prop :=
 fun x:Set => exists y:Set, [ x , y ] /e u.
Implicit Arguments CDom [A].

Definition CRng (A:Type) (u:A):Set -> Prop :=
 fun y:Set => exists x:Set, [ x , y ] /e u.
Implicit Arguments CRng [A].

Definition Dom (u:Set):Set :=
 ({ (/U (/U u)) ; (fun x:Set => exists y:Set, [ x , y ] /e u) }).

Definition Rng (u:Set):Set :=
 ({ (/U (/U u)) ; (fun y:Set => exists x:Set, [ x , y ] /e u) }).

Definition CIv (A:Type) (u:A):Set -> Prop :=
 fun z:Set => exists x:Set, exists y:Set, z = [ x , y ] /\ [ y , x ] /e u.
Implicit Arguments CIv [A].

Definition Iv (u:Set):Set :=
 ({ ((Rng u) /x (Dom u)) ; (fun z:Set => exists x:Set, exists y:Set, z = [ x , y ] /\ [ y , x ] /e u) }).

(* 関係の合成 *)
Definition CRcomp (A B:Type) (S:A) (R:B):Set -> Prop :=
 fun w:Set => exists x:Set, exists z:Set,
 (w = [ x , z ]) /\ exists y:Set, ([ x , y ] /e R) /\ ([ y , z ] /e S).
Implicit Arguments CRcomp [A B].
Notation "S /oo R" := (CRcomp S R) (at level 40, left associativity).

Definition Rcomp (u v:Set):Set :=
 ({ ((Dom v) /x (Rng u)) ; (fun w:Set => exists x:Set, exists z:Set,
 (w = [ x , z ]) /\ exists y:Set, ([ x , y ] /e v) /\ ([ y , z ] /e u)) }).
Notation "u /o v" := (Rcomp u v) (at level 40, left associativity).

(* ----------------------------------------------------------------------- *)
(* すべての集合を含むクラス *)
Definition Vs (x:Set):Prop := x = x.

(*射影を現す関数*)
Parameter pi1 : Set -> Set.
Parameter pi2 : Set -> Set.

(*射影の公理*)
Definition Aproj1 := forall (x y:Set), pi1 ([ x , y ]) = x.
Definition Aproj2 := forall (x y:Set), pi2 ([ x , y ]) = y.
Definition Aproj := Aproj1 /\ Aproj2.

(* ----------------------------------------------------------------------- *)
(*2つのクラスの差クラスを現す関数*)
Definition CDiff (A B:Type) (a:A) (b:B):Set -> Prop :=
 fun x:Set => ((x /e a) /\ ~ (x /e b)).
Implicit Arguments CDiff [A B].
Notation "a /-- b" := (CDiff a b) (at level 40).
Notation "/~ a" := (CDiff Vs a) (at level 40).

(*2つの集合の差集合を現す関数*)
Definition SDiff (a b:Set):Set := ({ a ; (fun x:Set => ~ (x /e b)) }).
Notation "a /- b" := (SDiff a b) (at level 40).

(* ----------------------------------------------------------------------- *)
(* クラス関数を定義する前 *)
Definition pFun (T:Type) (F:T) : Prop :=
 forall x y z:Set, ([ x , y ] /e F) -> ([ x , z ] /e F) -> y = z.
Implicit Arguments pFun [T].

(* クラス関数を定義する *)
Definition Func (T:Type) (F:T) : Prop :=
 (F /c= (Vs /xx Vs)) /\ (pFun (T := T) F).
Implicit Arguments Func [T].

(*関数の適用を現す関数*)
Parameter App : forall A:Type, A -> Set -> Set.
Implicit Arguments App [A].

Notation "F ` x" := (App F x) (at level 50).

(*関数の適用の公理*)
Definition AppFunc := forall (T:Type)(F:T)(x:Set),
 (exists! y:Set, [ x , y ] /e F) -> ([ x , (F ` x) ] /e F).

(* ----------------------------------------------------------------------- *)

Definition CFmake (T:Type) (P:Set -> Set) (A:T):Set -> Prop :=
 fun w:Set => exists x:Set, (x /e A) /\ (w = [ x , (P x) ]).
Implicit Arguments CFmake [T].
Notation "P /ff A" := (CFmake P A) (at level 40).

Definition Fmake (P:Set -> Set) (a:Set) : Set :=
  { (fun x w:Set => (w = [ x , (P x) ])) ;; a }.
Notation "P /f a" := (Fmake P a) (at level 40).

(* ----------------------------------------------------------------------- *)
(* 関数の定義域の制限 *)
Definition CFrest (S T:Type) (F:S) (A:T):Set -> Prop :=
 fun z:Set => exists x:Set, exists y:Set,
   z = ([ x , y ]) /\ (x /e A) /\ (z /e F).
Implicit Arguments CFrest [S T].
Notation "F /|| A" := (CFrest F A) (at level 40).

Definition Frest (f:Set) (a:Set) : Set := f /a (a /x (Rng f)).
Notation "f /| a" := (Frest f a) (at level 40).

(* ----------------------------------------------------------------------- *)
(* 関数の像 *)
Definition CFimage (S T:Type) (F:S) (B:T):Set -> Prop :=
 CRng (F /|| B).
Implicit Arguments CFimage [S T].
Notation "F /`` B" := (CFimage F B) (at level 40).

Definition Fimage (f:Set) (a:Set) : Set := Rng (f /| a).
Notation "f `` a" := (Fimage f a) (at level 40).

(* ----------------------------------------------------------------------- *)
(* {f(x)|(x /e A) /\ (P x)}のイメージ *)
Definition CtermP (S T:Type) (f:Set -> S) (A:T) (P:Set -> Prop):Set -> Prop :=
  fun z:Set => exists x:Set, (z /= (f x)) /\ (x /e A) /\ (P x).
Implicit Arguments CtermP [S T].
Notation "{ f ;; A ;; P }" := (CtermP f A P) (at level 40).

(* {f(x)|(x /e a) /\ (P x)}のイメージ *)
Definition StermP (T:Type) (f:Set -> T) (a:Set) (P:Set -> Prop):Set :=
  { (fun x z:Set => (z /= (f x)) /\ (P x)) ;; a }.
Implicit Arguments StermP [T].
Notation "{ f ; a ; P }" := (StermP f a P) (at level 40).

(* ----------------------------------------------------------------------- *)

(* 域付クラス関数表示を定義する *)
Definition Fundr (S T U:Type)(F:S)(A:T)(B:U) : Prop :=
 (Func (T := S) F) /\ (CDom (A := S) F /= A) /\ (CRng (A := S) F /c= B).
Implicit Arguments Fundr [S T U].

Notation "F /: A /> B" := (Fundr F A B) (at level 50).

(* 単射クラス関数表示を定義する *)
Definition Rel11 (T:Type)(F:T) : Prop :=
 forall x y z:Set, ([ x , z ] /e F) -> ([ y , z ] /e F) -> x = y.
Implicit Arguments Rel11 [T].

Definition Fun11 (T:Type)(F:T) : Prop :=
 (Func (T := T) F) /\ (Rel11 (T := T) F).
Implicit Arguments Fun11 [T].

Definition Funmn (S T U:Type)(F:S)(A:T)(B:U) : Prop :=
 (Func (T := S) F) /\ (Rel11 (T := S) F) /\ (CDom (A := S) F /= A) /\ (CRng (A := S) F /c= B).
Implicit Arguments Funmn [S T U].

Notation "F /: A /11> B" := (Funmn F A B) (at level 50).

Definition Funon (S T U:Type)(F:S)(A:T)(B:U) : Prop :=
 (Func (T := S) F) /\ (CDom (A := S) F /= A) /\ (CRng (A := S) F /= B).
Implicit Arguments Funon [S T U].

Notation "F /: A /on> B" := (Funon F A B) (at level 50).

Definition Funiso (S T U:Type)(F:S)(A:T)(B:U) : Prop :=
 (Func (T := S) F) /\ (Rel11 (T := S) F) /\ (CDom (A := S) F /= A) /\ (CRng (A := S) F /= B).
Implicit Arguments Funiso [S T U].

Notation "F /: A /=> B" := (Funiso F A B) (at level 50).

(* ----------------------------------------------------------------------- *)

もどる