# HG changeset patch
# User Shinji KONO
# Date 1593784485 -32400
# Node ID a9d380378efdc94eaf50fdf0cbe90fa8720393b7
# Parent a81824502ebdacd3a3e647d50c0dbfa47c700f8c
...
diff -r a81824502ebd -r a9d380378efd OD.agda
--- 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 = {!!}