### changeset 415:3dda56a5befd

...
author Shinji KONO Thu, 30 Jul 2020 17:22:34 +0900 aa306f5dab9b b737a2e0b46e VL.agda 1 files changed, 37 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/VL.agda	Thu Jul 30 16:06:36 2020 +0900
+++ b/VL.agda	Thu Jul 30 17:22:34 2020 +0900
@@ -25,19 +25,48 @@
open HOD

-- The cumulative hierarchy
---    V 0 := ∅ .
---    V β + 1 := P ( V β ) .
---    V λ := ⋃ β < λ V β .
+--    V 0 := ∅
+--    V α + 1 := P ( V α )
+--    V α := ⋃ { V β | β < α }

-{-# TERMINATING #-}
V : ( β : Ordinal ) → HOD
V β = TransFinite1  Vβ₁ β where
Vβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
Vβ₁ x Vβ₀ with trio< x o∅
Vβ₁ x Vβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
-   Vβ₁ x Vβ₀ | tri≈ ¬a refl ¬c = od∅
+   Vβ₁ x Vβ₀ | tri≈ ¬a refl ¬c = Ord o∅
Vβ₁ x Vβ₀ | tri> ¬a ¬b c with Oprev-p  x
Vβ₁ x Vβ₀ | tri> ¬a ¬b c | yes p = Power ( Vβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
-   Vβ₁ x Vβ₀ | tri> ¬a ¬b c | no ¬p = Vβ<α x where
-      Vβ<α : (α : Ordinal ) → HOD
-      Vβ<α α = record { od = record { def = λ x → (x o< α ) ∧ odef (V x) x  } ; odmax = α; <odmax = λ {x} lt → proj1 lt }
+   Vβ₁ x Vβ₀ | tri> ¬a ¬b c | no ¬p =
+        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (Vβ₀ y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
+
+--
+-- Definition for Power Set
+--
+record Definitions  : Set (suc n) where
+   field
+      Definition : HOD → HOD
+
+open Definitions
+
+Df : Definitions → (x : HOD) → HOD
+Df D x = Power x ∩ Definition D x
+
+-- The constructible Sets
+--    L 0 := ∅
+--    L α + 1 := Df (L α)   -- Definable Power Set
+--    V α := ⋃ { L β | β < α }
+
+L : ( β : Ordinal ) → Definitions → HOD
+L β D = TransFinite1  Lβ₁ β where
+   Lβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
+   Lβ₁ x Lβ₀ with trio< x o∅
+   Lβ₁ x Lβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
+   Lβ₁ x Lβ₀ | tri≈ ¬a refl ¬c = Ord o∅
+   Lβ₁ x Lβ₀ | tri> ¬a ¬b c with Oprev-p  x
+   Lβ₁ x Lβ₀ | tri> ¬a ¬b c | yes p = Df D ( Lβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
+   Lβ₁ x Lβ₀ | tri> ¬a ¬b c | no ¬p =
+        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (Lβ₀ y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
+
+V=L0 : Set (suc n)
+V=L0 = (x : Ordinal) → V x ≡  L x record { Definition = λ y → y }