annotate zf-in-agda.html @ 289:9f926b2210bc release

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