### changeset 322:a9d380378efd

...
author Shinji KONO Fri, 03 Jul 2020 22:54:45 +0900 a81824502ebd e228e96965f0 OD.agda 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 = {!!}

```