annotate zf.agda @ 78:9a7a64b2388c

infinite and replacement begin no Russel Pradox
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jun 2019 10:19:52 +0900
parents 75ba8cf64707
children c8b79d303867
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module zf where
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
5 data Bool : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
6 true : Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
7 false : Bool
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 field
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 proj1 : A
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 proj2 : B
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 case1 : A → A ∨ B
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 case2 : B → A ∨ B
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 _⇔_ : {n : Level } → ( A B : Set n ) → Set n
77
75ba8cf64707 Power Set on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
19 _⇔_ A B = ( A → B ) ∧ ( B → A )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
21 open import Relation.Nullary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
22 open import Relation.Binary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
23
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 infixr 130 _∧_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 infixr 140 _∨_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 infixr 150 _⇔_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
28 record IsZF {n m : Level }
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
29 (ZFSet : Set n)
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
30 (_∋_ : ( A x : ZFSet ) → Set m)
9
5ed16e2d8eb7 try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
31 (_≈_ : Rel ZFSet m)
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
32 (∅ : ZFSet)
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
33 (_,_ : ( A B : ZFSet ) → ZFSet)
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
34 (Union : ( A : ZFSet ) → ZFSet)
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
35 (Power : ( A : ZFSet ) → ZFSet)
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
36 (Select : ZFSet → ( ZFSet → Set m ) → ZFSet )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
37 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
38 (infinite : ZFSet)
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
39 : Set (suc (n ⊔ m)) where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 field
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
41 isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
43 pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B )
69
93abc0133b8a union continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
44 -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
70
cd9cf8b09610 Union needs +1 space
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
45 union-u : ( X z : ZFSet ) → Union X ∋ z → ZFSet
73
dd430a95610f fix ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
46 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
72
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
47 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 _∈_ : ( A B : ZFSet ) → Set m
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 A ∈ B = B ∋ A
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
50 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
51 _⊆_ A B {x} = A ∋ x → B ∋ x
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 _∩_ : ( A B : ZFSet ) → ZFSet
51
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
53 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 _∪_ : ( A B : ZFSet ) → ZFSet
51
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
55 A ∪ B = Union (A , B)
78
9a7a64b2388c infinite and replacement begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
56 {_} : ZFSet → ZFSet
9a7a64b2388c infinite and replacement begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
57 { x } = ( x , x )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 infixr 200 _∈_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 infixr 230 _∩_ _∪_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 infixr 220 _⊆_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 field
4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
62 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
64 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → _⊆_ t A {x}
77
75ba8cf64707 Power Set on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
65 power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t
65
164ad5a703d8 ¬∅=→∅∈ : {n : Level} → { x : OD {suc n} } → ¬ ( x == od∅ {suc n} ) → x ∋ od∅ {suc n}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
66 -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
76
8e8f54e7a030 extensionality done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
67 extensionality : { A B : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
37
f10ceee99d00 ¬ ( y c< x ) → x ≡ od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
69 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
f10ceee99d00 ¬ ( y c< x ) → x ≡ od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
70 regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 infinity∅ : ∅ ∈ infinite
78
9a7a64b2388c infinite and replacement begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
73 infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ { x }) ∈ infinite
54
33fb8228ace9 fix selection axiom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
74 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
76 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( ψ x ∈ Replace X ψ )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
78 record ZF {n m : Level } : Set (suc (n ⊔ m)) where
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
79 infixr 210 _,_
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
80 infixl 200 _∋_
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
81 infixr 220 _≈_
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
82 field
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
83 ZFSet : Set n
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
84 _∋_ : ( A x : ZFSet ) → Set m
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
85 _≈_ : ( A B : ZFSet ) → Set m
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
86 -- ZF Set constructor
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
87 ∅ : ZFSet
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
88 _,_ : ( A B : ZFSet ) → ZFSet
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
89 Union : ( A : ZFSet ) → ZFSet
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
90 Power : ( A : ZFSet ) → ZFSet
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
91 Select : ZFSet → ( ZFSet → Set m ) → ZFSet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
92 Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
93 infinite : ZFSet
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
94 isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
95