Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison ordinal.agda @ 184:65e1b2e415bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2019 17:31:52 +0900
parents de3d87b7494f
children ed88384b5102
comparison
equal deleted inserted replaced
183:de3d87b7494f 184:65e1b2e415bb
15 record Ordinal {n : Level} : Set n where 15 record Ordinal {n : Level} : Set n where
16 field 16 field
17 lv : Nat 17 lv : Nat
18 ord : OrdinalD {n} lv 18 ord : OrdinalD {n} lv
19 19
20 --
21 -- Φ (Suc lv) < ℵ lv < OSuc (Suc lv) (ℵ lv) < OSuc ... < OSuc (Suc lv) (Φ (Suc lv)) < OSuc ... < ℵ (Suc lv)
22 --
23 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where 20 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where
24 Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x 21 Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x
25 s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y 22 s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y
26 23
27 open Ordinal 24 open Ordinal
298 proj1 (osuc2 {n} x y) (case2 (s< lt)) = case2 lt 295 proj1 (osuc2 {n} x y) (case2 (s< lt)) = case2 lt
299 proj2 (osuc2 {n} x y) (case1 lt) = case1 lt 296 proj2 (osuc2 {n} x y) (case1 lt) = case1 lt
300 proj2 (osuc2 {n} x y) (case2 lt) with d<→lv lt 297 proj2 (osuc2 {n} x y) (case2 lt) with d<→lv lt
301 ... | refl = case2 (s< lt) 298 ... | refl = case2 (s< lt)
302 299
303 -- omax≡ (omax x x ) (osuc x) (omxx x)
304
305 OrdTrans : {n : Level} → Transitive {suc n} _o≤_ 300 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
306 OrdTrans (case1 refl) (case1 refl) = case1 refl 301 OrdTrans (case1 refl) (case1 refl) = case1 refl
307 OrdTrans (case1 refl) (case2 lt2) = case2 lt2 302 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
308 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 303 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
309 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) 304 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
325 → ∀ (x : Ordinal) → ψ x 320 → ∀ (x : Ordinal) → ψ x
326 TransFinite caseΦ caseOSuc record { lv = lv ; ord = (Φ (lv)) } = caseΦ lv 321 TransFinite caseΦ caseOSuc record { lv = lv ; ord = (Φ (lv)) } = caseΦ lv
327 TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = 322 TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } =
328 caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox }) 323 caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox })
329 324
330 -- we cannot prove this in intutonistic logic 325 -- we cannot prove this in intutionistic logic
331 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p 326 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p
332 -- postulate 327 -- postulate
333 -- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 328 -- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )
334 -- → (exists : ¬ (∀ y → ¬ ( ψ y ) )) 329 -- → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
335 -- → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → p ) 330 -- → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → p )