comparison OD.agda @ 277:d9d3654baee1

seperate choice from LEM
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 May 2020 09:38:21 +0900
parents 6f10c47e4e7a
children 5de8905a5a2b 359402cc6c3d
comparison
equal deleted inserted replaced
276:6f10c47e4e7a 277:d9d3654baee1
50 50
51 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y 51 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y
52 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m 52 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m
53 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m 53 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m
54 54
55 -- Ordinal in OD ( and ZFSet ) Transitive Set
56 Ord : ( a : Ordinal ) → OD
57 Ord a = record { def = λ y → y o< a }
58
59 od∅ : OD
60 od∅ = Ord o∅
61
62 -- next assumptions are our axiom 55 -- next assumptions are our axiom
63 -- it defines a subset of OD, which is called HOD, usually defined as 56 -- it defines a subset of OD, which is called HOD, usually defined as
64 -- HOD = { x | TC x ⊆ OD } 57 -- HOD = { x | TC x ⊆ OD }
65 -- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x 58 -- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x
66 59
67 postulate 60 record ODAxiom : Set (suc n) where
68 -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) 61 -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
62 field
69 od→ord : OD → Ordinal 63 od→ord : OD → Ordinal
70 ord→od : Ordinal → OD 64 ord→od : Ordinal → OD
71 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y 65 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
72 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x 66 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
73 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 67 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
74 ==→o≡ : { x y : OD } → (x == y) → x ≡ y 68 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
75 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD
76 -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x
77 -- ord→od x ≡ Ord x results the same
78 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum ) 69 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum )
79 sup-o : ( OD → Ordinal ) → Ordinal 70 sup-o : ( OD → Ordinal ) → Ordinal
80 sup-o< : { ψ : OD → Ordinal } → ∀ {x : OD } → ψ x o< sup-o ψ 71 sup-o< : { ψ : OD → Ordinal } → ∀ {x : OD } → ψ x o< sup-o ψ
81 -- contra-position of mimimulity of supermum required in Power Set Axiom 72 -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use
82 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal 73 -- sup-x : {n : Level } → ( OD → Ordinal ) → Ordinal
83 -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) 74 -- sup-lb : {n : Level } → { ψ : OD → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
75
76 postulate odAxiom : ODAxiom
77 open ODAxiom odAxiom
84 78
85 data One : Set n where 79 data One : Set n where
86 OneObj : One 80 OneObj : One
87 81
82 -- Ordinals in OD , the maximum
88 Ords : OD 83 Ords : OD
89 Ords = record { def = λ x → One } 84 Ords = record { def = λ x → One }
90 85
91 maxod : {x : OD} → od→ord x o< od→ord Ords 86 maxod : {x : OD} → od→ord x o< od→ord Ords
92 maxod {x} = c<→o< OneObj 87 maxod {x} = c<→o< OneObj
88
89 -- Ordinal in OD ( and ZFSet ) Transitive Set
90 Ord : ( a : Ordinal ) → OD
91 Ord a = record { def = λ y → y o< a }
92
93 od∅ : OD
94 od∅ = Ord o∅
95
93 96
94 o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y) x ) → {x : OD } → x ≡ Ord (od→ord x) 97 o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y) x ) → {x : OD } → x ≡ Ord (od→ord x)
95 o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where 98 o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
96 lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y 99 lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y
97 lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → def x k ) (sym diso) lt)) 100 lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → def x k ) (sym diso) lt))
254 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } 257 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
255 _∈_ : ( A B : ZFSet ) → Set n 258 _∈_ : ( A B : ZFSet ) → Set n
256 A ∈ B = B ∋ A 259 A ∈ B = B ∋ A
257 Power : OD → OD 260 Power : OD → OD
258 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) 261 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
259 {_} : ZFSet → ZFSet 262 -- {_} : ZFSet → ZFSet
260 { x } = ( x , x ) 263 -- { x } = ( x , x )
261 264
262 data infinite-d : ( x : Ordinal ) → Set n where 265 data infinite-d : ( x : Ordinal ) → Set n where
263 iφ : infinite-d o∅ 266 iφ : infinite-d o∅
264 isuc : {x : Ordinal } → infinite-d x → 267 isuc : {x : Ordinal } → infinite-d x →
265 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 268 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))