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

comparison zf-in-agda.html @ 273:9ccf8514c323

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add documents
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Jan 2020 20:11:51 +0900
parents
children 197e0b3d39dc
comparison
equal deleted inserted replaced
272:985a1af11bce 273:9ccf8514c323
1 <html>
2 <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=UTF-8">
3 <head>
4 <STYLE type="text/css">
5 .main { width:100%; }
6 .side { top:0px; width:0%; position:fixed; left:80%; display:none}
7 </STYLE>
8 <script type="text/javascript">
9 function showElement(layer){
10 var myLayer = document.getElementById(layer);
11 var main = document.getElementById('mmm');
12 if(myLayer.style.display=="none"){
13 myLayer.style.width="20%";
14 main.style.width="80%";
15 myLayer.style.display="block";
16 myLayer.backgroundPosition="top";
17 } else {
18 myLayer.style.width="0%";
19 main.style.width="100%";
20 myLayer.style.display="none";
21 }
22 }
23 </script>
24 <title>Constructing ZF Set Theory in Agda </title>
25 </head>
26 <body>
27 <div class="main" id="mmm">
28 <h1>Constructing ZF Set Theory in Agda </h1>
29 <a href="#" right="0px" onclick="javascript:showElement('menu')">
30 <span>Menu</span>
31 </a>
32 <a href="#" left="0px" onclick="javascript:showElement('menu')">
33 <span>Menu</span>
34 </a>
35
36 <p>
37
38 <author> Shinji KONO</author>
39
40 <hr/>
41 <h2><a name="content000">Programming Mathematics</a></h2>
42 Programming is processing data structure with λ terms.
43 <p>
44 We are going to handle Mathematics in intuitionistic logic with λ terms.
45 <p>
46 Mathematics is a functional programming which values are proofs.
47 <p>
48 Programming ZF Set Theory in Agda
49 <p>
50
51 <hr/>
52 <h2><a name="content001">Target</a></h2>
53
54 <pre>
55 Describe ZF axioms in Agda
56 Construction a Model of ZF Set Theory in Agda
57 Show necessary assumptions for the model
58 Show validities of ZF axioms on the model
59
60 </pre>
61 This shows consistency of Set Theory (with some assumptions),
62 without circulating ZF Theory assumption.
63 <p>
64 <a href="https://github.com/shinji-kono/zf-in-agda">
65 ZF in Agda https://github.com/shinji-kono/zf-in-agda
66 </a>
67 <p>
68
69 <hr/>
70 <h2><a name="content002">Why Set Theory</a></h2>
71 If we can formulate Set theory, it suppose to work on any mathematical theory.
72 <p>
73 Set Theory is a difficult point for beginners especially axiom of choice.
74 <p>
75 It has some amount of difficulty and self circulating discussion.
76 <p>
77 I'm planning to do it in my old age, but I'm enough age now.
78 <p>
79 This is done during from May to September.
80 <p>
81
82 <hr/>
83 <h2><a name="content003">Agda and Intuitionistic Logic </a></h2>
84 Curry Howard Isomorphism
85 <p>
86
87 <pre>
88 Proposition : Proof ⇔ Type : Value
89
90 </pre>
91 which means
92 <p>
93 　　constructing a typed lambda calculus which corresponds a logic
94 <p>
95 Typed lambda calculus which allows complex type as a value of a variable (System FC)
96 <p>
97 　　First class Type / Dependent Type
98 <p>
99 Agda is a such a programming language which has similar syntax of Haskell
100 <p>
101 Coq is specialized in proof assistance such as command and tactics .
102 <p>
103
104 <hr/>
105 <h2><a name="content004">Introduction of Agda </a></h2>
106 A length of a list of type A.
107 <p>
108
109 <pre>
110 length : {A : Set } → List A → Nat
111 length [] = zero
112 length (_ ∷ t) = suc ( length t )
113
114 </pre>
115 Simple functional programming language. Type declaration is mandatory.
116 A colon means type, an equal means value. Indentation based.
117 <p>
118 Set is a base type (which may have a level ).
119 <p>
120 {} means implicit variable which can be omitted if Agda infers its value.
121 <p>
122
123 <hr/>
124 <h2><a name="content005">data ( Sum type )</a></h2>
125 A data type which as exclusive multiple constructors. A similar one as
126 union in C or case class in Scala.
127 <p>
128 It has a similar syntax as Haskell but it has a slight difference.
129 <p>
130
131 <pre>
132 data List (A : Set ) : Set where
133 [] : List A
134 _∷_ : A → List A → List A
135
136 </pre>
137 _∷_ means infix operator. If use explicit _, it can be used in a normal function
138 syntax.
139 <p>
140 Natural number can be defined as a usual way.
141 <p>
142
143 <pre>
144 data Nat : Set where
145 zero : Nat
146 suc : Nat → Nat
147
148 </pre>
149
150 <hr/>
151 <h2><a name="content006"> A → B means "A implies B"</a></h2>
152
153 <p>
154 In Agda, a type can be a value of a variable, which is usually called dependent type.
155 Type has a name Set in Agda.
156 <p>
157
158 <pre>
159 ex3 : {A B : Set} → Set
160 ex3 {A}{B} = A → B
161
162 </pre>
163 ex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B.
164 <p>
165
166 <pre>
167 A type is a formula, the value is the proof
168
169 </pre>
170 A value of A → B can be interpreted as an inference from the formula A to the formula B, which
171 can be a function from a proof of A to a proof of B.
172 <p>
173
174 <hr/>
175 <h2><a name="content007">introduction と elimination</a></h2>
176 For a logical operator, there are two types of inference, an introduction and an elimination.
177 <p>
178
179 <pre>
180 intro creating symbol / constructor / introduction
181 elim using symbolic / accessors / elimination
182
183 </pre>
184 In Natural deduction, this can be written in proof schema.
185 <p>
186
187 <pre>
188 A
189 :
190 B A A → B
191 ------------- →intro ------------------ →elim
192 A → B B
193
194 </pre>
195 In Agda, this is a pair of type and value as follows. Introduction of → uses λ.
196 <p>
197
198 <pre>
199 →intro : {A B : Set } → A → B → ( A → B )
200 →intro _ b = λ x → b
201 →elim : {A B : Set } → A → ( A → B ) → B
202 →elim a f = f a
203
204 </pre>
205 Important
206 <p>
207
208 <pre>
209 {A B : Set } → A → B → ( A → B )
210
211 </pre>
212 is
213 <p>
214
215 <pre>
216 {A B : Set } → ( A → ( B → ( A → B ) ))
217
218 </pre>
219 This makes currying of function easy.
220 <p>
221
222 <hr/>
223 <h2><a name="content008"> To prove A → B </a></h2>
224 Make a left type as an argument. (intros in Coq)
225 <p>
226
227 <pre>
228 ex5 : {A B C : Set } → A → B → C → ?
229 ex5 a b c = ?
230
231 </pre>
232 ? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole.
233 <p>
234 We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red),
235 insufficient proof or instance (Yellow), Non-termination, the proof is completed.
236 <p>
237
238 <hr/>
239 <h2><a name="content009"> A ∧ B</a></h2>
240 Well known conjunction's introduction and elimination is as follow.
241 <p>
242
243 <pre>
244 A B A ∧ B A ∧ B
245 ------------- ----------- proj1 ---------- proj2
246 A ∧ B A B
247
248 </pre>
249 We can introduce a corresponding structure in our functional programming language.
250 <p>
251
252 <hr/>
253 <h2><a name="content010"> record</a></h2>
254
255 <pre>
256 record _∧_ A B : Set
257 field
258 proj1 : A
259 proj2 : B
260
261 </pre>
262 _∧_　means infix operator. _∧_ A B can be written as A ∧ B (Haskell uses (∧) )
263 <p>
264 This a type which constructed from type A and type B. You may think this as an object
265 or struct.
266 <p>
267
268 <pre>
269 record { proj1 = x ; proj2 = y }
270
271 </pre>
272 is a constructor of _∧_.
273 <p>
274
275 <pre>
276 ex3 : {A B : Set} → A → B → ( A ∧ B )
277 ex3 a b = record { proj1 = a ; proj2 = b }
278 ex1 : {A B : Set} → ( A ∧ B ) → A
279 ex1 a∧b = proj1 a∧b
280
281 </pre>
282 a∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols
283 except parenthesis or colons. A symbol requires space separation such as a type defining colon.
284 <p>
285 Defining record can be recursively, but we don't use the recursion here.
286 <p>
287
288 <hr/>
289 <h2><a name="content011"> Mathematical structure</a></h2>
290 We have types of elements and the relationship in a mathematical structure.
291 <p>
292
293 <pre>
294 logical relation has no ordering
295 there is a natural ordering in arguments and a value in a function
296
297 </pre>
298 So we have typical definition style of mathematical structure with records.
299 <p>
300
301 <pre>
302 record IsOrdinals {n : Level} (ord : Set n)
303 (_o&lt;_ : ord → ord → Set n) : Set (suc (suc n)) where
304 field
305 Otrans : {x y z : ord } → x o&lt; y → y o&lt; z → x o&lt; z
306 record Ordinals {n : Level} : Set (suc (suc n)) where
307 field
308 ord : Set n
309 _o&lt;_ : ord → ord → Set n
310 isOrdinal : IsOrdinals ord _o&lt;_
311
312 </pre>
313 In IsOrdinals, axioms are written in flat way. In Ordinal, we may have
314 inputs and outputs are put in the field including IsOrdinal.
315 <p>
316 Fields of Ordinal is existential objects in the mathematical structure.
317 <p>
318
319 <hr/>
320 <h2><a name="content012"> A Model and a theory</a></h2>
321 Agda record is a type, so we can write it in the argument, but is it really exists?
322 <p>
323 If we have a value of the record, it simply exists, that is, we need to create all the existence
324 in the record satisfies all the axioms (= field of IsOrdinal) should be valid.
325 <p>
326
327 <pre>
328 type of record = theory
329 value of record = model
330
331 </pre>
332 We call the value of the record as a model. If mathematical structure has a
333 model, it exists. Pretty Obvious.
334 <p>
335
336 <hr/>
337 <h2><a name="content013"> postulate と module</a></h2>
338 Agda proofs are separated by modules, which are large records.
339 <p>
340 postulates are assumptions. We can assume a type without proofs.
341 <p>
342
343 <pre>
344 postulate
345 sup-o : ( Ordinal → Ordinal ) → Ordinal
346 sup-o&lt; : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o&lt; sup-o ψ
347
348 </pre>
349 sup-o is an example of upper bound of a function and sup-o&lt; assumes it actually satisfies all the value is less than upper bound.
350 <p>
351 Writing some type in a module argument is the same as postulating a type, but
352 postulate can be written the middle of a proof.
353 <p>
354 postulate can be constructive.
355 <p>
356 postulate can be inconsistent, which result everything has a proof.
357 <p>
358
359 <hr/>
360 <h2><a name="content014"> A ∨ B</a></h2>
361
362 <pre>
363 data _∨_ (A B : Set) : Set where
364 case1 : A → A ∨ B
365 case2 : B → A ∨ B
366
367 </pre>
368 As Haskell, case1/case2 are patterns.
369 <p>
370
371 <pre>
372 ex3 : {A B : Set} → ( A ∨ A ) → A
373 ex3 = ?
374
375 </pre>
376 In a case statement, Agda command C-C C-C generates possible cases in the head.
377 <p>
378
379 <pre>
380 ex3 : {A B : Set} → ( A ∨ A ) → A
381 ex3 (case1 x) = ?
382 ex3 (case2 x) = ?
383
384 </pre>
385 Proof schema of ∨ is omit due to the complexity.
386 <p>
387
388 <hr/>
389 <h2><a name="content015"> Negation</a></h2>
390
391 <pre>
392 ⊥
393 ------------- ⊥-elim
394 A
395
396 </pre>
397 Anything can be derived from bottom, in this case a Set A. There is no introduction rule
398 in ⊥, which can be implemented as data which has no constructor.
399 <p>
400
401 <pre>
402 data ⊥ : Set where
403
404 </pre>
405 ⊥-elim can be proved like this.
406 <p>
407
408 <pre>
409 ⊥-elim : {A : Set } -&gt; ⊥ -&gt; A
410 ⊥-elim ()
411
412 </pre>
413 () means no match argument nor value.
414 <p>
415 A negation can be defined using ⊥ like this.
416 <p>
417
418 <pre>
419 ¬_ : Set → Set
420 ¬ A = A → ⊥
421
422 </pre>
423
424 <hr/>
425 <h2><a name="content016">Equality </a></h2>
426
427 <p>
428 All the value in Agda are terms. If we have the same normalized form, two terms are equal.
429 If we have variables in the terms, we will perform an unification. unifiable terms are equal.
430 We don't go further on the unification.
431 <p>
432
433 <pre>
434 { x : A } x ≡ y f x y
435 --------------- ≡-intro --------------------- ≡-elim
436 x ≡ x f x x
437
438 </pre>
439 equality _≡_ can be defined as a data.
440 <p>
441
442 <pre>
443 data _≡_ {A : Set } : A → A → Set where
444 refl : {x : A} → x ≡ x
445
446 </pre>
447 The elimination of equality is a substitution in a term.
448 <p>
449
450 <pre>
451 subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y
452 subst {A} {x} {y} f refl fx = fx
453 ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
454 ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y
455
456 </pre>
457
458 <hr/>
459 <h2><a name="content017">Equivalence relation</a></h2>
460
461 <p>
462
463 <pre>
464 refl' : {A : Set} {x : A } → x ≡ x
465 refl' = ?
466 sym : {A : Set} {x y : A } → x ≡ y → y ≡ x
467 sym = ?
468 trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
469 trans = ?
470 cong : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y
471 cong = ?
472
473 </pre>
474
475 <hr/>
476 <h2><a name="content018">Ordering</a></h2>
477
478 <p>
479 Relation is a predicate on two value which has a same type.
480 <p>
481
482 <pre>
483 A → A → Set
484
485 </pre>
486 Defining order is the definition of this type with predicate or a data.
487 <p>
488
489 <pre>
490 data _≤_ : Rel ℕ 0ℓ where
491 z≤n : ∀ {n} → zero ≤ n
492 s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
493
494 </pre>
495
496 <hr/>
497 <h2><a name="content019">Quantifier</a></h2>
498
499 <p>
500 Handling quantifier in an intuitionistic logic requires special cares.
501 <p>
502 In the input of a function, there are no restriction on it, that is, it has
503 a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it)
504 <p>
505 There is no ∃ in agda, the one way is using negation like this.
506 <p>
507 　∃ (x : A ) → p x = ¬ ( ( x : A ) → ¬ ( p x ) )
508 <p>
509 On the another way, f : A can be used like this.
510 <p>
511
512 <pre>
513 p f
514
515 </pre>
516 If we use a function which can be defined globally which has stronger meaning the
517 usage of ∃ x in a logical expression.
518 <p>
519
520 <hr/>
521 <h2><a name="content020">Can we do math in this way?</a></h2>
522 Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support).
523 <p>
524 In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF).
525 <p>
526
527 <pre>
528 define mathematical structure as a record
529 program inferences as if we have proofs in variables
530
531 </pre>
532
533 <hr/>
534 <h2><a name="content021">Things which Agda cannot prove</a></h2>
535
536 <p>
537 The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which
538 leads uniqueness of a functor in Category Theory.
539 <p>
540 Functional extensionality cannot be proved.
541 <pre>
542 (∀ x → f x ≡ g x) → f ≡ g
543
544 </pre>
545 Agda has no law of exclude middle.
546 <p>
547
548 <pre>
549 a ∨ ( ¬ a )
550
551 </pre>
552 For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot.
553 <p>
554 It also other problems such as termination, type inference or unification which we may overcome with
555 efforts or devices or may not.
556 <p>
557 If we cannot prove something, we can safely postulate it unless it leads a contradiction.
558 <pre>
559
560
561 </pre>
562
563 <hr/>
564 <h2><a name="content022">Classical story of ZF Set Theory</a></h2>
565
566 <p>
567 Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads
568 a relative consistency proof of the Set Theory.
569 Ordinal number is used in the flow.
570 <p>
571 In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD).
572 We need some non constructive assumptions in the construction. A model of Set theory is
573 constructed based on these assumptions.
574 <p>
575 <img src="fig/set-theory.svg">
576
577 <p>
578
579 <hr/>
580 <h2><a name="content023">Ordinals</a></h2>
581 Ordinals are our intuition of infinite things, which has ∅ and orders on the things.
582 It also has a successor osuc.
583 <p>
584
585 <pre>
586 record Ordinals {n : Level} : Set (suc (suc n)) where
587 field
588 ord : Set n
589 o∅ : ord
590 osuc : ord → ord
591 _o&lt;_ : ord → ord → Set n
592 isOrdinal : IsOrdinals ord o∅ osuc _o&lt;_
593
594 </pre>
595 It is different from natural numbers in way. The order of Ordinals is not defined in terms
596 of successor. It is given from outside, which make it possible to have higher order infinity.
597 <p>
598
599 <hr/>
600 <h2><a name="content024">Axiom of Ordinals</a></h2>
601 Properties of infinite things. We request a transfinite induction, which states that if
602 some properties are satisfied below all possible ordinals, the properties are true on all
603 ordinals.
604 <p>
605 Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals
606 which is not a successor of any ordinals. It is called limit ordinal.
607 <p>
608 Any two ordinal can be compared, that is less, equal or more, that is total order.
609 <p>
610
611 <pre>
612 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord )
613 (osuc : ord → ord )
614 (_o&lt;_ : ord → ord → Set n) : Set (suc (suc n)) where
615 field
616 Otrans : {x y z : ord } → x o&lt; y → y o&lt; z → x o&lt; z
617 OTri : Trichotomous {n} _≡_ _o&lt;_
618 ¬x&lt;0 : { x : ord } → ¬ ( x o&lt; o∅ )
619 &lt;-osuc : { x : ord } → x o&lt; osuc x
620 osuc-≡&lt; : { a x : ord } → x o&lt; osuc a → (x ≡ a ) ∨ (x o&lt; a)
621 TransFinite : { ψ : ord → Set (suc n) }
622 → ( (x : ord) → ( (y : ord ) → y o&lt; x → ψ y ) → ψ x )
623 → ∀ (x : ord) → ψ x
624
625 </pre>
626
627 <hr/>
628 <h2><a name="content025">Concrete Ordinals</a></h2>
629
630 <p>
631 We can define a list like structure with level, which is a kind of two dimensional infinite array.
632 <p>
633
634 <pre>
635 data OrdinalD {n : Level} : (lv : Nat) → Set n where
636 Φ : (lv : Nat) → OrdinalD lv
637 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
638
639 </pre>
640 The order of the OrdinalD can be defined in this way.
641 <p>
642
643 <pre>
644 data _d&lt;_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where
645 Φ&lt; : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d&lt; OSuc lx x
646 s&lt; : {lx : Nat} → {x y : OrdinalD {n} lx} → x d&lt; y → OSuc lx x d&lt; OSuc lx y
647
648 </pre>
649 This is a simple data structure, it has no abstract assumptions, and it is countable many data
650 structure.
651 <p>
652
653 <pre>
654 Φ 0
655 OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2)))
656 Osuc 0 (Φ 0) d&lt; Φ 1
657
658 </pre>
659
660 <hr/>
661 <h2><a name="content026">Model of Ordinals</a></h2>
662
663 <p>
664 It is easy to show OrdinalD and its order satisfies the axioms of Ordinals.
665 <p>
666 So our Ordinals has a mode. This means axiom of Ordinals are consistent.
667 <p>
668
669 <hr/>
670 <h2><a name="content027">Debugging axioms using Model</a></h2>
671 Whether axiom is correct or not can be checked by a validity on a mode.
672 <p>
673 If not, we may fix the axioms or the model, such as the definitions of the order.
674 <p>
675 We can also ask whether the inputs exist.
676 <p>
677
678 <hr/>
679 <h2><a name="content028">Countable Ordinals can contains uncountable set?</a></h2>
680 Yes, the ordinals contains any level of infinite Set in the axioms.
681 <p>
682 If we handle real-number in the model, only countable number of real-number is used.
683 <p>
684
685 <pre>
686 from the outside view point, it is countable
687 from the internal view point, it is uncountable
688
689 </pre>
690 The definition of countable/uncountable is the same, but the properties are different
691 depending on the context.
692 <p>
693 We don't show the definition of cardinal number here.
694 <p>
695
696 <hr/>
697 <h2><a name="content029">What is Set</a></h2>
698 The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?).
699 <p>
700 From naive point view, a set i a list, but in Agda, elements have all the same type.
701 A set in ZF may contain other Sets in ZF, which not easy to implement it as a list.
702 <p>
703 Finite set may be written in finite series of ∨, but ...
704 <p>
705
706 <hr/>
707 <h2><a name="content030">We don't ask the contents of Set. It can be anything.</a></h2>
708 From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on,
709 and all of them, and again we repeat this.
710 <p>
711
712 <pre>
713 φ {φ} {φ,{φ}}, {φ,{φ},...}
714
715 </pre>
716 It is called V.
717 <p>
718 This operation can be performed within a ZF Set theory. Classical Set Theory assumes
719 ZF, so this kind of thing is allowed.
720 <p>
721 But in our case, we have no ZF theory, so we are going to use Ordinals.
722 <p>
723
724 <hr/>
725 <h2><a name="content031">Ordinal Definable Set</a></h2>
726 We can define a sbuset of Ordinals using predicates. What is a subset?
727 <p>
728
729 <pre>
730 a predicate has an Ordinal argument
731
732 </pre>
733 is an Ordinal Definable Set (OD). In Agda, OD is defined as follows.
734 <p>
735
736 <pre>
737 record OD : Set (suc n ) where
738 field
739 def : (x : Ordinal ) → Set n
740
741 </pre>
742 Ordinals itself is not a set in a ZF Set theory but a class. In OD,
743 <p>
744
745 <pre>
746 record { def = λ x → true }
747
748 </pre>
749 means Ordinals itself, so ODs are larger than a notion of ZF Set Theory,
750 but we don't care about it.
751 <p>
752
753 <hr/>
754 <h2><a name="content032">∋ in OD</a></h2>
755 OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping
756 <p>
757
758 <pre>
759 od→ord : OD → Ordinal
760
761 </pre>
762 we may check an OD is an element of the OD using def.
763 <p>
764 A ∋ x can be define as follows.
765 <p>
766
767 <pre>
768 _∋_ : ( A x : OD ) → Set n
769 _∋_ A x = def A ( od→ord x )
770
771 </pre>
772 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then
773 <p>
774
775 <pre>
776 A x = def A ( od→ord x ) = ψ (od→ord x)
777
778 </pre>
779
780 <hr/>
781 <h2><a name="content033">1 to 1 mapping between an OD and an Ordinal</a></h2>
782
783 <p>
784
785 <pre>
786 od→ord : OD → Ordinal
787 ord→od : Ordinal → OD
788 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
789 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
790
791 </pre>
792 They say the existing of the mappings can be proved in Classical Set Theory, but we
793 simply assumes these non constructively.
794 <p>
795 We use postulate, it may contains additional restrictions which are not clear now. It look like the mapping should be a subset of Ordinals, but we don't explicitly
796 state it.
797 <p>
798 <img src="fig/ord-od-mapping.svg">
799
800 <p>
801
802 <hr/>
803 <h2><a name="content034">Order preserving in the mapping of OD and Ordinal</a></h2>
804 Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ).
805 <p>
806
807 <pre>
808 def y ( od→ord x )
809
810 </pre>
811 An elements of OD should be defined before the OD, that is, an ordinal corresponding an elements
812 have to be smaller than the corresponding ordinal of the containing OD.
813 <p>
814
815 <pre>
816 c&lt;→o&lt; : {x y : OD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y
817
818 </pre>
819 This is also said to be provable in classical Set Theory, but we simply assumes it.
820 <p>
821 OD has an order based on the corresponding ordinal, but it may not have corresponding def / ∋relation. This means the reverse order preservation,
822 <p>
823
824 <pre>
825 o&lt;→c&lt; : {n : Level} {x y : Ordinal } → x o&lt; y → def (ord→od y) x
826
827 </pre>
828 is not valid. If we assumes it, ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in
829 the model.
830 <p>
831 <img src="fig/ODandOrdinals.svg">
832
833 <p>
834
835 <hr/>
836 <h2><a name="content035">ISO</a></h2>
837 It also requires isomorphisms,
838 <p>
839
840 <pre>
841 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
842 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
843
844 </pre>
845
846 <hr/>
847 <h2><a name="content036">Various Sets</a></h2>
848
849 <p>
850 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
851 <p>
852
853 <pre>
854 Ordinal / things satisfies axiom of Ordinal / extension of natural number
855 V / hierarchical construction of Set from φ
856 L / hierarchical predicate definable construction of Set from φ
857 OD / equational formula on Ordinals
858 Agda Set / Type / it also has a level
859
860 </pre>
861
862 <hr/>
863 <h2><a name="content037">Fixes on ZF to intuitionistic logic</a></h2>
864
865 <p>
866 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
867 ZF axioms in Agda.
868 <p>
869 It may not valid in our model. We have to debug it.
870 <p>
871 Fixes are depends on axioms.
872 <p>
873 <img src="fig/axiom-type.svg">
874
875 <p>
876 <a href="fig/zf-record.html">
877 ZFのrecord </a>
878 <p>
879
880 <hr/>
881 <h2><a name="content038">Pure logical axioms</a></h2>
882
883 <pre>
884 empty, pair, select, ε-inductioninfinity
885
886 </pre>
887 These are logical relations among OD.
888 <p>
889
890 <pre>
891 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
892 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
893 pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
894 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
895 infinity∅ : ∅ ∈ infinite
896 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ( x , x ) ) ∈ infinite
897 ε-induction : { ψ : OD → Set (suc n)}
898 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
899 → (x : OD ) → ψ x
900
901 </pre>
902 finitely can be define by Agda data.
903 <p>
904
905 <pre>
906 data infinite-d : ( x : Ordinal ) → Set n where
907 iφ : infinite-d o∅
908 isuc : {x : Ordinal } → infinite-d x →
909 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
910
911 </pre>
912 Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model.
913 <p>
914
915 <hr/>
916 <h2><a name="content039">Axiom of Pair</a></h2>
917 In the Tanaka's book, axiom of pair is as follows.
918 <p>
919
920 <pre>
921 ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y)
922
923 </pre>
924 We have fix ∃ z, a function (x , y) is defined, which is _,_ .
925 <p>
926
927 <pre>
928 _,_ : ( A B : ZFSet ) → ZFSet
929
930 </pre>
931 using this, we can define two directions in separates axioms, like this.
932 <p>
933
934 <pre>
935 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
936 pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
937
938 </pre>
939 This is already written in Agda, so we use these as axioms. All inputs have ∀.
940 <p>
941
942 <hr/>
943 <h2><a name="content040">pair in OD</a></h2>
944 OD is an equation on Ordinals, we can simply write axiom of pair in the OD.
945 <p>
946
947 <pre>
948 _,_ : OD → OD → OD
949 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) }
950
951 </pre>
952 ≡ is an equality of λ terms, but please not that this is equality on Ordinals.
953 <p>
954
955 <hr/>
956 <h2><a name="content041">Validity of Axiom of Pair</a></h2>
957 Assuming ZFSet is OD, we are going to prove pair→ .
958 <p>
959
960 <pre>
961 pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y )
962 pair→ x y t p = ?
963
964 </pre>
965 In this program, type of p is ( x , y ) ∋ t , that is def ( x , y ) that is, (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) .
966 <p>
967 Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ).
968 <p>
969
970 <pre>
971 pair→ x y t (case1 t≡x ) = ?
972 pair→ x y t (case2 t≡y ) = ?
973
974 </pre>
975 The type of the ? is ( t == x ) ∨ ( t == y ), again it is data _∨_ .
976 <p>
977
978 <pre>
979 pair→ x y t (case1 t≡x ) = case1 ?
980 pair→ x y t (case2 t≡y ) = case2 ?
981
982 </pre>
983 The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable
984 which type is
985 <p>
986
987 <pre>
988 t≡x : od→ord t ≡ od→ord x
989
990 </pre>
991 which is shown by an Agda command (C-C C-E : agda2-show-context ).
992 <p>
993 But we haven't defined == yet.
994 <p>
995
996 <hr/>
997 <h2><a name="content042">Equality of OD and Axiom of Extensionality </a></h2>
998 OD is defined by a predicates, if we compares normal form of the predicates, even if
999 it contains the same elements, it may be different, which is no good as an equality of
1000 Sets.
1001 <p>
1002 Axiom of Extensionality requires sets having the same elements are handled in the same way
1003 each other.
1004 <p>
1005
1006 <pre>
1007 ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
1008
1009 </pre>
1010 We can write this axiom in Agda as follows.
1011 <p>
1012
1013 <pre>
1014 extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w )
1015
1016 </pre>
1017 So we use ( A ∋ z ) ⇔ (B ∋ z) as an equality (_==_) of our model. We have to show
1018 A ∈ w ⇔ B ∈ w from A == B.
1019 <p>
1020 x == y can be defined in this way.
1021 <p>
1022
1023 <pre>
1024 record _==_ ( a b : OD ) : Set n where
1025 field
1026 eq→ : ∀ { x : Ordinal } → def a x → def b x
1027 eq← : ∀ { x : Ordinal } → def b x → def a x
1028
1029 </pre>
1030 Actually, (z : OD) → (A ∋ z) ⇔ (B ∋ z) implies A == B.
1031 <p>
1032
1033 <pre>
1034 extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
1035 eq→ (extensionality0 {A} {B} eq ) {x} d = ?
1036 eq← (extensionality0 {A} {B} eq ) {x} d = ?
1037
1038 </pre>
1039 ? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) .
1040 <p>
1041 Actual proof is rather complicated.
1042 <p>
1043
1044 <pre>
1045 eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
1046 eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
1047
1048 </pre>
1049 where
1050 <p>
1051
1052 <pre>
1053 def-iso : {A B : OD } {x y : Ordinal } → x ≡ y → (def A y → def B y) → def A x → def B x
1054 def-iso refl t = t
1055
1056 </pre>
1057
1058 <hr/>
1059 <h2><a name="content043">Validity of Axiom of Extensionality</a></h2>
1060
1061 <p>
1062 If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible, so we assumes
1063 <p>
1064
1065 <pre>
1066 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
1067
1068 </pre>
1069 Using this, we have
1070 <p>
1071
1072 <pre>
1073 extensionality : {A B w : OD } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
1074 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
1075 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
1076
1077 </pre>
1078 This assumption means we may have an equivalence set on any predicates.
1079 <p>
1080
1081 <hr/>
1082 <h2><a name="content044">Non constructive assumptions so far</a></h2>
1083 We have correspondence between OD and Ordinals and one directional order preserving.
1084 <p>
1085 We also have equality assumption.
1086 <p>
1087
1088 <pre>
1089 od→ord : OD → Ordinal
1090 ord→od : Ordinal → OD
1091 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
1092 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
1093 c&lt;→o&lt; : {x y : OD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y
1094 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
1095
1096 </pre>
1097
1098 <hr/>
1099 <h2><a name="content045">Axiom which have negation form</a></h2>
1100
1101 <p>
1102
1103 <pre>
1104 Union, Selection
1105
1106 </pre>
1107 These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )).
1108 <p>
1109 Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive.
1110 <p>
1111 Power Set axiom requires double negation,
1112 <p>
1113
1114 <pre>
1115 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x )
1116 power← : ∀( A t : ZFSet ) → t ⊆_ A → Power A ∋ t
1117
1118 </pre>
1119 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form.
1120 <p>
1121
1122 <hr/>
1123 <h2><a name="content046">Union </a></h2>
1124 The original form of the Axiom of Union is
1125 <p>
1126
1127 <pre>
1128 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
1129
1130 </pre>
1131 Union requires the existence of b in a ⊇ ∃ b ∋ x . We will use negation form of ∃.
1132 <p>
1133
1134 <pre>
1135 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
1136 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
1137
1138 </pre>
1139 The definition of Union in OD is like this.
1140 <p>
1141
1142 <pre>
1143 Union : OD → OD
1144 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
1145
1146 </pre>
1147 Proof of validity is straight forward.
1148 <p>
1149
1150 <pre>
1151 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
1152 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
1153 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
1154 union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
1155 union← X z UX∋z = FExists _ lemma UX∋z where
1156 lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
1157 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
1158
1159 </pre>
1160 where
1161 <p>
1162
1163 <pre>
1164 FExists : {m l : Level} → ( ψ : Ordinal → Set m )
1165 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
1166 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
1167 → ¬ p
1168 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
1169
1170 </pre>
1171 which checks existence using contra-position.
1172 <p>
1173
1174 <hr/>
1175 <h2><a name="content047">Axiom of replacement</a></h2>
1176 We can replace the elements of a set by a function and it becomes a set. From the book,
1177 <p>
1178
1179 <pre>
1180 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
1181
1182 </pre>
1183 The existential quantifier can be related by a function,
1184 <p>
1185
1186 <pre>
1187 Replace : OD → (OD → OD ) → OD
1188
1189 </pre>
1190 The axioms becomes as follows.
1191 <p>
1192
1193 <pre>
1194 replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ
1195 replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) )
1196
1197 </pre>
1198 In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has
1199 negation form of existential quantifier in the definition.
1200 <p>
1201
1202 <pre>
1203 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD
1204 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
1205
1206 </pre>
1207 Besides this upper bounds is required.
1208 <p>
1209
1210 <pre>
1211 Replace : OD → (OD → OD ) → OD
1212 Replace X ψ = record { def = λ x → (x o&lt; sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
1213
1214 </pre>
1215 We omit the proof of the validity, but it is rather straight forward.
1216 <p>
1217
1218 <hr/>
1219 <h2><a name="content048">Validity of Power Set Axiom</a></h2>
1220 The original Power Set Axiom is this.
1221 <p>
1222
1223 <pre>
1224 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
1225
1226 </pre>
1227 The existential quantifier is replaced by a function
1228 <p>
1229
1230 <pre>
1231 Power : ( A : OD ) → OD
1232
1233 </pre>
1234 t ⊆ X is a record like this.
1235 <p>
1236
1237 <pre>
1238 record _⊆_ ( A B : OD ) : Set (suc n) where
1239 field
1240 incl : { x : OD } → A ∋ x → B ∋ x
1241
1242 </pre>
1243 Axiom becomes likes this.
1244 <p>
1245
1246 <pre>
1247 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
1248 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
1249
1250 </pre>
1251 The validity of the axioms are slight complicated, we have to define set of all subset. We define
1252 subset in a different form.
1253 <p>
1254
1255 <pre>
1256 ZFSubset : (A x : OD ) → OD
1257 ZFSubset A x = record { def = λ y → def A y ∧ def x y }
1258
1259 </pre>
1260 We can prove,
1261 <p>
1262
1263 <pre>
1264 ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A )
1265
1266 </pre>
1267 We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals,
1268 which is an Ordinals with our Model.
1269 <p>
1270
1271 <pre>
1272 Ord : ( a : Ordinal ) → OD
1273 Ord a = record { def = λ y → y o&lt; a }
1274 Def : (A : OD ) → OD
1275 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
1276
1277 </pre>
1278 This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty).
1279 <p>
1280
1281 <pre>
1282 Power : OD → OD
1283 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
1284
1285 </pre>
1286 Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this.
1287 <p>
1288
1289 <pre>
1290 ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
1291
1292 </pre>
1293 In case of Ord a intro of Power Set axiom becomes valid.
1294 <p>
1295
1296 <pre>
1297 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
1298
1299 </pre>
1300 Using this, we can prove,
1301 <p>
1302
1303 <pre>
1304 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
1305 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
1306
1307 </pre>
1308
1309 <hr/>
1310 <h2><a name="content049">Axiom of regularity, Axiom of choice, ε-induction</a></h2>
1311
1312 <p>
1313 Axiom of regularity requires non self intersectable elements (which is called minimum), if we
1314 replace it by a function, it becomes a choice function. It makes axiom of choice valid.
1315 <p>
1316 This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of
1317 choice also becomes valid.
1318 <p>
1319
1320 <pre>
1321 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
1322 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
1323 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
1324
1325 </pre>
1326 We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set).
1327 Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet.
1328 <p>
1329
1330 <pre>
1331 ε-induction : { ψ : OD → Set (suc n)}
1332 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
1333 → (x : OD ) → ψ x
1334
1335 </pre>
1336 In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals.
1337 <p>
1338 The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia.
1339 <p>
1340
1341 <pre>
1342 ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
1343
1344 </pre>
1345 We can formulate like this.
1346 <p>
1347
1348 <pre>
1349 choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
1350 choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
1351
1352 </pre>
1353 It does not requires ∅ ∉ X .
1354 <p>
1355
1356 <hr/>
1357 <h2><a name="content050">Axiom of choice and Law of Excluded Middle</a></h2>
1358 In our model, since OD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid,
1359 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice,
1360 but it requires law of the exclude middle.
1361 <p>
1362 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can
1363 perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the
1364 set is empty or not if we have an axiom of choice, so we have the law of the exclude middle p ∨ ( ¬ p ) .
1365 <p>
1366
1367 <pre>
1368 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p
1369 ppp {p} {a} d = d
1370
1371 </pre>
1372 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice
1373 and Law of Excluded Middle is equivalent in our mode.
1374 <p>
1375
1376 <hr/>
1377 <h2><a name="content051">Relation-ship among ZF axiom</a></h2>
1378 <img src="fig/axiom-dependency.svg">
1379
1380 <p>
1381
1382 <hr/>
1383 <h2><a name="content052">Non constructive assumption in our model</a></h2>
1384 mapping between OD and Ordinals
1385 <p>
1386
1387 <pre>
1388 od→ord : OD → Ordinal
1389 ord→od : Ordinal → OD
1390 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
1391 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
1392 c&lt;→o&lt; : {x y : OD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y
1393
1394 </pre>
1395 Equivalence on OD
1396 <p>
1397
1398 <pre>
1399 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
1400
1401 </pre>
1402 Upper bound
1403 <p>
1404
1405 <pre>
1406 sup-o : ( Ordinal → Ordinal ) → Ordinal
1407 sup-o&lt; : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o&lt; sup-o ψ
1408
1409 </pre>
1410 Axiom of choice and strong axiom of regularity.
1411 <p>
1412
1413 <pre>
1414 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
1415 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
1416 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
1417
1418 </pre>
1419
1420 <hr/>
1421 <h2><a name="content053">So it this correct?</a></h2>
1422
1423 <p>
1424 Our axiom are syntactically the same in the text book, but negations are slightly different.
1425 <p>
1426 If we assumes excluded middle, these are exactly same.
1427 <p>
1428 Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it.
1429 <p>
1430 Except the upper bound, axioms are simple logical relation.
1431 <p>
1432 Proof of existence of mapping between OD and Ordinals are not obvious. We don't know we prove it or not.
1433 <p>
1434 Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts,
1435 but we don't have explicit upper limit on Ordinals.
1436 <p>
1437 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct.
1438 <p>
1439
1440 <hr/>
1441 <h2><a name="content054">How to use Agda Set Theory</a></h2>
1442 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be
1443 postulated or assuming law of excluded middle.
1444 <p>
1445 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check
1446 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory.
1447 <p>
1448 ZF record itself is not necessary, for example, topology theory without ZF can be possible.
1449 <p>
1450
1451 <hr/>
1452 <h2><a name="content055">Topos and Set Theory</a></h2>
1453 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a
1454 sub-object classifier.
1455 <p>
1456 Topos itself is model of intuitionistic logic.
1457 <p>
1458 Transitive Sets are objects of Cartesian closed category.
1459 It is possible to introduce Power Set Functor on it
1460 <p>
1461 We can use replacement A ∩ x for each element in Transitive Set,
1462 in the similar way of our power set axiom. I
1463 <p>
1464 A model of ZF Set theory can be constructed on top of the Topos which is shown in Oisus.
1465 <p>
1466 Our Agda model is a proof theoretic version of it.
1467 <p>
1468
1469 <hr/>
1470 <h2><a name="content056">Cardinal number and Continuum hypothesis</a></h2>
1471 Axiom of choice is required to define cardinal number
1472 <p>
1473 definition of cardinal number is not yet done
1474 <p>
1475 definition of filter is not yet done
1476 <p>
1477 we may have a model without axiom of choice or without continuum hypothesis
1478 <p>
1479 Possible representation of continuum hypothesis is this.
1480 <p>
1481
1482 <pre>
1483 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
1484
1485 </pre>
1486
1487 <hr/>
1488 <h2><a name="content057">Filter</a></h2>
1489
1490 <p>
1491 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
1492 is depends on axiom of choice.
1493 <p>
1494
1495 <pre>
1496 record Filter ( L : OD ) : Set (suc n) where
1497 field
1498 filter : OD
1499 proper : ¬ ( filter ∋ od∅ )
1500 inL : filter ⊆ L
1501 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
1502 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
1503
1504 </pre>
1505 We may construct a model of non standard analysis or set theory.
1506 <p>
1507 This may be simpler than classical forcing theory ( not yet done).
1508 <p>
1509
1510 <hr/>
1511 <h2><a name="content058">Programming Mathematics</a></h2>
1512 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
1513 structure are
1514 <p>
1515
1516 <pre>
1517 record and data
1518
1519 </pre>
1520 Proof is check by type consistency not by the computation, but it may include some normalization.
1521 <p>
1522 Type inference and termination is not so clear in multi recursions.
1523 <p>
1524 Defining Agda record is a good way to understand mathematical theory, for examples,
1525 <p>
1526
1527 <pre>
1528 Category theory ( Yoneda lemma, Floyd Adjunction functor theorem, Applicative functor )
1529 Automaton ( Subset construction、Language containment)
1530
1531 </pre>
1532 are proved in Agda.
1533 <p>
1534
1535 <hr/>
1536 <h2><a name="content059">link</a></h2>
1537 Summer school of foundation of mathematics (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/</a>
1538 <p>
1539 Foundation of axiomatic set theory (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf
1540 </a>
1541 <p>
1542 Agda
1543 <br> <a href="https://agda.readthedocs.io/en/v2.6.0.1/">https://agda.readthedocs.io/en/v2.6.0.1/</a>
1544 <p>
1545 ZF-in-Agda source
1546 <br> <a href="https://github.com/shinji-kono/zf-in-agda.git">https://github.com/shinji-kono/zf-in-agda.git
1547 </a>
1548 <p>
1549 Category theory in Agda source
1550 <br> <a href="https://github.com/shinji-kono/category-exercise-in-agda">https://github.com/shinji-kono/category-exercise-in-agda
1551 </a>
1552 <p>
1553 </div>
1554 <ol class="side" id="menu">
1555 Constructing ZF Set Theory in Agda
1556 <li><a href="#content000"> Programming Mathematics</a>
1557 <li><a href="#content001"> Target</a>
1558 <li><a href="#content002"> Why Set Theory</a>
1559 <li><a href="#content003"> Agda and Intuitionistic Logic </a>
1560 <li><a href="#content004"> Introduction of Agda </a>
1561 <li><a href="#content005"> data ( Sum type )</a>
1562 <li><a href="#content006"> A → B means "A implies B"</a>
1563 <li><a href="#content007"> introduction と elimination</a>
1564 <li><a href="#content008"> To prove A → B </a>
1565 <li><a href="#content009"> A ∧ B</a>
1566 <li><a href="#content010"> record</a>
1567 <li><a href="#content011"> Mathematical structure</a>
1568 <li><a href="#content012"> A Model and a theory</a>
1569 <li><a href="#content013"> postulate と module</a>
1570 <li><a href="#content014"> A ∨ B</a>
1571 <li><a href="#content015"> Negation</a>
1572 <li><a href="#content016"> Equality </a>
1573 <li><a href="#content017"> Equivalence relation</a>
1574 <li><a href="#content018"> Ordering</a>
1575 <li><a href="#content019"> Quantifier</a>
1576 <li><a href="#content020"> Can we do math in this way?</a>
1577 <li><a href="#content021"> Things which Agda cannot prove</a>
1578 <li><a href="#content022"> Classical story of ZF Set Theory</a>
1579 <li><a href="#content023"> Ordinals</a>
1580 <li><a href="#content024"> Axiom of Ordinals</a>
1581 <li><a href="#content025"> Concrete Ordinals</a>
1582 <li><a href="#content026"> Model of Ordinals</a>
1583 <li><a href="#content027"> Debugging axioms using Model</a>
1584 <li><a href="#content028"> Countable Ordinals can contains uncountable set?</a>
1585 <li><a href="#content029"> What is Set</a>
1586 <li><a href="#content030"> We don't ask the contents of Set. It can be anything.</a>
1587 <li><a href="#content031"> Ordinal Definable Set</a>
1588 <li><a href="#content032"> ∋ in OD</a>
1589 <li><a href="#content033"> 1 to 1 mapping between an OD and an Ordinal</a>
1590 <li><a href="#content034"> Order preserving in the mapping of OD and Ordinal</a>
1591 <li><a href="#content035"> ISO</a>
1592 <li><a href="#content036"> Various Sets</a>
1593 <li><a href="#content037"> Fixes on ZF to intuitionistic logic</a>
1594 <li><a href="#content038"> Pure logical axioms</a>
1595 <li><a href="#content039"> Axiom of Pair</a>
1596 <li><a href="#content040"> pair in OD</a>
1597 <li><a href="#content041"> Validity of Axiom of Pair</a>
1598 <li><a href="#content042"> Equality of OD and Axiom of Extensionality </a>
1599 <li><a href="#content043"> Validity of Axiom of Extensionality</a>
1600 <li><a href="#content044"> Non constructive assumptions so far</a>
1601 <li><a href="#content045"> Axiom which have negation form</a>
1602 <li><a href="#content046"> Union </a>
1603 <li><a href="#content047"> Axiom of replacement</a>
1604 <li><a href="#content048"> Validity of Power Set Axiom</a>
1605 <li><a href="#content049"> Axiom of regularity, Axiom of choice, ε-induction</a>
1606 <li><a href="#content050"> Axiom of choice and Law of Excluded Middle</a>
1607 <li><a href="#content051"> Relation-ship among ZF axiom</a>
1608 <li><a href="#content052"> Non constructive assumption in our model</a>
1609 <li><a href="#content053"> So it this correct?</a>
1610 <li><a href="#content054"> How to use Agda Set Theory</a>
1611 <li><a href="#content055"> Topos and Set Theory</a>
1612 <li><a href="#content056"> Cardinal number and Continuum hypothesis</a>
1613 <li><a href="#content057"> Filter</a>
1614 <li><a href="#content058"> Programming Mathematics</a>
1615 <li><a href="#content059"> link</a>
1616 </ol>
1617
1618 <hr/> Shinji KONO / Sat Jan 11 20:04:01 2020
1619 </body></html>