|
273
|
1 -title: Constructing ZF Set Theory in Agda
|
|
|
2
|
|
|
3 --author: Shinji KONO
|
|
|
4
|
|
279
|
5 --ZF in Agda
|
|
|
6
|
|
|
7 zf.agda axiom of ZF
|
|
|
8 zfc.agda axiom of choice
|
|
|
9 Ordinals.agda axiom of Ordinals
|
|
|
10 ordinal.agda countable model of Ordinals
|
|
|
11 OD.agda model of ZF based on Ordinal Definable Set with assumptions
|
|
|
12 ODC.agda Law of exclude middle from axiom of choice assumptions
|
|
|
13 LEMC.agda model of choice with assumption of the Law of exclude middle
|
|
|
14 OPair.agda ordered pair on OD
|
|
|
15
|
|
|
16 BAlgbra.agda Boolean algebra on OD (not yet done)
|
|
|
17 filter.agda Filter on OD (not yet done)
|
|
|
18 cardinal.agda Caedinal number on OD (not yet done)
|
|
|
19
|
|
|
20 logic.agda some basics on logic
|
|
|
21 nat.agda some basics on Nat
|
|
|
22
|
|
273
|
23 --Programming Mathematics
|
|
|
24
|
|
|
25 Programming is processing data structure with λ terms.
|
|
|
26
|
|
|
27 We are going to handle Mathematics in intuitionistic logic with λ terms.
|
|
|
28
|
|
|
29 Mathematics is a functional programming which values are proofs.
|
|
|
30
|
|
|
31 Programming ZF Set Theory in Agda
|
|
|
32
|
|
|
33 --Target
|
|
|
34
|
|
|
35 Describe ZF axioms in Agda
|
|
|
36 Construction a Model of ZF Set Theory in Agda
|
|
|
37 Show necessary assumptions for the model
|
|
|
38 Show validities of ZF axioms on the model
|
|
|
39
|
|
|
40 This shows consistency of Set Theory (with some assumptions),
|
|
|
41 without circulating ZF Theory assumption.
|
|
|
42
|
|
|
43 <a href="https://github.com/shinji-kono/zf-in-agda">
|
|
|
44 ZF in Agda https://github.com/shinji-kono/zf-in-agda
|
|
|
45 </a>
|
|
|
46
|
|
|
47 --Why Set Theory
|
|
|
48
|
|
|
49 If we can formulate Set theory, it suppose to work on any mathematical theory.
|
|
|
50
|
|
|
51 Set Theory is a difficult point for beginners especially axiom of choice.
|
|
|
52
|
|
|
53 It has some amount of difficulty and self circulating discussion.
|
|
|
54
|
|
|
55 I'm planning to do it in my old age, but I'm enough age now.
|
|
|
56
|
|
|
57 This is done during from May to September.
|
|
|
58
|
|
|
59 --Agda and Intuitionistic Logic
|
|
|
60
|
|
|
61 Curry Howard Isomorphism
|
|
|
62
|
|
|
63 Proposition : Proof ⇔ Type : Value
|
|
|
64
|
|
|
65 which means
|
|
|
66
|
|
|
67 constructing a typed lambda calculus which corresponds a logic
|
|
|
68
|
|
|
69 Typed lambda calculus which allows complex type as a value of a variable (System FC)
|
|
|
70
|
|
|
71 First class Type / Dependent Type
|
|
|
72
|
|
|
73 Agda is a such a programming language which has similar syntax of Haskell
|
|
|
74
|
|
|
75 Coq is specialized in proof assistance such as command and tactics .
|
|
|
76
|
|
|
77 --Introduction of Agda
|
|
|
78
|
|
|
79 A length of a list of type A.
|
|
|
80
|
|
|
81 length : {A : Set } → List A → Nat
|
|
|
82 length [] = zero
|
|
|
83 length (_ ∷ t) = suc ( length t )
|
|
|
84
|
|
|
85 Simple functional programming language. Type declaration is mandatory.
|
|
|
86 A colon means type, an equal means value. Indentation based.
|
|
|
87
|
|
|
88 Set is a base type (which may have a level ).
|
|
|
89
|
|
|
90 {} means implicit variable which can be omitted if Agda infers its value.
|
|
|
91
|
|
|
92 --data ( Sum type )
|
|
|
93
|
|
|
94 A data type which as exclusive multiple constructors. A similar one as
|
|
|
95 union in C or case class in Scala.
|
|
|
96
|
|
|
97 It has a similar syntax as Haskell but it has a slight difference.
|
|
|
98
|
|
|
99 data List (A : Set ) : Set where
|
|
|
100 [] : List A
|
|
|
101 _∷_ : A → List A → List A
|
|
|
102
|
|
|
103 _∷_ means infix operator. If use explicit _, it can be used in a normal function
|
|
|
104 syntax.
|
|
|
105
|
|
|
106 Natural number can be defined as a usual way.
|
|
|
107
|
|
|
108 data Nat : Set where
|
|
|
109 zero : Nat
|
|
|
110 suc : Nat → Nat
|
|
|
111
|
|
|
112 -- A → B means "A implies B"
|
|
|
113
|
|
|
114 In Agda, a type can be a value of a variable, which is usually called dependent type.
|
|
|
115 Type has a name Set in Agda.
|
|
|
116
|
|
|
117 ex3 : {A B : Set} → Set
|
|
|
118 ex3 {A}{B} = A → B
|
|
|
119
|
|
|
120 ex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B.
|
|
|
121
|
|
|
122 A type is a formula, the value is the proof
|
|
|
123
|
|
|
124 A value of A → B can be interpreted as an inference from the formula A to the formula B, which
|
|
|
125 can be a function from a proof of A to a proof of B.
|
|
|
126
|
|
|
127 --introduction と elimination
|
|
|
128
|
|
|
129 For a logical operator, there are two types of inference, an introduction and an elimination.
|
|
|
130
|
|
|
131 intro creating symbol / constructor / introduction
|
|
|
132 elim using symbolic / accessors / elimination
|
|
|
133
|
|
|
134 In Natural deduction, this can be written in proof schema.
|
|
|
135
|
|
|
136 A
|
|
|
137 :
|
|
|
138 B A A → B
|
|
|
139 ------------- →intro ------------------ →elim
|
|
|
140 A → B B
|
|
|
141
|
|
|
142 In Agda, this is a pair of type and value as follows. Introduction of → uses λ.
|
|
|
143
|
|
|
144 →intro : {A B : Set } → A → B → ( A → B )
|
|
|
145 →intro _ b = λ x → b
|
|
|
146
|
|
|
147 →elim : {A B : Set } → A → ( A → B ) → B
|
|
|
148 →elim a f = f a
|
|
|
149
|
|
|
150 Important
|
|
|
151
|
|
|
152 {A B : Set } → A → B → ( A → B )
|
|
|
153
|
|
|
154 is
|
|
|
155
|
|
|
156 {A B : Set } → ( A → ( B → ( A → B ) ))
|
|
|
157
|
|
|
158 This makes currying of function easy.
|
|
|
159
|
|
|
160 -- To prove A → B
|
|
|
161
|
|
|
162 Make a left type as an argument. (intros in Coq)
|
|
|
163
|
|
|
164 ex5 : {A B C : Set } → A → B → C → ?
|
|
|
165 ex5 a b c = ?
|
|
|
166
|
|
|
167 ? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole.
|
|
|
168
|
|
|
169 We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red),
|
|
|
170 insufficient proof or instance (Yellow), Non-termination, the proof is completed.
|
|
|
171
|
|
|
172 -- A ∧ B
|
|
|
173
|
|
|
174 Well known conjunction's introduction and elimination is as follow.
|
|
|
175
|
|
|
176 A B A ∧ B A ∧ B
|
|
|
177 ------------- ----------- proj1 ---------- proj2
|
|
|
178 A ∧ B A B
|
|
|
179
|
|
|
180 We can introduce a corresponding structure in our functional programming language.
|
|
|
181
|
|
|
182 -- record
|
|
|
183
|
|
|
184 record _∧_ A B : Set
|
|
|
185 field
|
|
|
186 proj1 : A
|
|
|
187 proj2 : B
|
|
|
188
|
|
|
189 _∧_ means infix operator. _∧_ A B can be written as A ∧ B (Haskell uses (∧) )
|
|
|
190
|
|
|
191 This a type which constructed from type A and type B. You may think this as an object
|
|
|
192 or struct.
|
|
|
193
|
|
|
194 record { proj1 = x ; proj2 = y }
|
|
|
195
|
|
|
196 is a constructor of _∧_.
|
|
|
197
|
|
|
198 ex3 : {A B : Set} → A → B → ( A ∧ B )
|
|
|
199 ex3 a b = record { proj1 = a ; proj2 = b }
|
|
|
200
|
|
|
201 ex1 : {A B : Set} → ( A ∧ B ) → A
|
|
|
202 ex1 a∧b = proj1 a∧b
|
|
|
203
|
|
|
204 a∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols
|
|
|
205 except parenthesis or colons. A symbol requires space separation such as a type defining colon.
|
|
|
206
|
|
|
207 Defining record can be recursively, but we don't use the recursion here.
|
|
|
208
|
|
|
209 -- Mathematical structure
|
|
|
210
|
|
|
211 We have types of elements and the relationship in a mathematical structure.
|
|
|
212
|
|
|
213 logical relation has no ordering
|
|
|
214 there is a natural ordering in arguments and a value in a function
|
|
|
215
|
|
|
216 So we have typical definition style of mathematical structure with records.
|
|
|
217
|
|
|
218 record IsOrdinals {n : Level} (ord : Set n)
|
|
|
219 (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
|
|
|
220 field
|
|
|
221 Otrans : {x y z : ord } → x o< y → y o< z → x o< z
|
|
|
222
|
|
|
223 record Ordinals {n : Level} : Set (suc (suc n)) where
|
|
|
224 field
|
|
|
225 ord : Set n
|
|
|
226 _o<_ : ord → ord → Set n
|
|
|
227 isOrdinal : IsOrdinals ord _o<_
|
|
|
228
|
|
|
229 In IsOrdinals, axioms are written in flat way. In Ordinal, we may have
|
|
|
230 inputs and outputs are put in the field including IsOrdinal.
|
|
|
231
|
|
|
232 Fields of Ordinal is existential objects in the mathematical structure.
|
|
|
233
|
|
|
234 -- A Model and a theory
|
|
|
235
|
|
|
236 Agda record is a type, so we can write it in the argument, but is it really exists?
|
|
|
237
|
|
|
238 If we have a value of the record, it simply exists, that is, we need to create all the existence
|
|
|
239 in the record satisfies all the axioms (= field of IsOrdinal) should be valid.
|
|
|
240
|
|
|
241 type of record = theory
|
|
|
242 value of record = model
|
|
|
243
|
|
|
244 We call the value of the record as a model. If mathematical structure has a
|
|
|
245 model, it exists. Pretty Obvious.
|
|
|
246
|
|
|
247 -- postulate と module
|
|
|
248
|
|
|
249 Agda proofs are separated by modules, which are large records.
|
|
|
250
|
|
|
251 postulates are assumptions. We can assume a type without proofs.
|
|
|
252
|
|
|
253 postulate
|
|
|
254 sup-o : ( Ordinal → Ordinal ) → Ordinal
|
|
|
255 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ
|
|
|
256
|
|
|
257 sup-o is an example of upper bound of a function and sup-o< assumes it actually
|
|
|
258 satisfies all the value is less than upper bound.
|
|
|
259
|
|
|
260 Writing some type in a module argument is the same as postulating a type, but
|
|
|
261 postulate can be written the middle of a proof.
|
|
|
262
|
|
|
263 postulate can be constructive.
|
|
|
264
|
|
|
265 postulate can be inconsistent, which result everything has a proof.
|
|
|
266
|
|
|
267 -- A ∨ B
|
|
|
268
|
|
|
269 data _∨_ (A B : Set) : Set where
|
|
|
270 case1 : A → A ∨ B
|
|
|
271 case2 : B → A ∨ B
|
|
|
272
|
|
|
273 As Haskell, case1/case2 are patterns.
|
|
|
274
|
|
|
275 ex3 : {A B : Set} → ( A ∨ A ) → A
|
|
|
276 ex3 = ?
|
|
|
277
|
|
|
278 In a case statement, Agda command C-C C-C generates possible cases in the head.
|
|
|
279
|
|
|
280 ex3 : {A B : Set} → ( A ∨ A ) → A
|
|
|
281 ex3 (case1 x) = ?
|
|
|
282 ex3 (case2 x) = ?
|
|
|
283
|
|
|
284 Proof schema of ∨ is omit due to the complexity.
|
|
|
285
|
|
|
286 -- Negation
|
|
|
287
|
|
|
288 ⊥
|
|
|
289 ------------- ⊥-elim
|
|
|
290 A
|
|
|
291
|
|
|
292 Anything can be derived from bottom, in this case a Set A. There is no introduction rule
|
|
|
293 in ⊥, which can be implemented as data which has no constructor.
|
|
|
294
|
|
|
295 data ⊥ : Set where
|
|
|
296
|
|
|
297 ⊥-elim can be proved like this.
|
|
|
298
|
|
|
299 ⊥-elim : {A : Set } -> ⊥ -> A
|
|
|
300 ⊥-elim ()
|
|
|
301
|
|
|
302 () means no match argument nor value.
|
|
|
303
|
|
|
304 A negation can be defined using ⊥ like this.
|
|
|
305
|
|
|
306 ¬_ : Set → Set
|
|
|
307 ¬ A = A → ⊥
|
|
|
308
|
|
|
309 --Equality
|
|
|
310
|
|
|
311 All the value in Agda are terms. If we have the same normalized form, two terms are equal.
|
|
|
312 If we have variables in the terms, we will perform an unification. unifiable terms are equal.
|
|
|
313 We don't go further on the unification.
|
|
|
314
|
|
|
315 { x : A } x ≡ y f x y
|
|
|
316 --------------- ≡-intro --------------------- ≡-elim
|
|
|
317 x ≡ x f x x
|
|
|
318
|
|
|
319 equality _≡_ can be defined as a data.
|
|
|
320
|
|
|
321 data _≡_ {A : Set } : A → A → Set where
|
|
|
322 refl : {x : A} → x ≡ x
|
|
|
323
|
|
|
324 The elimination of equality is a substitution in a term.
|
|
|
325
|
|
|
326 subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y
|
|
|
327 subst {A} {x} {y} f refl fx = fx
|
|
|
328
|
|
|
329 ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
|
|
|
330 ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y
|
|
|
331
|
|
|
332
|
|
|
333 --Equivalence relation
|
|
|
334
|
|
|
335 refl' : {A : Set} {x : A } → x ≡ x
|
|
|
336 refl' = ?
|
|
|
337 sym : {A : Set} {x y : A } → x ≡ y → y ≡ x
|
|
|
338 sym = ?
|
|
|
339 trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
|
|
|
340 trans = ?
|
|
|
341 cong : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y
|
|
|
342 cong = ?
|
|
|
343
|
|
|
344 --Ordering
|
|
|
345
|
|
|
346 Relation is a predicate on two value which has a same type.
|
|
|
347
|
|
|
348 A → A → Set
|
|
|
349
|
|
|
350 Defining order is the definition of this type with predicate or a data.
|
|
|
351
|
|
|
352 data _≤_ : Rel ℕ 0ℓ where
|
|
|
353 z≤n : ∀ {n} → zero ≤ n
|
|
|
354 s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
|
|
|
355
|
|
|
356
|
|
|
357 --Quantifier
|
|
|
358
|
|
|
359 Handling quantifier in an intuitionistic logic requires special cares.
|
|
|
360
|
|
|
361 In the input of a function, there are no restriction on it, that is, it has
|
|
|
362 a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it)
|
|
|
363
|
|
|
364 There is no ∃ in agda, the one way is using negation like this.
|
|
|
365
|
|
|
366 ∃ (x : A ) → p x = ¬ ( ( x : A ) → ¬ ( p x ) )
|
|
|
367
|
|
|
368 On the another way, f : A can be used like this.
|
|
|
369
|
|
|
370 p f
|
|
|
371
|
|
|
372 If we use a function which can be defined globally which has stronger meaning the
|
|
|
373 usage of ∃ x in a logical expression.
|
|
|
374
|
|
|
375
|
|
|
376 --Can we do math in this way?
|
|
|
377
|
|
|
378 Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support).
|
|
|
379
|
|
|
380 In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF).
|
|
|
381
|
|
|
382 define mathematical structure as a record
|
|
|
383 program inferences as if we have proofs in variables
|
|
|
384
|
|
|
385 --Things which Agda cannot prove
|
|
|
386
|
|
|
387 The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which
|
|
|
388 leads uniqueness of a functor in Category Theory.
|
|
|
389
|
|
|
390 Functional extensionality cannot be proved.
|
|
|
391 (∀ x → f x ≡ g x) → f ≡ g
|
|
|
392
|
|
|
393 Agda has no law of exclude middle.
|
|
|
394
|
|
|
395 a ∨ ( ¬ a )
|
|
|
396
|
|
|
397 For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot.
|
|
|
398
|
|
|
399 It also other problems such as termination, type inference or unification which we may overcome with
|
|
|
400 efforts or devices or may not.
|
|
|
401
|
|
|
402 If we cannot prove something, we can safely postulate it unless it leads a contradiction.
|
|
|
403
|
|
|
404 --Classical story of ZF Set Theory
|
|
|
405
|
|
|
406 Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads
|
|
|
407 a relative consistency proof of the Set Theory.
|
|
|
408 Ordinal number is used in the flow.
|
|
|
409
|
|
|
410 In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD).
|
|
|
411 We need some non constructive assumptions in the construction. A model of Set theory is
|
|
|
412 constructed based on these assumptions.
|
|
|
413
|
|
|
414 <center><img src="fig/set-theory.svg"></center>
|
|
|
415
|
|
|
416 --Ordinals
|
|
|
417
|
|
|
418 Ordinals are our intuition of infinite things, which has ∅ and orders on the things.
|
|
|
419 It also has a successor osuc.
|
|
|
420
|
|
|
421 record Ordinals {n : Level} : Set (suc (suc n)) where
|
|
|
422 field
|
|
|
423 ord : Set n
|
|
|
424 o∅ : ord
|
|
|
425 osuc : ord → ord
|
|
|
426 _o<_ : ord → ord → Set n
|
|
|
427 isOrdinal : IsOrdinals ord o∅ osuc _o<_
|
|
|
428
|
|
|
429 It is different from natural numbers in way. The order of Ordinals is not defined in terms
|
|
|
430 of successor. It is given from outside, which make it possible to have higher order infinity.
|
|
|
431
|
|
|
432 --Axiom of Ordinals
|
|
|
433
|
|
|
434 Properties of infinite things. We request a transfinite induction, which states that if
|
|
|
435 some properties are satisfied below all possible ordinals, the properties are true on all
|
|
|
436 ordinals.
|
|
|
437
|
|
|
438 Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals
|
|
|
439 which is not a successor of any ordinals. It is called limit ordinal.
|
|
|
440
|
|
|
441 Any two ordinal can be compared, that is less, equal or more, that is total order.
|
|
|
442
|
|
|
443 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord )
|
|
|
444 (osuc : ord → ord )
|
|
|
445 (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
|
|
|
446 field
|
|
|
447 Otrans : {x y z : ord } → x o< y → y o< z → x o< z
|
|
|
448 OTri : Trichotomous {n} _≡_ _o<_
|
|
|
449 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
|
|
|
450 <-osuc : { x : ord } → x o< osuc x
|
|
|
451 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
|
|
|
452 TransFinite : { ψ : ord → Set (suc n) }
|
|
|
453 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
|
|
|
454 → ∀ (x : ord) → ψ x
|
|
|
455
|
|
|
456 --Concrete Ordinals
|
|
|
457
|
|
|
458 We can define a list like structure with level, which is a kind of two dimensional infinite array.
|
|
|
459
|
|
|
460 data OrdinalD {n : Level} : (lv : Nat) → Set n where
|
|
|
461 Φ : (lv : Nat) → OrdinalD lv
|
|
|
462 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
|
|
|
463
|
|
|
464 The order of the OrdinalD can be defined in this way.
|
|
|
465
|
|
|
466 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where
|
|
|
467 Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x
|
|
|
468 s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y
|
|
|
469
|
|
|
470 This is a simple data structure, it has no abstract assumptions, and it is countable many data
|
|
|
471 structure.
|
|
|
472
|
|
|
473 Φ 0
|
|
|
474 OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2)))
|
|
|
475 Osuc 0 (Φ 0) d< Φ 1
|
|
|
476
|
|
|
477 --Model of Ordinals
|
|
|
478
|
|
|
479 It is easy to show OrdinalD and its order satisfies the axioms of Ordinals.
|
|
|
480
|
|
|
481 So our Ordinals has a mode. This means axiom of Ordinals are consistent.
|
|
|
482
|
|
|
483 --Debugging axioms using Model
|
|
|
484
|
|
|
485 Whether axiom is correct or not can be checked by a validity on a mode.
|
|
|
486
|
|
|
487 If not, we may fix the axioms or the model, such as the definitions of the order.
|
|
|
488
|
|
|
489 We can also ask whether the inputs exist.
|
|
|
490
|
|
|
491 --Countable Ordinals can contains uncountable set?
|
|
|
492
|
|
|
493 Yes, the ordinals contains any level of infinite Set in the axioms.
|
|
|
494
|
|
|
495 If we handle real-number in the model, only countable number of real-number is used.
|
|
|
496
|
|
|
497 from the outside view point, it is countable
|
|
|
498 from the internal view point, it is uncountable
|
|
|
499
|
|
|
500 The definition of countable/uncountable is the same, but the properties are different
|
|
|
501 depending on the context.
|
|
|
502
|
|
|
503 We don't show the definition of cardinal number here.
|
|
|
504
|
|
|
505 --What is Set
|
|
|
506
|
|
|
507 The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?).
|
|
|
508
|
|
|
509 From naive point view, a set i a list, but in Agda, elements have all the same type.
|
|
|
510 A set in ZF may contain other Sets in ZF, which not easy to implement it as a list.
|
|
|
511
|
|
|
512 Finite set may be written in finite series of ∨, but ...
|
|
|
513
|
|
|
514 --We don't ask the contents of Set. It can be anything.
|
|
|
515
|
|
|
516 From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on,
|
|
|
517 and all of them, and again we repeat this.
|
|
|
518
|
|
|
519 φ {φ} {φ,{φ}}, {φ,{φ},...}
|
|
|
520
|
|
|
521 It is called V.
|
|
|
522
|
|
|
523 This operation can be performed within a ZF Set theory. Classical Set Theory assumes
|
|
|
524 ZF, so this kind of thing is allowed.
|
|
|
525
|
|
|
526 But in our case, we have no ZF theory, so we are going to use Ordinals.
|
|
|
527
|
|
|
528
|
|
|
529 --Ordinal Definable Set
|
|
|
530
|
|
|
531 We can define a sbuset of Ordinals using predicates. What is a subset?
|
|
|
532
|
|
|
533 a predicate has an Ordinal argument
|
|
|
534
|
|
|
535 is an Ordinal Definable Set (OD). In Agda, OD is defined as follows.
|
|
|
536
|
|
|
537 record OD : Set (suc n ) where
|
|
|
538 field
|
|
|
539 def : (x : Ordinal ) → Set n
|
|
|
540
|
|
|
541 Ordinals itself is not a set in a ZF Set theory but a class. In OD,
|
|
|
542
|
|
|
543 record { def = λ x → true }
|
|
|
544
|
|
|
545 means Ordinals itself, so ODs are larger than a notion of ZF Set Theory,
|
|
|
546 but we don't care about it.
|
|
|
547
|
|
|
548
|
|
|
549 --∋ in OD
|
|
|
550
|
|
|
551 OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping
|
|
|
552
|
|
|
553 od→ord : OD → Ordinal
|
|
|
554
|
|
|
555 we may check an OD is an element of the OD using def.
|
|
|
556
|
|
|
557 A ∋ x can be define as follows.
|
|
|
558
|
|
|
559 _∋_ : ( A x : OD ) → Set n
|
|
|
560 _∋_ A x = def A ( od→ord x )
|
|
|
561
|
|
|
562 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then
|
|
|
563
|
|
|
564 A x = def A ( od→ord x ) = ψ (od→ord x)
|
|
|
565
|
|
|
566 --1 to 1 mapping between an OD and an Ordinal
|
|
|
567
|
|
|
568 od→ord : OD → Ordinal
|
|
|
569 ord→od : Ordinal → OD
|
|
|
570 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
|
|
|
571 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
|
|
|
572
|
|
|
573 They say the existing of the mappings can be proved in Classical Set Theory, but we
|
|
|
574 simply assumes these non constructively.
|
|
|
575
|
|
|
576 We use postulate, it may contains additional restrictions which are not clear now.
|
|
|
577 It look like the mapping should be a subset of Ordinals, but we don't explicitly
|
|
|
578 state it.
|
|
|
579
|
|
|
580 <center><img src="fig/ord-od-mapping.svg"></center>
|
|
|
581
|
|
|
582 --Order preserving in the mapping of OD and Ordinal
|
|
|
583
|
|
|
584 Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ).
|
|
|
585
|
|
|
586 def y ( od→ord x )
|
|
|
587
|
|
|
588 An elements of OD should be defined before the OD, that is, an ordinal corresponding an elements
|
|
|
589 have to be smaller than the corresponding ordinal of the containing OD.
|
|
|
590
|
|
|
591 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
|
|
|
592
|
|
|
593 This is also said to be provable in classical Set Theory, but we simply assumes it.
|
|
|
594
|
|
|
595 OD has an order based on the corresponding ordinal, but it may not have corresponding def / ∋
|
|
|
596 relation. This means the reverse order preservation,
|
|
|
597
|
|
|
598 o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x
|
|
|
599
|
|
|
600 is not valid. If we assumes it, ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in
|
|
|
601 the model.
|
|
|
602
|
|
|
603 <center><img src="fig/ODandOrdinals.svg"></center>
|
|
|
604
|
|
|
605 --ISO
|
|
|
606
|
|
|
607 It also requires isomorphisms,
|
|
|
608
|
|
|
609 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
|
|
|
610 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
|
|
|
611
|
|
|
612
|
|
|
613 --Various Sets
|
|
|
614
|
|
|
615 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
|
|
|
616
|
|
|
617 Ordinal / things satisfies axiom of Ordinal / extension of natural number
|
|
|
618 V / hierarchical construction of Set from φ
|
|
|
619 L / hierarchical predicate definable construction of Set from φ
|
|
|
620 OD / equational formula on Ordinals
|
|
|
621 Agda Set / Type / it also has a level
|
|
|
622
|
|
|
623
|
|
|
624 --Fixes on ZF to intuitionistic logic
|
|
|
625
|
|
|
626 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
|
|
|
627 ZF axioms in Agda.
|
|
|
628
|
|
|
629 It may not valid in our model. We have to debug it.
|
|
|
630
|
|
|
631 Fixes are depends on axioms.
|
|
|
632
|
|
|
633 <center><img src="fig/axiom-type.svg"></center>
|
|
|
634
|
|
|
635 <a href="fig/zf-record.html">
|
|
|
636 ZFのrecord
|
|
|
637 </a>
|
|
|
638
|
|
|
639 --Pure logical axioms
|
|
|
640
|
|
279
|
641 empty, pair, select, ε-induction??infinity
|
|
273
|
642
|
|
|
643 These are logical relations among OD.
|
|
|
644
|
|
|
645 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
|
|
|
646 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
|
|
|
647 pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
|
|
|
648 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
|
|
|
649 infinity∅ : ∅ ∈ infinite
|
|
|
650 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ( x , x ) ) ∈ infinite
|
|
|
651 ε-induction : { ψ : OD → Set (suc n)}
|
|
|
652 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
|
|
|
653 → (x : OD ) → ψ x
|
|
|
654
|
|
|
655 finitely can be define by Agda data.
|
|
|
656
|
|
|
657 data infinite-d : ( x : Ordinal ) → Set n where
|
|
|
658 iφ : infinite-d o∅
|
|
|
659 isuc : {x : Ordinal } → infinite-d x →
|
|
|
660 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
|
|
|
661
|
|
|
662 Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model.
|
|
|
663
|
|
|
664 --Axiom of Pair
|
|
|
665
|
|
|
666 In the Tanaka's book, axiom of pair is as follows.
|
|
|
667
|
|
|
668 ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y)
|
|
|
669
|
|
|
670 We have fix ∃ z, a function (x , y) is defined, which is _,_ .
|
|
|
671
|
|
|
672 _,_ : ( A B : ZFSet ) → ZFSet
|
|
|
673
|
|
|
674 using this, we can define two directions in separates axioms, like this.
|
|
|
675
|
|
|
676 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
|
|
|
677 pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
|
|
|
678
|
|
|
679 This is already written in Agda, so we use these as axioms. All inputs have ∀.
|
|
|
680
|
|
|
681 --pair in OD
|
|
|
682
|
|
|
683 OD is an equation on Ordinals, we can simply write axiom of pair in the OD.
|
|
|
684
|
|
|
685 _,_ : OD → OD → OD
|
|
|
686 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) }
|
|
|
687
|
|
|
688 ≡ is an equality of λ terms, but please not that this is equality on Ordinals.
|
|
|
689
|
|
|
690 --Validity of Axiom of Pair
|
|
|
691
|
|
|
692 Assuming ZFSet is OD, we are going to prove pair→ .
|
|
|
693
|
|
|
694 pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y )
|
|
|
695 pair→ x y t p = ?
|
|
|
696
|
|
|
697 In this program, type of p is ( x , y ) ∋ t , that is
|
|
|
698 def ( x , y ) that is, (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) .
|
|
|
699
|
|
|
700 Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ).
|
|
|
701
|
|
|
702 pair→ x y t (case1 t≡x ) = ?
|
|
|
703 pair→ x y t (case2 t≡y ) = ?
|
|
|
704
|
|
|
705 The type of the ? is ( t == x ) ∨ ( t == y ), again it is data _∨_ .
|
|
|
706
|
|
|
707 pair→ x y t (case1 t≡x ) = case1 ?
|
|
|
708 pair→ x y t (case2 t≡y ) = case2 ?
|
|
|
709
|
|
|
710 The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable
|
|
|
711 which type is
|
|
|
712
|
|
|
713 t≡x : od→ord t ≡ od→ord x
|
|
|
714
|
|
|
715 which is shown by an Agda command (C-C C-E : agda2-show-context ).
|
|
|
716
|
|
|
717 But we haven't defined == yet.
|
|
|
718
|
|
|
719 --Equality of OD and Axiom of Extensionality
|
|
|
720
|
|
|
721 OD is defined by a predicates, if we compares normal form of the predicates, even if
|
|
|
722 it contains the same elements, it may be different, which is no good as an equality of
|
|
|
723 Sets.
|
|
|
724
|
|
|
725 Axiom of Extensionality requires sets having the same elements are handled in the same way
|
|
|
726 each other.
|
|
|
727
|
|
|
728 ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
|
|
|
729
|
|
|
730 We can write this axiom in Agda as follows.
|
|
|
731
|
|
|
732 extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w )
|
|
|
733
|
|
|
734 So we use ( A ∋ z ) ⇔ (B ∋ z) as an equality (_==_) of our model. We have to show
|
|
|
735 A ∈ w ⇔ B ∈ w from A == B.
|
|
|
736
|
|
|
737 x == y can be defined in this way.
|
|
|
738
|
|
|
739 record _==_ ( a b : OD ) : Set n where
|
|
|
740 field
|
|
|
741 eq→ : ∀ { x : Ordinal } → def a x → def b x
|
|
|
742 eq← : ∀ { x : Ordinal } → def b x → def a x
|
|
|
743
|
|
|
744 Actually, (z : OD) → (A ∋ z) ⇔ (B ∋ z) implies A == B.
|
|
|
745
|
|
|
746 extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
|
|
|
747 eq→ (extensionality0 {A} {B} eq ) {x} d = ?
|
|
|
748 eq← (extensionality0 {A} {B} eq ) {x} d = ?
|
|
|
749
|
|
|
750 ? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) .
|
|
|
751
|
|
|
752 Actual proof is rather complicated.
|
|
|
753
|
|
|
754 eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
|
|
|
755 eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
|
|
|
756
|
|
|
757 where
|
|
|
758
|
|
|
759 def-iso : {A B : OD } {x y : Ordinal } → x ≡ y → (def A y → def B y) → def A x → def B x
|
|
|
760 def-iso refl t = t
|
|
|
761
|
|
|
762 --Validity of Axiom of Extensionality
|
|
|
763
|
|
|
764 If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible,
|
|
|
765 so we assumes
|
|
|
766
|
|
|
767 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
|
|
|
768
|
|
|
769 Using this, we have
|
|
|
770
|
|
|
771 extensionality : {A B w : OD } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
|
|
|
772 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
|
|
|
773 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
|
|
|
774
|
|
|
775 This assumption means we may have an equivalence set on any predicates.
|
|
|
776
|
|
|
777 --Non constructive assumptions so far
|
|
|
778
|
|
|
779 We have correspondence between OD and Ordinals and one directional order preserving.
|
|
|
780
|
|
|
781 We also have equality assumption.
|
|
|
782
|
|
|
783 od→ord : OD → Ordinal
|
|
|
784 ord→od : Ordinal → OD
|
|
|
785 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
|
|
|
786 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
|
|
|
787 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
|
|
|
788 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
|
|
|
789
|
|
|
790
|
|
|
791 --Axiom which have negation form
|
|
|
792
|
|
|
793 Union, Selection
|
|
|
794
|
|
|
795 These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )).
|
|
|
796
|
|
|
797 Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive.
|
|
|
798
|
|
|
799 Power Set axiom requires double negation,
|
|
|
800
|
|
|
801 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x )
|
|
|
802 power← : ∀( A t : ZFSet ) → t ⊆_ A → Power A ∋ t
|
|
|
803
|
|
|
804 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form.
|
|
|
805
|
|
|
806 --Union
|
|
|
807
|
|
|
808 The original form of the Axiom of Union is
|
|
|
809
|
|
|
810 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
|
|
|
811
|
|
|
812 Union requires the existence of b in a ⊇ ∃ b ∋ x . We will use negation form of ∃.
|
|
|
813
|
|
|
814 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
|
|
|
815 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
|
|
|
816
|
|
|
817 The definition of Union in OD is like this.
|
|
|
818
|
|
|
819 Union : OD → OD
|
|
|
820 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
|
|
|
821
|
|
|
822 Proof of validity is straight forward.
|
|
|
823
|
|
|
824 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
|
|
|
825 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
|
|
|
826 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
|
|
|
827 union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
|
|
|
828 union← X z UX∋z = FExists _ lemma UX∋z where
|
|
|
829 lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
|
|
|
830 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
|
|
|
831
|
|
|
832 where
|
|
|
833
|
|
|
834 FExists : {m l : Level} → ( ψ : Ordinal → Set m )
|
|
|
835 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
|
|
|
836 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
|
|
|
837 → ¬ p
|
|
|
838 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
|
|
|
839
|
|
|
840 which checks existence using contra-position.
|
|
|
841
|
|
|
842 --Axiom of replacement
|
|
|
843
|
|
|
844 We can replace the elements of a set by a function and it becomes a set. From the book,
|
|
|
845
|
|
|
846 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
|
|
|
847
|
|
|
848 The existential quantifier can be related by a function,
|
|
|
849
|
|
|
850 Replace : OD → (OD → OD ) → OD
|
|
|
851
|
|
|
852 The axioms becomes as follows.
|
|
|
853
|
|
|
854 replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ
|
|
|
855 replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) )
|
|
|
856
|
|
|
857 In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has
|
|
|
858 negation form of existential quantifier in the definition.
|
|
|
859
|
|
|
860 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD
|
|
|
861 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
|
|
|
862
|
|
|
863 Besides this upper bounds is required.
|
|
|
864
|
|
|
865 Replace : OD → (OD → OD ) → OD
|
|
|
866 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
|
|
|
867
|
|
|
868 We omit the proof of the validity, but it is rather straight forward.
|
|
|
869
|
|
|
870 --Validity of Power Set Axiom
|
|
|
871
|
|
|
872 The original Power Set Axiom is this.
|
|
|
873
|
|
|
874 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
|
|
|
875
|
|
|
876 The existential quantifier is replaced by a function
|
|
|
877
|
|
|
878 Power : ( A : OD ) → OD
|
|
|
879
|
|
|
880 t ⊆ X is a record like this.
|
|
|
881
|
|
|
882 record _⊆_ ( A B : OD ) : Set (suc n) where
|
|
|
883 field
|
|
|
884 incl : { x : OD } → A ∋ x → B ∋ x
|
|
|
885
|
|
|
886 Axiom becomes likes this.
|
|
|
887
|
|
|
888 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
|
|
|
889 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
|
|
|
890
|
|
|
891 The validity of the axioms are slight complicated, we have to define set of all subset. We define
|
|
|
892 subset in a different form.
|
|
|
893
|
|
|
894 ZFSubset : (A x : OD ) → OD
|
|
|
895 ZFSubset A x = record { def = λ y → def A y ∧ def x y }
|
|
|
896
|
|
|
897 We can prove,
|
|
|
898
|
|
|
899 ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A )
|
|
|
900
|
|
|
901 We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals,
|
|
|
902 which is an Ordinals with our Model.
|
|
|
903
|
|
|
904 Ord : ( a : Ordinal ) → OD
|
|
|
905 Ord a = record { def = λ y → y o< a }
|
|
|
906
|
|
|
907 Def : (A : OD ) → OD
|
|
|
908 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
|
|
|
909
|
|
|
910 This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty).
|
|
|
911
|
|
|
912 Power : OD → OD
|
|
|
913 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
|
|
|
914
|
|
|
915 Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this.
|
|
|
916
|
|
|
917 ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
|
|
|
918
|
|
|
919 In case of Ord a intro of Power Set axiom becomes valid.
|
|
|
920
|
|
|
921 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
|
|
|
922
|
|
|
923 Using this, we can prove,
|
|
|
924
|
|
|
925 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
|
|
|
926 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
|
|
|
927
|
|
|
928
|
|
|
929 --Axiom of regularity, Axiom of choice, ε-induction
|
|
|
930
|
|
|
931 Axiom of regularity requires non self intersectable elements (which is called minimum), if we
|
|
|
932 replace it by a function, it becomes a choice function. It makes axiom of choice valid.
|
|
|
933
|
|
|
934 This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of
|
|
|
935 choice also becomes valid.
|
|
|
936
|
|
|
937 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
|
|
|
938 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
|
|
|
939 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
|
|
|
940
|
|
|
941 We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set).
|
|
|
942 Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet.
|
|
|
943
|
|
|
944 ε-induction : { ψ : OD → Set (suc n)}
|
|
|
945 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
|
|
|
946 → (x : OD ) → ψ x
|
|
|
947
|
|
|
948 In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals.
|
|
|
949
|
|
|
950 The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia.
|
|
|
951
|
|
|
952 ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
|
|
|
953
|
|
|
954 We can formulate like this.
|
|
|
955
|
|
|
956 choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
|
|
|
957 choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
|
|
|
958
|
|
|
959 It does not requires ∅ ∉ X .
|
|
|
960
|
|
|
961 --Axiom of choice and Law of Excluded Middle
|
|
|
962
|
|
|
963 In our model, since OD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid,
|
|
|
964 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice,
|
|
|
965 but it requires law of the exclude middle.
|
|
|
966
|
|
|
967 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can
|
|
|
968 perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the
|
|
|
969 set is empty or not if we have an axiom of choice, so we have the law of the exclude middle p ∨ ( ¬ p ) .
|
|
|
970
|
|
|
971 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p
|
|
|
972 ppp {p} {a} d = d
|
|
|
973
|
|
|
974 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice
|
|
|
975 and Law of Excluded Middle is equivalent in our mode.
|
|
|
976
|
|
|
977 --Relation-ship among ZF axiom
|
|
|
978
|
|
|
979 <center><img src="fig/axiom-dependency.svg"></center>
|
|
|
980
|
|
|
981 --Non constructive assumption in our model
|
|
|
982
|
|
|
983 mapping between OD and Ordinals
|
|
|
984
|
|
|
985 od→ord : OD → Ordinal
|
|
|
986 ord→od : Ordinal → OD
|
|
|
987 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
|
|
|
988 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
|
|
|
989 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
|
|
|
990
|
|
|
991 Equivalence on OD
|
|
|
992
|
|
|
993 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
|
|
|
994
|
|
|
995 Upper bound
|
|
|
996
|
|
|
997 sup-o : ( Ordinal → Ordinal ) → Ordinal
|
|
|
998 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ
|
|
|
999
|
|
|
1000 Axiom of choice and strong axiom of regularity.
|
|
|
1001
|
|
|
1002 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
|
|
|
1003 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
|
|
|
1004 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
|
|
|
1005
|
|
|
1006 --So it this correct?
|
|
|
1007
|
|
|
1008 Our axiom are syntactically the same in the text book, but negations are slightly different.
|
|
|
1009
|
|
|
1010 If we assumes excluded middle, these are exactly same.
|
|
|
1011
|
|
|
1012 Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it.
|
|
|
1013
|
|
|
1014 Except the upper bound, axioms are simple logical relation.
|
|
|
1015
|
|
|
1016 Proof of existence of mapping between OD and Ordinals are not obvious. We don't know we prove it or not.
|
|
|
1017
|
|
|
1018 Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts,
|
|
|
1019 but we don't have explicit upper limit on Ordinals.
|
|
|
1020
|
|
|
1021 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct.
|
|
|
1022
|
|
|
1023 --How to use Agda Set Theory
|
|
|
1024
|
|
|
1025 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be
|
|
|
1026 postulated or assuming law of excluded middle.
|
|
|
1027
|
|
|
1028 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check
|
|
|
1029 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory.
|
|
|
1030
|
|
|
1031 ZF record itself is not necessary, for example, topology theory without ZF can be possible.
|
|
|
1032
|
|
|
1033 --Topos and Set Theory
|
|
|
1034
|
|
|
1035 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a
|
|
|
1036 sub-object classifier.
|
|
|
1037
|
|
|
1038 Topos itself is model of intuitionistic logic.
|
|
|
1039
|
|
|
1040 Transitive Sets are objects of Cartesian closed category.
|
|
|
1041 It is possible to introduce Power Set Functor on it
|
|
|
1042
|
|
|
1043 We can use replacement A ∩ x for each element in Transitive Set,
|
|
|
1044 in the similar way of our power set axiom. I
|
|
|
1045
|
|
|
1046 A model of ZF Set theory can be constructed on top of the Topos which is shown in Oisus.
|
|
|
1047
|
|
|
1048 Our Agda model is a proof theoretic version of it.
|
|
|
1049
|
|
|
1050 --Cardinal number and Continuum hypothesis
|
|
|
1051
|
|
|
1052 Axiom of choice is required to define cardinal number
|
|
|
1053
|
|
|
1054 definition of cardinal number is not yet done
|
|
|
1055
|
|
|
1056 definition of filter is not yet done
|
|
|
1057
|
|
|
1058 we may have a model without axiom of choice or without continuum hypothesis
|
|
|
1059
|
|
|
1060 Possible representation of continuum hypothesis is this.
|
|
|
1061
|
|
|
1062 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
|
|
|
1063
|
|
|
1064 --Filter
|
|
|
1065
|
|
|
1066 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
|
|
|
1067 is depends on axiom of choice.
|
|
|
1068
|
|
|
1069 record Filter ( L : OD ) : Set (suc n) where
|
|
|
1070 field
|
|
|
1071 filter : OD
|
|
|
1072 proper : ¬ ( filter ∋ od∅ )
|
|
|
1073 inL : filter ⊆ L
|
|
|
1074 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
|
|
|
1075 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
|
|
|
1076
|
|
|
1077 We may construct a model of non standard analysis or set theory.
|
|
|
1078
|
|
|
1079 This may be simpler than classical forcing theory ( not yet done).
|
|
|
1080
|
|
|
1081 --Programming Mathematics
|
|
|
1082
|
|
|
1083 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
|
|
|
1084 structure are
|
|
|
1085
|
|
|
1086 record and data
|
|
|
1087
|
|
|
1088 Proof is check by type consistency not by the computation, but it may include some normalization.
|
|
|
1089
|
|
|
1090 Type inference and termination is not so clear in multi recursions.
|
|
|
1091
|
|
|
1092 Defining Agda record is a good way to understand mathematical theory, for examples,
|
|
|
1093
|
|
|
1094 Category theory ( Yoneda lemma, Floyd Adjunction functor theorem, Applicative functor )
|
|
|
1095 Automaton ( Subset construction、Language containment)
|
|
|
1096
|
|
|
1097 are proved in Agda.
|
|
|
1098
|
|
|
1099 --link
|
|
|
1100
|
|
|
1101 Summer school of foundation of mathematics (in Japanese)
|
|
|
1102 <br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/">
|
|
|
1103 https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/
|
|
|
1104 </a>
|
|
|
1105
|
|
|
1106 Foundation of axiomatic set theory (in Japanese)
|
|
|
1107 <br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf">
|
|
|
1108 https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf
|
|
|
1109 </a>
|
|
|
1110
|
|
|
1111 Agda
|
|
|
1112 <br> <a href="https://agda.readthedocs.io/en/v2.6.0.1/">
|
|
|
1113 https://agda.readthedocs.io/en/v2.6.0.1/
|
|
|
1114 </a>
|
|
|
1115
|
|
|
1116 ZF-in-Agda source
|
|
|
1117 <br> <a href="https://github.com/shinji-kono/zf-in-agda.git">
|
|
|
1118 https://github.com/shinji-kono/zf-in-agda.git
|
|
|
1119 </a>
|
|
|
1120
|
|
|
1121 Category theory in Agda source
|
|
|
1122 <br> <a href="https://github.com/shinji-kono/category-exercise-in-agda">
|
|
|
1123 https://github.com/shinji-kono/category-exercise-in-agda
|
|
|
1124 </a>
|
|
|
1125
|
|
|
1126
|
|
|
1127
|
