open import Level
module OD where
open import zf
open import ordinal
open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Core
open import logic
open import nat
-- Ordinal Definable Set
record OD {n : Level} : Set (suc n) where
field
def : (x : Ordinal {n} ) → Set n
open OD
open Ordinal
open _∧_
open _∨_
open Bool
record _==_ {n : Level} ( a b : OD {n} ) : Set n where
field
eq→ : ∀ { x : Ordinal {n} } → def a x → def b x
eq← : ∀ { x : Ordinal {n} } → def b x → def a x
id : {n : Level} {A : Set n} → A → A
id x = x
eq-refl : {n : Level} { x : OD {n} } → x == x
eq-refl {n} {x} = record { eq→ = id ; eq← = id }
open _==_
eq-sym : {n : Level} { x y : OD {n} } → x == y → y == x
eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq }
eq-trans : {n : Level} { x y z : OD {n} } → x == y → y == z → x == z
eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) }
⇔→== : {n : Level} { x y : OD {suc n} } → ( {z : Ordinal {suc n}} → def x z ⇔ def y z) → x == y
eq→ ( ⇔→== {n} {x} {y} eq ) {z} m = proj1 eq m
eq← ( ⇔→== {n} {x} {y} eq ) {z} m = proj2 eq m
-- Ordinal in OD ( and ZFSet ) Transitive Set
Ord : { n : Level } → ( a : Ordinal {n} ) → OD {n}
Ord {n} a = record { def = λ y → y o< a }
od∅ : {n : Level} → OD {n}
od∅ {n} = Ord o∅
postulate
-- OD can be iso to a subset of Ordinal ( by means of Godel Set )
od→ord : {n : Level} → OD {n} → Ordinal {n}
ord→od : {n : Level} → Ordinal {n} → OD {n}
c<→o< : {n : Level} {x y : OD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y
oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
-- we should prove this in agda, but simply put here
==→o≡ : {n : Level} → { x y : OD {suc n} } → (x == y) → x ≡ y
-- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
-- o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x
-- ord→od x ≡ Ord x results the same
-- supermum as Replacement Axiom
sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ
-- contra-position of mimimulity of supermum required in Power Set Axiom
-- sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
-- sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
-- mimimul and x∋minimul is an Axiom of choice
minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n}
-- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
-- minimulity (may proved by ε-induction )
minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) )
_∋_ : { n : Level } → ( a x : OD {n} ) → Set n
_∋_ {n} a x = def a ( od→ord x )
_c<_ : { n : Level } → ( x a : OD {n} ) → Set n
x c< a = a ∋ x
_c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n)
a c≤ b = (a ≡ b) ∨ ( b ∋ a )
cseq : {n : Level} → OD {n} → OD {n}
cseq x = record { def = λ y → def x (osuc y) } where
def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x
def-subst df refl refl = df
sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n}
sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → def ( sup-od ψ ) (od→ord ( ψ x ))
sup-c< {n} ψ {x} = def-subst {n} {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) )
otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y
otrans x ¬a ¬b c = yes c
-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
in-codomain : {n : Level} → (X : OD {suc n} ) → ( ψ : OD {suc n} → OD {suc n} ) → OD {suc n}
in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
-- Power Set of X ( or constructible by λ y → def X (od→ord y )
ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n}
ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set
Def : {n : Level} → (A : OD {suc n}) → OD {suc n}
Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
_⊆_ : {n : Level} ( A B : OD {suc n} ) → ∀{ x : OD {suc n} } → Set (suc n)
_⊆_ A B {x} = A ∋ x → B ∋ x
infixr 220 _⊆_
subset-lemma : {n : Level} → {A x y : OD {suc n} } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} )
subset-lemma {n} {A} {x} {y} = record {
proj1 = λ z lt → proj1 (z lt)
; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
}
-- Constructible Set on α
-- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x }
-- L (Φ 0) = Φ
-- L (OSuc lv n) = { Def ( L n ) }
-- L (Φ (Suc n)) = Union (L α) (α < Φ (Suc n) )
L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n}
L {n} record { lv = Zero ; ord = (Φ .0) } = od∅
L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) )
L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
cseq ( Ord (od→ord (L {n} (record { lv = lx ; ord = Φ lx }))))
-- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α
-- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x
OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
OD→ZF {n} = record {
ZFSet = OD {suc n}
; _∋_ = _∋_
; _≈_ = _==_
; ∅ = od∅
; _,_ = _,_
; Union = Union
; Power = Power
; Select = Select
; Replace = Replace
; infinite = infinite
; isZF = isZF
} where
ZFSet = OD {suc n}
Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → Set (suc n) ) → OD {suc n}
Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
_,_ : OD {suc n} → OD {suc n} → OD {suc n}
x , y = Ord (omax (od→ord x) (od→ord y))
_∩_ : ( A B : ZFSet ) → ZFSet
A ∩ B = record { def = λ x → def A x ∧ def B x }
Union : OD {suc n} → OD {suc n}
Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
_∈_ : ( A B : ZFSet ) → Set (suc n)
A ∈ B = B ∋ A
Power : OD {suc n} → OD {suc n}
Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
{_} : ZFSet → ZFSet
{ x } = ( x , x )
data infinite-d : ( x : Ordinal {suc n} ) → Set (suc n) where
iφ : infinite-d o∅
isuc : {x : Ordinal {suc n} } → infinite-d x →
infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
infinite : OD {suc n}
infinite = record { def = λ x → infinite-d x }
infixr 200 _∈_
-- infixr 230 _∩_ _∪_
isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite
isZF = record {
isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
; pair = pair
; union→ = union→
; union← = union←
; empty = empty
; power→ = power→
; power← = power←
; extensionality = λ {A} {B} {w} → extensionality {A} {B} {w}
; ε-induction = ε-induction
; infinity∅ = infinity∅
; infinity = infinity
; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
; replacement← = replacement←
; replacement→ = replacement→
; choice-func = choice-func
; choice = choice
} where
pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
empty : {n : Level } (x : OD {suc n} ) → ¬ (od∅ ∋ x)
empty x (case1 ())
empty x (case2 ())
o<→c< : {x y : Ordinal {suc n}} {z : OD {suc n}}→ x o< y → _⊆_ (Ord x) (Ord y) {z}
o<→c< lt lt1 = ordtrans lt1 lt
⊆→o< : {x y : Ordinal {suc n}} → (∀ (z : OD) → _⊆_ (Ord x) (Ord y) {z} ) → x o< osuc y
⊆→o< {x} {y} lt with trio< x y
⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc
⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl )
... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
union← X z UX∋z = TransFiniteExists _ lemma UX∋z where
lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y
ψiso {ψ} t refl = t
selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
selection {ψ} {X} {y} = record {
proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }
; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
}
replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x
replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where
lemma : def (in-codomain X ψ) (od→ord (ψ x))
lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
→ ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)))
lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y))) → (ord→od (od→ord x) == ψ (ord→od y))
lemma3 {y} eq = subst (λ k → ord→od (od→ord x) == k ) oiso (o≡→== eq )
lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)) )
lemma not y not2 = not (ord→od y) (subst (λ k → k == ψ (ord→od y)) oiso ( proj2 not2 ))
---
--- Power Set
---
--- First consider ordinals in OD
---
--- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A
--- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A
--
--
∩-≡ : { a b : OD {suc n} } → ({x : OD {suc n} } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
∩-≡ {a} {b} inc = record {
eq→ = λ {x} x ¬a ¬b c = -- lz(a)
subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz ¬a ¬b c with d<→lv lz=ly -- lz(b)
... | eq = subst (λ k → ψ k ) oiso
(ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c )))
lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly -- lz(c)
... | eq = lemma6 {ly} {Φ lx} {oy} lx=ly (sym (subst (λ k → lv (od→ord z) ≡ k) lemma1 eq)) where
lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z
lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt )
lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } →
lx ≡ ly → ly ≡ lv (od→ord z) → ψ z
lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s axiom of choice
---
record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where
field
a-choice : OD {suc n}
is-in : X ∋ a-choice
choice-func' : (X : OD {suc n} ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
choice-func' X p∨¬p not = have_to_find
where
ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
ψ ox = (( x : Ordinal {suc n}) → x o< ox → ( ¬ def X x )) ∨ choiced X
lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
lemma-ord ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc ox where
∋-p' : (A x : OD {suc n} ) → Dec ( A ∋ x )
∋-p' A x with p∨¬p ( A ∋ x )
∋-p' A x | case1 t = yes t
∋-p' A x | case2 t = no t
∀-imply-or : {n : Level} {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) }
→ ((x : Ordinal {suc n}) → A x ∨ B) → ((x : Ordinal {suc n}) → A x) ∨ B
∀-imply-or {n} {A} {B} ∀AB with p∨¬p ((x : Ordinal {suc n}) → A x)
∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t
∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where
lemma : ¬ ((x : Ordinal {suc n}) → A x) → B
lemma not with p∨¬p B
lemma not | case1 b = b
lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) )
caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) ))
caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
caseΦ lx prev | no ¬p = lemma where
lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X)
lemma1 x with trio< x (ordinal lx (Φ lx))
lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where
lemma2 : x o< (ordinal lx (Φ lx)) → osuc x o< ordinal lx (Φ lx)
lemma2 (case1 lt) = case1 lt
lemma1 x | tri< a ¬b ¬c | case2 found = case2 found
lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df )
lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt ))
lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c ))
lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X
lemma = ∀-imply-or lemma1
caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } )
caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where
lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥
lemma y lt with trio< y (ordinal lx x )
lemma y lt | tri< a ¬b ¬c = not_found y a
lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p
lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
caseOSuc lx x (case2 found) | no ¬p = case2 found
have_to_find : choiced X
have_to_find with lemma-ord (od→ord X )
have_to_find | t = dont-or t ¬¬X∋x where
¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (od→ord X)) → def X x → ⊥)
¬¬X∋x nn = not record {
eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
}