# HG changeset patch
# User Shinji KONO
# Date 1594023286 32400
# Node ID 231deb255e74be53e62098494612d0dd78425ce1
# Parent daafa2213dd2dd8096f29a9b8ab395015865c058
...
diff r daafa2213dd2 r 231deb255e74 zfinagda.ind
 a/zfinagda.ind Mon Jul 06 11:09:40 2020 +0900
+++ b/zfinagda.ind Mon Jul 06 17:14:46 2020 +0900
@@ 54,7 +54,10 @@
I'm planning to do it in my old age, but I'm enough age now.
This is done during from May to September.
+if you familier with Agda, you can skip to
+
+there
+
Agda and Intuitionistic Logic
@@ 262,7 +265,8 @@
postulate can be constructive.
postulate can be inconsistent, which result everything has a proof.
+postulate can be inconsistent, which result everything has a proof. Actualy this assumption
+doesnot work for Ordinals, we discuss this later.
 A ∨ B
@@ 403,6 +407,7 @@
Classical story of ZF Set Theory
+
Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads
a relative consistency proof of the Set Theory.
Ordinal number is used in the flow.
@@ 453,7 +458,7 @@
→ ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
→ ∀ (x : ord) → ψ x
Concrete Ordinals
+Concrete Ordinals or Countable Ordinals
We can define a list like structure with level, which is a kind of two dimensional infinite array.
@@ 525,6 +530,9 @@
But in our case, we have no ZF theory, so we are going to use Ordinals.
+The idea is to use an ordinal as a pointer to a record which defines a Set.
+If the recored defines a series of Ordinals which is a pointer to the Set.
+This record looks like a Set.
Ordinal Definable Set
@@ 540,76 +548,93 @@
Ordinals itself is not a set in a ZF Set theory but a class. In OD,
 record { def = λ x → true }
+ data One : Set n where
+ OneObj : One
means Ordinals itself, so ODs are larger than a notion of ZF Set Theory,
but we don't care about it.
+ record { def = λ x → One }
+
+means it accepets all Ordinals, i.e. this is Ordinals itself, so ODs are larger than ZF Set.
+You can say OD is a class in ZF Set Theory term.
∋ in OD
+OD is not ZF Set
+
+If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like
+a Set. The idea is to use an ordinal as a pointer to OD.
+Unfortunately this scheme does not work well. As we saw OD includes all Ordinals,
+which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like
OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping
+ ¬ODorder : ( od→ord : OD → Ordinal )
+ → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥
+ ¬ODorder od→ord ord→od c<→o< = ?
+
+Actualy we can prove this contrdction, so we need some restrctions on OD.
+
+This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself.
+
+ HOD : Hereditarily Ordinal Definable
+
+What we need is a bounded OD, the containment is limited by an ordinal.
 od→ord : OD → Ordinal
+ record HOD : Set (suc n) where
+ field
+ od : OD
+ odmax : Ordinal
+
Order preserving in the mapping of OD and Ordinal
Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ).
+Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ).
 def y ( od→ord x )

An elements of OD should be defined before the OD, that is, an ordinal corresponding an elements
have to be smaller than the corresponding ordinal of the containing OD.
+ def (od y) ( od→ord x )
 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
+An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements
+have to be smaller than the corresponding ordinal of the containing OD.
+We also assumes subset is always smaller. This is necessary to make a limit of Power Set.
This is also said to be provable in classical Set Theory, but we simply assumes it.
+ 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)
OD has an order based on the corresponding ordinal, but it may not have corresponding def / ∋
relation. This means the reverse order preservation,
+If wa assumes reverse order preservation,
o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x
is not valid. If we assumes it, ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in
the model.
+∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model.
ISO

It also requires isomorphisms,

 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x


Various Sets
In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
@@ 617,6 +642,7 @@
Ordinal / things satisfies axiom of Ordinal / extension of natural number
V / hierarchical construction of Set from φ
L / hierarchical predicate definable construction of Set from φ
+ HOD / Hereditarily Ordinal Definable
OD / equational formula on Ordinals
Agda Set / Type / it also has a level
@@ 682,8 +708,10 @@
OD is an equation on Ordinals, we can simply write axiom of pair in the OD.
 _,_ : OD → OD → OD
 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) }
+ _,_ : HOD → HOD → HOD
+ x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = ? ;