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

comparison src/OD.agda @ 1097:40345abc0949

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add README
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 24 Dec 2022 11:39:30 +0900
parents 55ab5de1ae02
children f46a16cebbab
comparison
equal deleted inserted replaced
1096:55ab5de1ae02 1097:40345abc0949
97 c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y 97 c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y
98 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) 98 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
99 *iso : {x : HOD } → * ( & x ) ≡ x 99 *iso : {x : HOD } → * ( & x ) ≡ x
100 &iso : {x : Ordinal } → & ( * x ) ≡ x 100 &iso : {x : Ordinal } → & ( * x ) ≡ x
101 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y 101 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y
102 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal 102 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal -- required in Replace
103 sup-o≤ : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤ sup-o A ψ 103 sup-o≤ : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤ sup-o A ψ
104 -- possible order restriction 104 -- possible order restriction (required in the axiom of infinite )
105 ho< : {x : HOD} → & x o< next (odmax x) 105 ho< : {x : HOD} → & x o< next (odmax x)
106 106
107 107
108 postulate odAxiom : ODAxiom 108 postulate odAxiom : ODAxiom
109 open ODAxiom odAxiom 109 open ODAxiom odAxiom
400 -- We simply assumes infinite-d y has a maximum. 400 -- We simply assumes infinite-d y has a maximum.
401 -- 401 --
402 -- This means that many of OD may not be HODs because of the & mapping divergence. 402 -- This means that many of OD may not be HODs because of the & mapping divergence.
403 -- We should have some axioms to prevent this such as & x o< next (odmax x). 403 -- We should have some axioms to prevent this such as & x o< next (odmax x).
404 -- 404 --
405 -- postulate 405 -- Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho<
406 -- ωmax : Ordinal
407 -- <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
408 --
409 -- infinite : HOD
410 -- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax }
411 406
412 infinite : HOD 407 infinite : HOD
413 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where 408 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
414 u : (y : Ordinal ) → HOD 409 u : (y : Ordinal ) → HOD
415 u y = Union (* y , (* y , * y)) 410 u y = Union (* y , (* y , * y))