# HG changeset patch # User Shinji KONO # Date 1594023286 -32400 # Node ID 231deb255e74be53e62098494612d0dd78425ce1 # Parent daafa2213dd2dd8096f29a9b8ab395015865c058 ... diff -r daafa2213dd2 -r 231deb255e74 zf-in-agda.ind --- a/zf-in-agda.ind Mon Jul 06 11:09:40 2020 +0900 +++ b/zf-in-agda.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 + ¬OD-order : ( od→ord : OD → Ordinal ) + → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥ + ¬OD-order 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 = ? ;