Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 322:a9d380378efd
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 03 Jul 2020 22:54:45 +0900 |
parents | a81824502ebd |
children | e228e96965f0 |
files | OD.agda |
diffstat | 1 files changed, 15 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Fri Jul 03 22:22:59 2020 +0900 +++ b/OD.agda Fri Jul 03 22:54:45 2020 +0900 @@ -53,17 +53,25 @@ eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m -- next assumptions are our axiom +-- +-- OD is an equation on Ordinals, so it contains Ordinals. If these Ordinals have one-to-one +-- correspondence to the OD then the OD looks like a ZF Set. +-- +-- If all ZF Set have supreme upper bound, the solutions of OD have to be bounded, i.e. +-- bbounded ODs are ZF Set. Unbounded ODs are classes. +-- -- In classical Set Theory, HOD is used, as a subset of OD, -- HOD = { x | TC x ⊆ OD } -- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x. --- This is not possible because we don't have V yet. +-- This is not possible because we don't have V yet. So we assumes HODs are bounded OD. -- -- We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks. --- ODs have an ovbious maximum, but Ordinals are not. So HOD cannot be a maximum OD. +-- There two contraints on the HOD order, one is ∋, the other one is ⊂. +-- ODs have an ovbious maximum, but Ordinals are not, but HOD has no maximum because there is an aribtrary +-- bound on each HOD. -- --- In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic, +-- In classical Set Theory, sup is defined by Uion, since we are working on constructive logic, -- we need explict assumption on sup. --- In order to allow sup on od→ord HOD, solutions of a HOD have to have a maximu. -- -- ==→o≡ is necessary to prove axiom of extensionality. @@ -90,8 +98,8 @@ c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x - diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x - ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y sup-o : (A : HOD) → (( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ @@ -313,7 +321,7 @@ lemma {o∅} iφ = proj1 next-limit lemma (isuc {x} i) = lemma1 where -- proj2 next-limit ? ( lemma i ) lemma1 : od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅ - lemma1 = ? + lemma1 = {!!}