Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 322:a9d380378efd
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 03 Jul 2020 22:54:45 +0900 |
| parents | a81824502ebd |
| children | e228e96965f0 |
comparison
equal
deleted
inserted
replaced
| 321:a81824502ebd | 322:a9d380378efd |
|---|---|
| 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 -- next assumptions are our axiom | 55 -- next assumptions are our axiom |
| 56 -- | |
| 57 -- OD is an equation on Ordinals, so it contains Ordinals. If these Ordinals have one-to-one | |
| 58 -- correspondence to the OD then the OD looks like a ZF Set. | |
| 59 -- | |
| 60 -- If all ZF Set have supreme upper bound, the solutions of OD have to be bounded, i.e. | |
| 61 -- bbounded ODs are ZF Set. Unbounded ODs are classes. | |
| 62 -- | |
| 56 -- In classical Set Theory, HOD is used, as a subset of OD, | 63 -- In classical Set Theory, HOD is used, as a subset of OD, |
| 57 -- HOD = { x | TC x ⊆ OD } | 64 -- 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. | 65 -- 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. | 66 -- This is not possible because we don't have V yet. So we assumes HODs are bounded OD. |
| 60 -- | 67 -- |
| 61 -- We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks. | 68 -- We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks. |
| 62 -- ODs have an ovbious maximum, but Ordinals are not. So HOD cannot be a maximum OD. | 69 -- There two contraints on the HOD order, one is ∋, the other one is ⊂. |
| 70 -- ODs have an ovbious maximum, but Ordinals are not, but HOD has no maximum because there is an aribtrary | |
| 71 -- bound on each HOD. | |
| 63 -- | 72 -- |
| 64 -- In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic, | 73 -- In classical Set Theory, sup is defined by Uion, since we are working on constructive logic, |
| 65 -- we need explict assumption on sup. | 74 -- 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 -- | 75 -- |
| 68 -- ==→o≡ is necessary to prove axiom of extensionality. | 76 -- ==→o≡ is necessary to prove axiom of extensionality. |
| 69 | 77 |
| 70 data One : Set n where | 78 data One : Set n where |
| 71 OneObj : One | 79 OneObj : One |
| 88 od→ord : HOD → Ordinal | 96 od→ord : HOD → Ordinal |
| 89 ord→od : Ordinal → HOD | 97 ord→od : Ordinal → HOD |
| 90 c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y | 98 c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y |
| 91 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) | 99 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) |
| 92 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x | 100 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x |
| 93 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | 101 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x |
| 94 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y | 102 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y |
| 95 sup-o : (A : HOD) → (( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal | 103 sup-o : (A : HOD) → (( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal |
| 96 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 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ |
| 97 | 105 |
| 98 postulate odAxiom : ODAxiom | 106 postulate odAxiom : ODAxiom |
| 99 open ODAxiom odAxiom | 107 open ODAxiom odAxiom |
| 311 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where | 319 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where |
| 312 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ | 320 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ |
| 313 lemma {o∅} iφ = proj1 next-limit | 321 lemma {o∅} iφ = proj1 next-limit |
| 314 lemma (isuc {x} i) = lemma1 where -- proj2 next-limit ? ( lemma i ) | 322 lemma (isuc {x} i) = lemma1 where -- proj2 next-limit ? ( lemma i ) |
| 315 lemma1 : od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅ | 323 lemma1 : od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅ |
| 316 lemma1 = ? | 324 lemma1 = {!!} |
| 317 | 325 |
| 318 | 326 |
| 319 | 327 |
| 320 _=h=_ : (x y : HOD) → Set n | 328 _=h=_ : (x y : HOD) → Set n |
| 321 x =h= y = od x == od y | 329 x =h= y = od x == od y |