Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf-in-agda.html @ 273:9ccf8514c323
add documents
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 11 Jan 2020 20:11:51 +0900 |
| parents | |
| children | 197e0b3d39dc |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/zf-in-agda.html Sat Jan 11 20:11:51 2020 +0900 @@ -0,0 +1,1619 @@ +<html> +<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=UTF-8"> +<head> +<STYLE type="text/css"> +.main { width:100%; } +.side { top:0px; width:0%; position:fixed; left:80%; display:none} +</STYLE> +<script type="text/javascript"> +function showElement(layer){ + var myLayer = document.getElementById(layer); + var main = document.getElementById('mmm'); + if(myLayer.style.display=="none"){ + myLayer.style.width="20%"; + main.style.width="80%"; + myLayer.style.display="block"; + myLayer.backgroundPosition="top"; + } else { + myLayer.style.width="0%"; + main.style.width="100%"; + myLayer.style.display="none"; + } +} +</script> +<title>Constructing ZF Set Theory in Agda </title> +</head> +<body> +<div class="main" id="mmm"> +<h1>Constructing ZF Set Theory in Agda </h1> +<a href="#" right="0px" onclick="javascript:showElement('menu')"> +<span>Menu</span> +</a> +<a href="#" left="0px" onclick="javascript:showElement('menu')"> +<span>Menu</span> +</a> + +<p> + +<author> Shinji KONO</author> + +<hr/> +<h2><a name="content000">Programming Mathematics</a></h2> +Programming is processing data structure with λ terms. +<p> +We are going to handle Mathematics in intuitionistic logic with λ terms. +<p> +Mathematics is a functional programming which values are proofs. +<p> +Programming ZF Set Theory in Agda +<p> + +<hr/> +<h2><a name="content001">Target</a></h2> + +<pre> + Describe ZF axioms in Agda + Construction a Model of ZF Set Theory in Agda + Show necessary assumptions for the model + Show validities of ZF axioms on the model + +</pre> +This shows consistency of Set Theory (with some assumptions), +without circulating ZF Theory assumption. +<p> +<a href="https://github.com/shinji-kono/zf-in-agda"> +ZF in Agda https://github.com/shinji-kono/zf-in-agda +</a> +<p> + +<hr/> +<h2><a name="content002">Why Set Theory</a></h2> +If we can formulate Set theory, it suppose to work on any mathematical theory. +<p> +Set Theory is a difficult point for beginners especially axiom of choice. +<p> +It has some amount of difficulty and self circulating discussion. +<p> +I'm planning to do it in my old age, but I'm enough age now. +<p> +This is done during from May to September. +<p> + +<hr/> +<h2><a name="content003">Agda and Intuitionistic Logic </a></h2> +Curry Howard Isomorphism +<p> + +<pre> + Proposition : Proof ⇔ Type : Value + +</pre> +which means +<p> + constructing a typed lambda calculus which corresponds a logic +<p> +Typed lambda calculus which allows complex type as a value of a variable (System FC) +<p> + First class Type / Dependent Type +<p> +Agda is a such a programming language which has similar syntax of Haskell +<p> +Coq is specialized in proof assistance such as command and tactics . +<p> + +<hr/> +<h2><a name="content004">Introduction of Agda </a></h2> +A length of a list of type A. +<p> + +<pre> + length : {A : Set } → List A → Nat + length [] = zero + length (_ ∷ t) = suc ( length t ) + +</pre> +Simple functional programming language. Type declaration is mandatory. +A colon means type, an equal means value. Indentation based. +<p> +Set is a base type (which may have a level ). +<p> +{} means implicit variable which can be omitted if Agda infers its value. +<p> + +<hr/> +<h2><a name="content005">data ( Sum type )</a></h2> +A data type which as exclusive multiple constructors. A similar one as +union in C or case class in Scala. +<p> +It has a similar syntax as Haskell but it has a slight difference. +<p> + +<pre> + data List (A : Set ) : Set where + [] : List A + _∷_ : A → List A → List A + +</pre> +_∷_ means infix operator. If use explicit _, it can be used in a normal function +syntax. +<p> +Natural number can be defined as a usual way. +<p> + +<pre> + data Nat : Set where + zero : Nat + suc : Nat → Nat + +</pre> + +<hr/> +<h2><a name="content006"> A → B means "A implies B"</a></h2> + +<p> +In Agda, a type can be a value of a variable, which is usually called dependent type. +Type has a name Set in Agda. +<p> + +<pre> + ex3 : {A B : Set} → Set + ex3 {A}{B} = A → B + +</pre> +ex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B. +<p> + +<pre> + A type is a formula, the value is the proof + +</pre> +A value of A → B can be interpreted as an inference from the formula A to the formula B, which +can be a function from a proof of A to a proof of B. +<p> + +<hr/> +<h2><a name="content007">introduction と elimination</a></h2> +For a logical operator, there are two types of inference, an introduction and an elimination. +<p> + +<pre> + intro creating symbol / constructor / introduction + elim using symbolic / accessors / elimination + +</pre> +In Natural deduction, this can be written in proof schema. +<p> + +<pre> + A + : + B A A → B + ------------- →intro ------------------ →elim + A → B B + +</pre> +In Agda, this is a pair of type and value as follows. Introduction of → uses λ. +<p> + +<pre> + →intro : {A B : Set } → A → B → ( A → B ) + →intro _ b = λ x → b + →elim : {A B : Set } → A → ( A → B ) → B + →elim a f = f a + +</pre> +Important +<p> + +<pre> + {A B : Set } → A → B → ( A → B ) + +</pre> +is +<p> + +<pre> + {A B : Set } → ( A → ( B → ( A → B ) )) + +</pre> +This makes currying of function easy. +<p> + +<hr/> +<h2><a name="content008"> To prove A → B </a></h2> +Make a left type as an argument. (intros in Coq) +<p> + +<pre> + ex5 : {A B C : Set } → A → B → C → ? + ex5 a b c = ? + +</pre> +? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole. +<p> +We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red), +insufficient proof or instance (Yellow), Non-termination, the proof is completed. +<p> + +<hr/> +<h2><a name="content009"> A ∧ B</a></h2> +Well known conjunction's introduction and elimination is as follow. +<p> + +<pre> + A B A ∧ B A ∧ B + ------------- ----------- proj1 ---------- proj2 + A ∧ B A B + +</pre> +We can introduce a corresponding structure in our functional programming language. +<p> + +<hr/> +<h2><a name="content010"> record</a></h2> + +<pre> + record _∧_ A B : Set + field + proj1 : A + proj2 : B + +</pre> +_∧_ means infix operator. _∧_ A B can be written as A ∧ B (Haskell uses (∧) ) +<p> +This a type which constructed from type A and type B. You may think this as an object +or struct. +<p> + +<pre> + record { proj1 = x ; proj2 = y } + +</pre> +is a constructor of _∧_. +<p> + +<pre> + ex3 : {A B : Set} → A → B → ( A ∧ B ) + ex3 a b = record { proj1 = a ; proj2 = b } + ex1 : {A B : Set} → ( A ∧ B ) → A + ex1 a∧b = proj1 a∧b + +</pre> +a∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols +except parenthesis or colons. A symbol requires space separation such as a type defining colon. +<p> +Defining record can be recursively, but we don't use the recursion here. +<p> + +<hr/> +<h2><a name="content011"> Mathematical structure</a></h2> +We have types of elements and the relationship in a mathematical structure. +<p> + +<pre> + logical relation has no ordering + there is a natural ordering in arguments and a value in a function + +</pre> +So we have typical definition style of mathematical structure with records. +<p> + +<pre> + record IsOrdinals {n : Level} (ord : Set n) + (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where + field + Otrans : {x y z : ord } → x o< y → y o< z → x o< z + record Ordinals {n : Level} : Set (suc (suc n)) where + field + ord : Set n + _o<_ : ord → ord → Set n + isOrdinal : IsOrdinals ord _o<_ + +</pre> +In IsOrdinals, axioms are written in flat way. In Ordinal, we may have +inputs and outputs are put in the field including IsOrdinal. +<p> +Fields of Ordinal is existential objects in the mathematical structure. +<p> + +<hr/> +<h2><a name="content012"> A Model and a theory</a></h2> +Agda record is a type, so we can write it in the argument, but is it really exists? +<p> +If we have a value of the record, it simply exists, that is, we need to create all the existence +in the record satisfies all the axioms (= field of IsOrdinal) should be valid. +<p> + +<pre> + type of record = theory + value of record = model + +</pre> +We call the value of the record as a model. If mathematical structure has a +model, it exists. Pretty Obvious. +<p> + +<hr/> +<h2><a name="content013"> postulate と module</a></h2> +Agda proofs are separated by modules, which are large records. +<p> +postulates are assumptions. We can assume a type without proofs. +<p> + +<pre> + postulate + sup-o : ( Ordinal → Ordinal ) → Ordinal + sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ + +</pre> +sup-o is an example of upper bound of a function and sup-o< assumes it actually satisfies all the value is less than upper bound. +<p> +Writing some type in a module argument is the same as postulating a type, but +postulate can be written the middle of a proof. +<p> +postulate can be constructive. +<p> +postulate can be inconsistent, which result everything has a proof. +<p> + +<hr/> +<h2><a name="content014"> A ∨ B</a></h2> + +<pre> + data _∨_ (A B : Set) : Set where + case1 : A → A ∨ B + case2 : B → A ∨ B + +</pre> +As Haskell, case1/case2 are patterns. +<p> + +<pre> + ex3 : {A B : Set} → ( A ∨ A ) → A + ex3 = ? + +</pre> +In a case statement, Agda command C-C C-C generates possible cases in the head. +<p> + +<pre> + ex3 : {A B : Set} → ( A ∨ A ) → A + ex3 (case1 x) = ? + ex3 (case2 x) = ? + +</pre> +Proof schema of ∨ is omit due to the complexity. +<p> + +<hr/> +<h2><a name="content015"> Negation</a></h2> + +<pre> + ⊥ + ------------- ⊥-elim + A + +</pre> +Anything can be derived from bottom, in this case a Set A. There is no introduction rule +in ⊥, which can be implemented as data which has no constructor. +<p> + +<pre> + data ⊥ : Set where + +</pre> +⊥-elim can be proved like this. +<p> + +<pre> + ⊥-elim : {A : Set } -> ⊥ -> A + ⊥-elim () + +</pre> +() means no match argument nor value. +<p> +A negation can be defined using ⊥ like this. +<p> + +<pre> + ¬_ : Set → Set + ¬ A = A → ⊥ + +</pre> + +<hr/> +<h2><a name="content016">Equality </a></h2> + +<p> +All the value in Agda are terms. If we have the same normalized form, two terms are equal. +If we have variables in the terms, we will perform an unification. unifiable terms are equal. +We don't go further on the unification. +<p> + +<pre> + { x : A } x ≡ y f x y + --------------- ≡-intro --------------------- ≡-elim + x ≡ x f x x + +</pre> +equality _≡_ can be defined as a data. +<p> + +<pre> + data _≡_ {A : Set } : A → A → Set where + refl : {x : A} → x ≡ x + +</pre> +The elimination of equality is a substitution in a term. +<p> + +<pre> + subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y + subst {A} {x} {y} f refl fx = fx + ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z + ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y + +</pre> + +<hr/> +<h2><a name="content017">Equivalence relation</a></h2> + +<p> + +<pre> + refl' : {A : Set} {x : A } → x ≡ x + refl' = ? + sym : {A : Set} {x y : A } → x ≡ y → y ≡ x + sym = ? + trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z + trans = ? + cong : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y + cong = ? + +</pre> + +<hr/> +<h2><a name="content018">Ordering</a></h2> + +<p> +Relation is a predicate on two value which has a same type. +<p> + +<pre> + A → A → Set + +</pre> +Defining order is the definition of this type with predicate or a data. +<p> + +<pre> + data _≤_ : Rel ℕ 0ℓ where + z≤n : ∀ {n} → zero ≤ n + s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n + +</pre> + +<hr/> +<h2><a name="content019">Quantifier</a></h2> + +<p> +Handling quantifier in an intuitionistic logic requires special cares. +<p> +In the input of a function, there are no restriction on it, that is, it has +a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it) +<p> +There is no ∃ in agda, the one way is using negation like this. +<p> + ∃ (x : A ) → p x = ¬ ( ( x : A ) → ¬ ( p x ) ) +<p> +On the another way, f : A can be used like this. +<p> + +<pre> + p f + +</pre> +If we use a function which can be defined globally which has stronger meaning the +usage of ∃ x in a logical expression. +<p> + +<hr/> +<h2><a name="content020">Can we do math in this way?</a></h2> +Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support). +<p> +In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF). +<p> + +<pre> + define mathematical structure as a record + program inferences as if we have proofs in variables + +</pre> + +<hr/> +<h2><a name="content021">Things which Agda cannot prove</a></h2> + +<p> +The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which +leads uniqueness of a functor in Category Theory. +<p> +Functional extensionality cannot be proved. +<pre> + (∀ x → f x ≡ g x) → f ≡ g + +</pre> +Agda has no law of exclude middle. +<p> + +<pre> + a ∨ ( ¬ a ) + +</pre> +For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot. +<p> +It also other problems such as termination, type inference or unification which we may overcome with +efforts or devices or may not. +<p> +If we cannot prove something, we can safely postulate it unless it leads a contradiction. +<pre> + + +</pre> + +<hr/> +<h2><a name="content022">Classical story of ZF Set Theory</a></h2> + +<p> +Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads +a relative consistency proof of the Set Theory. +Ordinal number is used in the flow. +<p> +In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD). +We need some non constructive assumptions in the construction. A model of Set theory is +constructed based on these assumptions. +<p> +<img src="fig/set-theory.svg"> + +<p> + +<hr/> +<h2><a name="content023">Ordinals</a></h2> +Ordinals are our intuition of infinite things, which has ∅ and orders on the things. +It also has a successor osuc. +<p> + +<pre> + record Ordinals {n : Level} : Set (suc (suc n)) where + field + ord : Set n + o∅ : ord + osuc : ord → ord + _o<_ : ord → ord → Set n + isOrdinal : IsOrdinals ord o∅ osuc _o<_ + +</pre> +It is different from natural numbers in way. The order of Ordinals is not defined in terms +of successor. It is given from outside, which make it possible to have higher order infinity. +<p> + +<hr/> +<h2><a name="content024">Axiom of Ordinals</a></h2> +Properties of infinite things. We request a transfinite induction, which states that if +some properties are satisfied below all possible ordinals, the properties are true on all +ordinals. +<p> +Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals +which is not a successor of any ordinals. It is called limit ordinal. +<p> +Any two ordinal can be compared, that is less, equal or more, that is total order. +<p> + +<pre> + record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) + (osuc : ord → ord ) + (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where + field + Otrans : {x y z : ord } → x o< y → y o< z → x o< z + OTri : Trichotomous {n} _≡_ _o<_ + ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) + <-osuc : { x : ord } → x o< osuc x + osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) + TransFinite : { ψ : ord → Set (suc n) } + → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) + → ∀ (x : ord) → ψ x + +</pre> + +<hr/> +<h2><a name="content025">Concrete Ordinals</a></h2> + +<p> +We can define a list like structure with level, which is a kind of two dimensional infinite array. +<p> + +<pre> + data OrdinalD {n : Level} : (lv : Nat) → Set n where + Φ : (lv : Nat) → OrdinalD lv + OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv + +</pre> +The order of the OrdinalD can be defined in this way. +<p> + +<pre> + data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where + Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x + s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y + +</pre> +This is a simple data structure, it has no abstract assumptions, and it is countable many data +structure. +<p> + +<pre> + Φ 0 + OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2))) + Osuc 0 (Φ 0) d< Φ 1 + +</pre> + +<hr/> +<h2><a name="content026">Model of Ordinals</a></h2> + +<p> +It is easy to show OrdinalD and its order satisfies the axioms of Ordinals. +<p> +So our Ordinals has a mode. This means axiom of Ordinals are consistent. +<p> + +<hr/> +<h2><a name="content027">Debugging axioms using Model</a></h2> +Whether axiom is correct or not can be checked by a validity on a mode. +<p> +If not, we may fix the axioms or the model, such as the definitions of the order. +<p> +We can also ask whether the inputs exist. +<p> + +<hr/> +<h2><a name="content028">Countable Ordinals can contains uncountable set?</a></h2> +Yes, the ordinals contains any level of infinite Set in the axioms. +<p> +If we handle real-number in the model, only countable number of real-number is used. +<p> + +<pre> + from the outside view point, it is countable + from the internal view point, it is uncountable + +</pre> +The definition of countable/uncountable is the same, but the properties are different +depending on the context. +<p> +We don't show the definition of cardinal number here. +<p> + +<hr/> +<h2><a name="content029">What is Set</a></h2> +The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?). +<p> +From naive point view, a set i a list, but in Agda, elements have all the same type. +A set in ZF may contain other Sets in ZF, which not easy to implement it as a list. +<p> +Finite set may be written in finite series of ∨, but ... +<p> + +<hr/> +<h2><a name="content030">We don't ask the contents of Set. It can be anything.</a></h2> +From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on, +and all of them, and again we repeat this. +<p> + +<pre> + φ {φ} {φ,{φ}}, {φ,{φ},...} + +</pre> +It is called V. +<p> +This operation can be performed within a ZF Set theory. Classical Set Theory assumes +ZF, so this kind of thing is allowed. +<p> +But in our case, we have no ZF theory, so we are going to use Ordinals. +<p> + +<hr/> +<h2><a name="content031">Ordinal Definable Set</a></h2> +We can define a sbuset of Ordinals using predicates. What is a subset? +<p> + +<pre> + a predicate has an Ordinal argument + +</pre> +is an Ordinal Definable Set (OD). In Agda, OD is defined as follows. +<p> + +<pre> + record OD : Set (suc n ) where + field + def : (x : Ordinal ) → Set n + +</pre> +Ordinals itself is not a set in a ZF Set theory but a class. In OD, +<p> + +<pre> + record { def = λ x → true } + +</pre> +means Ordinals itself, so ODs are larger than a notion of ZF Set Theory, +but we don't care about it. +<p> + +<hr/> +<h2><a name="content032">∋ in OD</a></h2> +OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping +<p> + +<pre> + od→ord : OD → Ordinal + +</pre> +we may check an OD is an element of the OD using def. +<p> +A ∋ x can be define as follows. +<p> + +<pre> + _∋_ : ( A x : OD ) → Set n + _∋_ A x = def A ( od→ord x ) + +</pre> +In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then +<p> + +<pre> + A x = def A ( od→ord x ) = ψ (od→ord x) + +</pre> + +<hr/> +<h2><a name="content033">1 to 1 mapping between an OD and an Ordinal</a></h2> + +<p> + +<pre> + od→ord : OD → Ordinal + ord→od : Ordinal → OD + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + +</pre> +They say the existing of the mappings can be proved in Classical Set Theory, but we +simply assumes these non constructively. +<p> +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 +state it. +<p> +<img src="fig/ord-od-mapping.svg"> + +<p> + +<hr/> +<h2><a name="content034">Order preserving in the mapping of OD and Ordinal</a></h2> +Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ). +<p> + +<pre> + def y ( od→ord x ) + +</pre> +An elements of OD should be defined before the OD, that is, an ordinal corresponding an elements +have to be smaller than the corresponding ordinal of the containing OD. +<p> + +<pre> + c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y + +</pre> +This is also said to be provable in classical Set Theory, but we simply assumes it. +<p> +OD has an order based on the corresponding ordinal, but it may not have corresponding def / ∋relation. This means the reverse order preservation, +<p> + +<pre> + o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x + +</pre> +is not valid. If we assumes it, ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in +the model. +<p> +<img src="fig/ODandOrdinals.svg"> + +<p> + +<hr/> +<h2><a name="content035">ISO</a></h2> +It also requires isomorphisms, +<p> + +<pre> + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + +</pre> + +<hr/> +<h2><a name="content036">Various Sets</a></h2> + +<p> +In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate. +<p> + +<pre> + Ordinal / things satisfies axiom of Ordinal / extension of natural number + V / hierarchical construction of Set from φ + L / hierarchical predicate definable construction of Set from φ + OD / equational formula on Ordinals + Agda Set / Type / it also has a level + +</pre> + +<hr/> +<h2><a name="content037">Fixes on ZF to intuitionistic logic</a></h2> + +<p> +We use ODs as Sets in ZF, and defines record ZF, that is, we have to define +ZF axioms in Agda. +<p> +It may not valid in our model. We have to debug it. +<p> +Fixes are depends on axioms. +<p> +<img src="fig/axiom-type.svg"> + +<p> +<a href="fig/zf-record.html"> +ZFのrecord </a> +<p> + +<hr/> +<h2><a name="content038">Pure logical axioms</a></h2> + +<pre> + empty, pair, select, ε-inductioninfinity + +</pre> +These are logical relations among OD. +<p> + +<pre> + empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) + pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) + pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t + selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ ) + infinity∅ : ∅ ∈ infinite + infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ( x , x ) ) ∈ infinite + ε-induction : { ψ : OD → Set (suc n)} + → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) + → (x : OD ) → ψ x + +</pre> +finitely can be define by Agda data. +<p> + +<pre> + data infinite-d : ( x : Ordinal ) → Set n where + iφ : infinite-d o∅ + isuc : {x : Ordinal } → infinite-d x → + infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) + +</pre> +Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model. +<p> + +<hr/> +<h2><a name="content039">Axiom of Pair</a></h2> +In the Tanaka's book, axiom of pair is as follows. +<p> + +<pre> + ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y) + +</pre> +We have fix ∃ z, a function (x , y) is defined, which is _,_ . +<p> + +<pre> + _,_ : ( A B : ZFSet ) → ZFSet + +</pre> +using this, we can define two directions in separates axioms, like this. +<p> + +<pre> + pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) + pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t + +</pre> +This is already written in Agda, so we use these as axioms. All inputs have ∀. +<p> + +<hr/> +<h2><a name="content040">pair in OD</a></h2> +OD is an equation on Ordinals, we can simply write axiom of pair in the OD. +<p> + +<pre> + _,_ : OD → OD → OD + x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } + +</pre> +≡ is an equality of λ terms, but please not that this is equality on Ordinals. +<p> + +<hr/> +<h2><a name="content041">Validity of Axiom of Pair</a></h2> +Assuming ZFSet is OD, we are going to prove pair→ . +<p> + +<pre> + pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) + pair→ x y t p = ? + +</pre> +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 ) . +<p> +Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ). +<p> + +<pre> + pair→ x y t (case1 t≡x ) = ? + pair→ x y t (case2 t≡y ) = ? + +</pre> +The type of the ? is ( t == x ) ∨ ( t == y ), again it is data _∨_ . +<p> + +<pre> + pair→ x y t (case1 t≡x ) = case1 ? + pair→ x y t (case2 t≡y ) = case2 ? + +</pre> +The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable +which type is +<p> + +<pre> + t≡x : od→ord t ≡ od→ord x + +</pre> +which is shown by an Agda command (C-C C-E : agda2-show-context ). +<p> +But we haven't defined == yet. +<p> + +<hr/> +<h2><a name="content042">Equality of OD and Axiom of Extensionality </a></h2> +OD is defined by a predicates, if we compares normal form of the predicates, even if +it contains the same elements, it may be different, which is no good as an equality of +Sets. +<p> +Axiom of Extensionality requires sets having the same elements are handled in the same way +each other. +<p> + +<pre> + ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) + +</pre> +We can write this axiom in Agda as follows. +<p> + +<pre> + extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w ) + +</pre> +So we use ( A ∋ z ) ⇔ (B ∋ z) as an equality (_==_) of our model. We have to show +A ∈ w ⇔ B ∈ w from A == B. +<p> +x == y can be defined in this way. +<p> + +<pre> + record _==_ ( a b : OD ) : Set n where + field + eq→ : ∀ { x : Ordinal } → def a x → def b x + eq← : ∀ { x : Ordinal } → def b x → def a x + +</pre> +Actually, (z : OD) → (A ∋ z) ⇔ (B ∋ z) implies A == B. +<p> + +<pre> + extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B + eq→ (extensionality0 {A} {B} eq ) {x} d = ? + eq← (extensionality0 {A} {B} eq ) {x} d = ? + +</pre> +? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) . +<p> +Actual proof is rather complicated. +<p> + +<pre> + eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d + eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d + +</pre> +where +<p> + +<pre> + def-iso : {A B : OD } {x y : Ordinal } → x ≡ y → (def A y → def B y) → def A x → def B x + def-iso refl t = t + +</pre> + +<hr/> +<h2><a name="content043">Validity of Axiom of Extensionality</a></h2> + +<p> +If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible, so we assumes +<p> + +<pre> + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + +</pre> +Using this, we have +<p> + +<pre> + extensionality : {A B w : OD } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B) + proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d + proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d + +</pre> +This assumption means we may have an equivalence set on any predicates. +<p> + +<hr/> +<h2><a name="content044">Non constructive assumptions so far</a></h2> +We have correspondence between OD and Ordinals and one directional order preserving. +<p> +We also have equality assumption. +<p> + +<pre> + od→ord : OD → Ordinal + ord→od : Ordinal → OD + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + +</pre> + +<hr/> +<h2><a name="content045">Axiom which have negation form</a></h2> + +<p> + +<pre> + Union, Selection + +</pre> +These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )). +<p> +Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive. +<p> +Power Set axiom requires double negation, +<p> + +<pre> + power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x ) + power← : ∀( A t : ZFSet ) → t ⊆_ A → Power A ∋ t + +</pre> +If we have an assumption of law of exclude middle, we can recover the original A ∋ x form. +<p> + +<hr/> +<h2><a name="content046">Union </a></h2> +The original form of the Axiom of Union is +<p> + +<pre> + ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) + +</pre> +Union requires the existence of b in a ⊇ ∃ b ∋ x . We will use negation form of ∃. +<p> + +<pre> + union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z + union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) + +</pre> +The definition of Union in OD is like this. +<p> + +<pre> + Union : OD → OD + Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } + +</pre> +Proof of validity is straight forward. +<p> + +<pre> + union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z + union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx + ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) + union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) + union← X z UX∋z = FExists _ lemma UX∋z where + lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) + lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } + +</pre> +where +<p> + +<pre> + FExists : {m l : Level} → ( ψ : Ordinal → Set m ) + → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) + → (exists : ¬ (∀ y → ¬ ( ψ y ) )) + → ¬ p + FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) + +</pre> +which checks existence using contra-position. +<p> + +<hr/> +<h2><a name="content047">Axiom of replacement</a></h2> +We can replace the elements of a set by a function and it becomes a set. From the book, +<p> + +<pre> + ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) + +</pre> +The existential quantifier can be related by a function, +<p> + +<pre> + Replace : OD → (OD → OD ) → OD + +</pre> +The axioms becomes as follows. +<p> + +<pre> + replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ + replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) ) + +</pre> +In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has +negation form of existential quantifier in the definition. +<p> + +<pre> + in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD + in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } + +</pre> +Besides this upper bounds is required. +<p> + +<pre> + Replace : OD → (OD → OD ) → OD + Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } + +</pre> +We omit the proof of the validity, but it is rather straight forward. +<p> + +<hr/> +<h2><a name="content048">Validity of Power Set Axiom</a></h2> +The original Power Set Axiom is this. +<p> + +<pre> + ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) + +</pre> +The existential quantifier is replaced by a function +<p> + +<pre> + Power : ( A : OD ) → OD + +</pre> +t ⊆ X is a record like this. +<p> + +<pre> + record _⊆_ ( A B : OD ) : Set (suc n) where + field + incl : { x : OD } → A ∋ x → B ∋ x + +</pre> +Axiom becomes likes this. +<p> + +<pre> + power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) + power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t + +</pre> +The validity of the axioms are slight complicated, we have to define set of all subset. We define +subset in a different form. +<p> + +<pre> + ZFSubset : (A x : OD ) → OD + ZFSubset A x = record { def = λ y → def A y ∧ def x y } + +</pre> +We can prove, +<p> + +<pre> + ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) + +</pre> +We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals, +which is an Ordinals with our Model. +<p> + +<pre> + Ord : ( a : Ordinal ) → OD + Ord a = record { def = λ y → y o< a } + Def : (A : OD ) → OD + Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) + +</pre> +This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty). +<p> + +<pre> + Power : OD → OD + Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) + +</pre> +Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this. +<p> + +<pre> + ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) + +</pre> +In case of Ord a intro of Power Set axiom becomes valid. +<p> + +<pre> + ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t + +</pre> +Using this, we can prove, +<p> + +<pre> + power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) + power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t + +</pre> + +<hr/> +<h2><a name="content049">Axiom of regularity, Axiom of choice, ε-induction</a></h2> + +<p> +Axiom of regularity requires non self intersectable elements (which is called minimum), if we +replace it by a function, it becomes a choice function. It makes axiom of choice valid. +<p> +This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of +choice also becomes valid. +<p> + +<pre> + minimal : (x : OD ) → ¬ (x == od∅ )→ OD + x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) + minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) + +</pre> +We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set). +Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet. +<p> + +<pre> + ε-induction : { ψ : OD → Set (suc n)} + → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) + → (x : OD ) → ψ x + +</pre> +In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals. +<p> +The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia. +<p> + +<pre> + ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] + +</pre> +We can formulate like this. +<p> + +<pre> + choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet + choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A + +</pre> +It does not requires ∅ ∉ X . +<p> + +<hr/> +<h2><a name="content050">Axiom of choice and Law of Excluded Middle</a></h2> +In our model, since OD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid, +but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice, +but it requires law of the exclude middle. +<p> +Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can +perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the +set is empty or not if we have an axiom of choice, so we have the law of the exclude middle p ∨ ( ¬ p ) . +<p> + +<pre> + ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p + ppp {p} {a} d = d + +</pre> +We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice +and Law of Excluded Middle is equivalent in our mode. +<p> + +<hr/> +<h2><a name="content051">Relation-ship among ZF axiom</a></h2> +<img src="fig/axiom-dependency.svg"> + +<p> + +<hr/> +<h2><a name="content052">Non constructive assumption in our model</a></h2> +mapping between OD and Ordinals +<p> + +<pre> + od→ord : OD → Ordinal + ord→od : Ordinal → OD + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y + +</pre> +Equivalence on OD +<p> + +<pre> + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + +</pre> +Upper bound +<p> + +<pre> + sup-o : ( Ordinal → Ordinal ) → Ordinal + sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ + +</pre> +Axiom of choice and strong axiom of regularity. +<p> + +<pre> + minimal : (x : OD ) → ¬ (x == od∅ )→ OD + x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) + minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) + +</pre> + +<hr/> +<h2><a name="content053">So it this correct?</a></h2> + +<p> +Our axiom are syntactically the same in the text book, but negations are slightly different. +<p> +If we assumes excluded middle, these are exactly same. +<p> +Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it. +<p> +Except the upper bound, axioms are simple logical relation. +<p> +Proof of existence of mapping between OD and Ordinals are not obvious. We don't know we prove it or not. +<p> +Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts, +but we don't have explicit upper limit on Ordinals. +<p> +Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct. +<p> + +<hr/> +<h2><a name="content054">How to use Agda Set Theory</a></h2> +Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be +postulated or assuming law of excluded middle. +<p> +Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check +these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory. +<p> +ZF record itself is not necessary, for example, topology theory without ZF can be possible. +<p> + +<hr/> +<h2><a name="content055">Topos and Set Theory</a></h2> +Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a +sub-object classifier. +<p> +Topos itself is model of intuitionistic logic. +<p> +Transitive Sets are objects of Cartesian closed category. +It is possible to introduce Power Set Functor on it +<p> +We can use replacement A ∩ x for each element in Transitive Set, +in the similar way of our power set axiom. I +<p> +A model of ZF Set theory can be constructed on top of the Topos which is shown in Oisus. +<p> +Our Agda model is a proof theoretic version of it. +<p> + +<hr/> +<h2><a name="content056">Cardinal number and Continuum hypothesis</a></h2> +Axiom of choice is required to define cardinal number +<p> +definition of cardinal number is not yet done +<p> +definition of filter is not yet done +<p> +we may have a model without axiom of choice or without continuum hypothesis +<p> +Possible representation of continuum hypothesis is this. +<p> + +<pre> + continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a) + +</pre> + +<hr/> +<h2><a name="content057">Filter</a></h2> + +<p> +filter is a dual of ideal on boolean algebra or lattice. Existence on natural number +is depends on axiom of choice. +<p> + +<pre> + record Filter ( L : OD ) : Set (suc n) where + field + filter : OD + proper : ¬ ( filter ∋ od∅ ) + inL : filter ⊆ L + filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q + filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) + +</pre> +We may construct a model of non standard analysis or set theory. +<p> +This may be simpler than classical forcing theory ( not yet done). +<p> + +<hr/> +<h2><a name="content058">Programming Mathematics</a></h2> +Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical +structure are +<p> + +<pre> + record and data + +</pre> +Proof is check by type consistency not by the computation, but it may include some normalization. +<p> +Type inference and termination is not so clear in multi recursions. +<p> +Defining Agda record is a good way to understand mathematical theory, for examples, +<p> + +<pre> + Category theory ( Yoneda lemma, Floyd Adjunction functor theorem, Applicative functor ) + Automaton ( Subset construction、Language containment) + +</pre> +are proved in Agda. +<p> + +<hr/> +<h2><a name="content059">link</a></h2> +Summer school of foundation of mathematics (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/</a> +<p> +Foundation of axiomatic set theory (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf +</a> +<p> +Agda +<br> <a href="https://agda.readthedocs.io/en/v2.6.0.1/">https://agda.readthedocs.io/en/v2.6.0.1/</a> +<p> +ZF-in-Agda source +<br> <a href="https://github.com/shinji-kono/zf-in-agda.git">https://github.com/shinji-kono/zf-in-agda.git +</a> +<p> +Category theory in Agda source +<br> <a href="https://github.com/shinji-kono/category-exercise-in-agda">https://github.com/shinji-kono/category-exercise-in-agda +</a> +<p> +</div> +<ol class="side" id="menu"> +Constructing ZF Set Theory in Agda +<li><a href="#content000"> Programming Mathematics</a> +<li><a href="#content001"> Target</a> +<li><a href="#content002"> Why Set Theory</a> +<li><a href="#content003"> Agda and Intuitionistic Logic </a> +<li><a href="#content004"> Introduction of Agda </a> +<li><a href="#content005"> data ( Sum type )</a> +<li><a href="#content006"> A → B means "A implies B"</a> +<li><a href="#content007"> introduction と elimination</a> +<li><a href="#content008"> To prove A → B </a> +<li><a href="#content009"> A ∧ B</a> +<li><a href="#content010"> record</a> +<li><a href="#content011"> Mathematical structure</a> +<li><a href="#content012"> A Model and a theory</a> +<li><a href="#content013"> postulate と module</a> +<li><a href="#content014"> A ∨ B</a> +<li><a href="#content015"> Negation</a> +<li><a href="#content016"> Equality </a> +<li><a href="#content017"> Equivalence relation</a> +<li><a href="#content018"> Ordering</a> +<li><a href="#content019"> Quantifier</a> +<li><a href="#content020"> Can we do math in this way?</a> +<li><a href="#content021"> Things which Agda cannot prove</a> +<li><a href="#content022"> Classical story of ZF Set Theory</a> +<li><a href="#content023"> Ordinals</a> +<li><a href="#content024"> Axiom of Ordinals</a> +<li><a href="#content025"> Concrete Ordinals</a> +<li><a href="#content026"> Model of Ordinals</a> +<li><a href="#content027"> Debugging axioms using Model</a> +<li><a href="#content028"> Countable Ordinals can contains uncountable set?</a> +<li><a href="#content029"> What is Set</a> +<li><a href="#content030"> We don't ask the contents of Set. It can be anything.</a> +<li><a href="#content031"> Ordinal Definable Set</a> +<li><a href="#content032"> ∋ in OD</a> +<li><a href="#content033"> 1 to 1 mapping between an OD and an Ordinal</a> +<li><a href="#content034"> Order preserving in the mapping of OD and Ordinal</a> +<li><a href="#content035"> ISO</a> +<li><a href="#content036"> Various Sets</a> +<li><a href="#content037"> Fixes on ZF to intuitionistic logic</a> +<li><a href="#content038"> Pure logical axioms</a> +<li><a href="#content039"> Axiom of Pair</a> +<li><a href="#content040"> pair in OD</a> +<li><a href="#content041"> Validity of Axiom of Pair</a> +<li><a href="#content042"> Equality of OD and Axiom of Extensionality </a> +<li><a href="#content043"> Validity of Axiom of Extensionality</a> +<li><a href="#content044"> Non constructive assumptions so far</a> +<li><a href="#content045"> Axiom which have negation form</a> +<li><a href="#content046"> Union </a> +<li><a href="#content047"> Axiom of replacement</a> +<li><a href="#content048"> Validity of Power Set Axiom</a> +<li><a href="#content049"> Axiom of regularity, Axiom of choice, ε-induction</a> +<li><a href="#content050"> Axiom of choice and Law of Excluded Middle</a> +<li><a href="#content051"> Relation-ship among ZF axiom</a> +<li><a href="#content052"> Non constructive assumption in our model</a> +<li><a href="#content053"> So it this correct?</a> +<li><a href="#content054"> How to use Agda Set Theory</a> +<li><a href="#content055"> Topos and Set Theory</a> +<li><a href="#content056"> Cardinal number and Continuum hypothesis</a> +<li><a href="#content057"> Filter</a> +<li><a href="#content058"> Programming Mathematics</a> +<li><a href="#content059"> link</a> +</ol> + +<hr/> Shinji KONO / Sat Jan 11 20:04:01 2020 +</body></html>