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

comparison src/OD.agda @ 1297:ad9ed7c4a0b3

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 Sat, 03 Jun 2023 08:13:50 +0900
parents 968feed7cf64
children 47d3cc596d68
comparison
equal deleted inserted replaced
1296:428227847d62 1297:ad9ed7c4a0b3
106 postulate odAxiom : ODAxiom 106 postulate odAxiom : ODAxiom
107 open ODAxiom odAxiom 107 open ODAxiom odAxiom
108 108
109 -- possible order restriction (required in the axiom of infinite ) 109 -- possible order restriction (required in the axiom of infinite )
110 110
111 record ODAxiom-ho< : Set (suc n) where 111 -- postulate odAxiom-ho< : ODAxiom-ho<
112 field 112 -- open ODAxiom-ho< odAxiom-ho<
113 ho< : {x : HOD} → & x o< next (odmax x)
114
115 postulate odAxiom-ho< : ODAxiom-ho<
116 open ODAxiom-ho< odAxiom-ho<
117 113
118 -- odmax minimality 114 -- odmax minimality
119 -- 115 --
120 -- since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD. 116 -- since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD.
121 -- We can calculate the minimum using sup but it is tedius. 117 -- We can calculate the minimum using sup but it is tedius.
449 445
450 446
451 -- ｛_｝ : ZFSet → ZFSet 447 -- ｛_｝ : ZFSet → ZFSet
452 -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly 448 -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly
453 449
454
455 data infinite-d : ( x : Ordinal ) → Set n where 450 data infinite-d : ( x : Ordinal ) → Set n where
456 iφ : infinite-d o∅ 451 iφ : infinite-d o∅
457 isuc : {x : Ordinal } → infinite-d x → 452 isuc : {x : Ordinal } → infinite-d x →
458 infinite-d (& ( Union (* x , (* x , * x ) ) )) 453 infinite-d (& ( Union (* x , (* x , * x ) ) ))
459 454
463 -- This means that many of OD may not be HODs because of the & mapping divergence. 458 -- This means that many of OD may not be HODs because of the & mapping divergence.
464 -- We should have some axioms to prevent this such as & x o< next (odmax x). 459 -- We should have some axioms to prevent this such as & x o< next (odmax x).
465 -- 460 --
466 -- Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho< 461 -- Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho<
467 462
463 infinite-od : OD
464 infinite-od = record { def = λ x → infinite-d x }
465
466 record ODAxiom-ho< : Set (suc n) where
467 field
468 omega : Ordinal
469 ho< : {x : Ordinal } → infinite-d x → x o< next omega
470
471 postulate
472 odaxion-ho< : ODAxiom-ho<
473
474 open ODAxiom-ho< odaxion-ho<
475
468 infinite : HOD 476 infinite : HOD
469 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where 477 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next omega ; <odmax = ho<}
470 u : (y : Ordinal ) → HOD
471 u y = Union (* y , (* y , * y))
472 -- next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z
473 lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y))
474 lemma8 = ho<
475 --- (x,y) < next (omax x y) < next (osuc y) = next y
476 lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y)
477 lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
478 lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y))
479 lemma81 {y} = nexto=n (subst (λ k → & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
480 lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y))
481 lemma9 = lemmaa (c<→o< (case1 refl))
482 lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y))
483 lemma71 = next< lemma81 lemma9
484 lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y))))
485 lemma1 = ho<
486 --- main recursion
487 lemma : {y : Ordinal} → infinite-d y → y o< next o∅
488 lemma {o∅} iφ = x<nx
489 lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))
490 478
491 empty : (x : HOD ) → ¬ (od∅ ∋ x) 479 empty : (x : HOD ) → ¬ (od∅ ∋ x)
492 empty x = ¬x<0 480 empty x = ¬x<0
493 481
494 pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y ) 482 pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y )