Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison OD.agda @ 309:d4802179a66f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Jun 2020 00:17:05 +0900
parents b172ab9f12bc
children 73a2a8ec9603
comparison
equal deleted inserted replaced
308:b172ab9f12bc 309:d4802179a66f
55 -- next assumptions are our axiom 55 -- next assumptions are our axiom
56 -- In classical Set Theory, HOD is used, as a subset of OD, 56 -- In classical Set Theory, HOD is used, as a subset of OD,
57 -- HOD = { x | TC x ⊆ OD } 57 -- HOD = { x | TC x ⊆ OD }
58 -- 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.
59 -- This is not possible because we don't have V yet. 59 -- This is not possible because we don't have V yet.
60 -- We simply assume V=OD here.
61 -- 60 --
62 -- We also assumes ODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks. 61 -- We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
63 -- ODs have an ovbious maximum, but Ordinals are not. This means, od→ord is not an on-to mapping. 62 -- ODs have an ovbious maximum, but Ordinals are not. So HOD cannot be a maximum OD.
64 --
65 -- ==→o≡ is necessary to prove axiom of extensionality.
66 -- 63 --
67 -- In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic, 64 -- In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic,
68 -- we need explict assumption on sup. 65 -- we need explict assumption on sup.
66 -- In order to allow sup on od→ord HOD, solutions of a HOD have to have a maximu.
67 --
68 -- ==→o≡ is necessary to prove axiom of extensionality.
69 69
70 data One : Set n where 70 data One : Set n where
71 OneObj : One 71 OneObj : One
72 72
73 -- Ordinals in OD , the maximum 73 -- Ordinals in OD , the maximum
77 record HOD : Set (suc n) where 77 record HOD : Set (suc n) where
78 field 78 field
79 od : OD 79 od : OD
80 odmax : Ordinal 80 odmax : Ordinal
81 <odmax : {y : Ordinal} → def od y → y o< odmax 81 <odmax : {y : Ordinal} → def od y → y o< odmax
82
83 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
84 field
85 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
86 os← : Ordinal → Ordinal
87 os←limit : (x : Ordinal) → os← x o< maxordinal
88 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x
89 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x
90 82
91 open HOD 83 open HOD
92 84
93 record ODAxiom : Set (suc n) where 85 record ODAxiom : Set (suc n) where
94 field 86 field
97 ord→od : Ordinal → HOD 89 ord→od : Ordinal → HOD
98 c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y 90 c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y
99 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x 91 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x
100 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 92 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
101 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y 93 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y
102 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum )
103 sup-o : (A : HOD) → (( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal 94 sup-o : (A : HOD) → (( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal
104 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ 95 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ
105 96
106 postulate odAxiom : ODAxiom 97 postulate odAxiom : ODAxiom
107 open ODAxiom odAxiom 98 open ODAxiom odAxiom
280 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD 271 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD
281 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } 272 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
282 Replace : HOD → (HOD → HOD ) → HOD 273 Replace : HOD → (HOD → HOD ) → HOD
283 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X {!!} ) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x)) 274 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X {!!} ) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
284 _∩_ : ( A B : ZFSet ) → ZFSet 275 _∩_ : ( A B : ZFSet ) → ZFSet
285 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = {!!} ; <odmax = {!!} } 276 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
286 Union : HOD → HOD 277 Union : HOD → HOD
287 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; odmax = {!!} ; <odmax = {!!} } 278 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; odmax = {!!} ; <odmax = {!!} }
288 _∈_ : ( A B : ZFSet ) → Set n 279 _∈_ : ( A B : ZFSet ) → Set n
289 A ∈ B = B ∋ A 280 A ∈ B = B ∋ A
290 Power : HOD → HOD 281 Power : HOD → HOD