Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate README.md @ 1036:23a8e4d558e0
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 02 Dec 2022 15:49:50 +0900 |
parents | a5f8084b8368 |
children | 42000f20fdbe |
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 | |
8 ``` | |
9 zf.agda axiom of ZF | |
10 zfc.agda axiom of choice | |
11 Ordinals.agda axiom of Ordinals | |
12 ordinal.agda countable model of Ordinals | |
13 OD.agda model of ZF based on Ordinal Definable Set with assumptions | |
14 ODC.agda Law of exclude middle from axiom of choice assumptions | |
15 LEMC.agda model of choice with assumption of the Law of exclude middle | |
16 OPair.agda ordered pair on OD | |
17 | |
18 BAlgbra.agda Boolean algebra on OD (not yet done) | |
19 filter.agda Filter on OD (not yet done) | |
20 cardinal.agda Caedinal number on OD (not yet done) | |
21 | |
22 logic.agda some basics on logic | |
23 nat.agda some basics on Nat | |
24 ``` | |
25 | |
26 ## Ordinal Definable Set | |
27 | |
28 It is a predicate has an Ordinal argument. | |
29 | |
30 In Agda, OD is defined as follows. | |
31 | |
32 ``` | |
33 record OD : Set (suc n ) where | |
34 field | |
35 def : (x : Ordinal ) → Set n | |
36 ``` | |
37 | |
38 This is not a ZF Set, because it can contain entire Ordinals. | |
39 | |
338 | 40 ## HOD : Hereditarily Ordinal Definable |
337 | 41 |
42 What we need is a bounded OD, the containment is limited by an ordinal. | |
43 | |
44 ``` | |
45 record HOD : Set (suc n) where | |
46 field | |
47 od : OD | |
48 odmax : Ordinal | |
49 <odmax : {y : Ordinal} → def od y → y o< odmax | |
50 ``` | |
51 | |
52 In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means | |
53 | |
54 ``` | |
55 HOD = { x | TC x ⊆ OD } | |
56 ``` | |
57 | |
58 TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But | |
59 what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. | |
60 | |
61 ## 1 to 1 mapping between an HOD and an Ordinal | |
62 | |
63 HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping | |
64 | |
65 ``` | |
66 od→ord : HOD → Ordinal | |
67 ord→od : Ordinal → HOD | |
68 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x | |
69 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | |
70 ``` | |
71 | |
72 we can check an HOD is an element of the OD using def. | |
73 | |
74 A ∋ x can be define as follows. | |
75 | |
76 ``` | |
77 _∋_ : ( A x : HOD ) → Set n | |
78 _∋_ A x = def (od A) ( od→ord x ) | |
79 | |
80 ``` | |
431
a5f8084b8368
reorganiztion for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
359
diff
changeset
|
81 In ψ : Ordinal → Set, if A is a record { od = { def = λ x → ψ x } ...} , then |
337 | 82 |
431
a5f8084b8368
reorganiztion for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
359
diff
changeset
|
83 A ∋ x = def (od A) ( od→ord x ) = ψ (od→ord x) |
337 | 84 |
85 They say the existing of the mappings can be proved in Classical Set Theory, but we | |
86 simply assumes these non constructively. | |
87 |