Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate README.md @ 1464:484f83b04b5d default tip
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Jan 2024 19:29:23 +0900 |
| parents | 003424a36fed |
| children |
| rev | line source |
|---|---|
| 337 | 1 Constructing ZF Set Theory in Agda |
| 2 ============ | |
| 3 | |
| 4 Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus | |
| 5 | |
| 6 ## ZF in Agda | |
| 7 | |
| 1200 | 8 [zfc](https://shinji-kono.github.io/zf-in-agda/html/zfc.html) axiom of choice |
| 9 | |
| 10 [NSet](https://shinji-kono.github.io/zf-in-agda/html/NSet.html) Naive Set Theory | |
| 11 | |
| 12 [Ordinals](https://shinji-kono.github.io/zf-in-agda/html/Ordinals.html) axiom of Ordinals | |
| 13 | |
| 14 [OD](https://shinji-kono.github.io/zf-in-agda/html/OD.html) a model of ZF based on Ordinal Definable Set with assumptions | |
| 15 | |
| 16 [ODC](https://shinji-kono.github.io/zf-in-agda/html/ODC.html) Law of exclude middle from axiom of choice assumptions | |
| 17 | |
| 18 [LEMC](https://shinji-kono.github.io/zf-in-agda/html/LEMC.html) choice with assumption of the Law of exclude middle | |
| 19 | |
| 20 [BAlgebra](https://shinji-kono.github.io/zf-in-agda/html/BAlgebra.html) Boolean algebra on OD (not yet done) | |
| 21 | |
| 22 [zorn](https://shinji-kono.github.io/zf-in-agda/html/zorn.html) Zorn lemma | |
| 23 | |
| 24 [Topology](https://shinji-kono.github.io/zf-in-agda/html/Topology.html) Topology | |
| 337 | 25 |
| 1200 | 26 [Tychonoff](https://shinji-kono.github.io/zf-in-agda/html/Tychonoff.html) |
| 27 | |
| 28 [VL](https://shinji-kono.github.io/zf-in-agda/html/VL.html) V and L | |
| 29 | |
| 30 [cardinal](https://shinji-kono.github.io/zf-in-agda/html/cardinal.html) Cardinals | |
| 31 | |
| 32 [filter](https://shinji-kono.github.io/zf-in-agda/html/filter.html) Filter | |
| 337 | 33 |
| 1200 | 34 [generic-filter](https://shinji-kono.github.io/zf-in-agda/html/generic-filter.html) Generic Filter |
| 35 | |
| 36 [maximum-filter](https://shinji-kono.github.io/zf-in-agda/html/maximum-filter.html) Maximum filter by Zorn lemma | |
| 37 | |
| 38 [ordinal](https://shinji-kono.github.io/zf-in-agda/html/ordinal.html) countable model of Ordinals | |
| 39 | |
| 40 [OPair](https://shinji-kono.github.io/zf-in-agda/html/OPair.html) Orderd Pair and Direct Product | |
| 41 | |
| 1387 | 42 [bijection](https://shinji-kono.github.io/zf-in-agda/html/bijection.html) Bijection without HOD |
| 43 | |
| 1200 | 44 |
| 337 | 45 ``` |
| 46 | |
| 47 ## Ordinal Definable Set | |
| 48 | |
| 49 It is a predicate has an Ordinal argument. | |
| 50 | |
| 51 In Agda, OD is defined as follows. | |
| 52 | |
| 53 ``` | |
| 54 record OD : Set (suc n ) where | |
| 55 field | |
| 56 def : (x : Ordinal ) → Set n | |
| 57 ``` | |
| 58 | |
| 59 This is not a ZF Set, because it can contain entire Ordinals. | |
| 60 | |
| 338 | 61 ## HOD : Hereditarily Ordinal Definable |
| 337 | 62 |
| 63 What we need is a bounded OD, the containment is limited by an ordinal. | |
| 64 | |
| 65 ``` | |
| 66 record HOD : Set (suc n) where | |
| 67 field | |
| 68 od : OD | |
| 69 odmax : Ordinal | |
| 70 <odmax : {y : Ordinal} → def od y → y o< odmax | |
| 71 ``` | |
| 72 | |
| 73 In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means | |
| 74 | |
| 75 ``` | |
| 76 HOD = { x | TC x ⊆ OD } | |
| 77 ``` | |
| 78 | |
| 79 TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But | |
| 80 what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. | |
| 81 | |
| 82 ## 1 to 1 mapping between an HOD and an Ordinal | |
| 83 | |
| 84 HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping | |
| 85 | |
| 86 ``` | |
| 87 od→ord : HOD → Ordinal | |
| 88 ord→od : Ordinal → HOD | |
| 89 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x | |
| 90 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | |
| 91 ``` | |
| 92 | |
| 93 we can check an HOD is an element of the OD using def. | |
| 94 | |
| 95 A ∋ x can be define as follows. | |
| 96 | |
| 97 ``` | |
| 98 _∋_ : ( A x : HOD ) → Set n | |
| 99 _∋_ A x = def (od A) ( od→ord x ) | |
| 100 | |
| 101 ``` | |
|
431
a5f8084b8368
reorganiztion for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
359
diff
changeset
|
102 In ψ : Ordinal → Set, if A is a record { od = { def = λ x → ψ x } ...} , then |
| 337 | 103 |
|
431
a5f8084b8368
reorganiztion for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
359
diff
changeset
|
104 A ∋ x = def (od A) ( od→ord x ) = ψ (od→ord x) |
| 337 | 105 |
| 106 They say the existing of the mappings can be proved in Classical Set Theory, but we | |
| 107 simply assumes these non constructively. | |
| 108 |