Mercurial > hg > Members > kono > Proof > ZF-in-agda
view zf-in-agda.html @ 624:d0938f220648
supf again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 20 Jun 2022 07:49:35 +0900 |
| parents | f7d66c84bc26 |
| children |
line wrap: on
line source
<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">ZF in Agda</a></h2> <pre> zf.agda axiom of ZF zfc.agda axiom of choice Ordinals.agda axiom of Ordinals ordinal.agda countable model of Ordinals OD.agda model of ZF based on Ordinal Definable Set with assumptions ODC.agda Law of exclude middle from axiom of choice assumptions LEMC.agda model of choice with assumption of the Law of exclude middle OPair.agda ordered pair on OD BAlgbra.agda Boolean algebra on OD (not yet done) filter.agda Filter on OD (not yet done) cardinal.agda Caedinal number on OD (not yet done) logic.agda some basics on logic nat.agda some basics on Nat </pre> <hr/> <h2><a name="content001">Programming Mathematics</a></h2> <p> 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="content002">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="content003">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> if you familier with Agda, you can skip to <a href="#set-theory"> there </a> <p> <hr/> <h2><a name="content004">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="content005">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="content006">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="content007"> 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="content008">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="content009"> 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="content010"> 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="content011"> 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="content012"> 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="content013"> Limit Ordinal</a></h2> If an ordinal is not a succesor of other, it is called limit ordinal. We need predicate to decide it. <p> <pre> not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) </pre> An ordinal may have an imeditate limit ordinal, we call it next x. Axiom of nrext is this. <p> <pre> record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where field x<nx : { y : ord } → (y o< next y ) osuc<nx : { x y : ord } → x o< next y → osuc x o< next y ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z)) </pre> We show some intresting lemma. <p> <pre> next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y nexto≡ : {x : Ordinal} → next x ≡ next (osuc x) next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y) </pre> These are proved from the axiom. Our countable ordinal satisfies these. <p> <hr/> <h2><a name="content014"> 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="content015"> 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. Actualy this assumption doesnot work for Ordinals, we discuss this later. <p> <hr/> <h2><a name="content016"> 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="content017"> 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="content018">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="content019">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="content020">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="content021">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="content022">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="content023">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="content024">Classical story of ZF Set Theory</a></h2> <p> <a name="set-theory"> 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="content025">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="content026">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="content027">Concrete Ordinals or Countable 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="content028">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="content029">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="content030">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="content031">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="content032">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> The idea is to use an ordinal as a pointer to a record which defines a Set. If the recored defines a series of Ordinals which is a pointer to the Set. This record looks like a Set. <p> <hr/> <h2><a name="content033">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> data One : Set n where OneObj : One record { def = λ x → One } </pre> means it accepets all Ordinals, i.e. this is Ordinals itself, so ODs are larger than ZF Set. You can say OD is a class in ZF Set Theory term. <p> <hr/> <h2><a name="content034">OD is not ZF Set</a></h2> If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like a Set. The idea is to use an ordinal as a pointer to OD. Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like <p> <pre> ¬OD-order : ( & : OD → Ordinal ) → ( * : Ordinal → OD ) → ( { x y : OD } → def y ( & x ) → & x o< & y) → ⊥ ¬OD-order & * c<→o< = ? </pre> Actualy we can prove this contrdction, so we need some restrctions on OD. <p> This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself. <p> <hr/> <h2><a name="content035"> HOD : Hereditarily Ordinal Definable</a></h2> What we need is a bounded OD, the containment is limited by an ordinal. <p> <pre> record HOD : Set (suc n) where field od : OD odmax : Ordinal <odmax : {y : Ordinal} → def od y → y o< odmax </pre> In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means <p> <pre> HOD = { x | TC x ⊆ OD } </pre> TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. <p> <hr/> <h2><a name="content036">1 to 1 mapping between an HOD and an Ordinal</a></h2> HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping <p> <pre> & : HOD → Ordinal * : Ordinal → HOD oiso : {x : HOD } → * ( & x ) ≡ x diso : {x : Ordinal } → & ( * x ) ≡ x </pre> we can check an HOD is an element of the OD using def. <p> A ∋ x can be define as follows. <p> <pre> _∋_ : ( A x : HOD ) → Set n _∋_ A x = def (od A) ( & x ) </pre> In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then <p> <pre> A x = def A ( & 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> <img src="fig/ord-od-mapping.svg"> <p> <hr/> <h2><a name="content037">Order preserving in the mapping of OD and Ordinal</a></h2> Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ). <p> <pre> def (od y) ( & x ) </pre> An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements have to be smaller than the corresponding ordinal of the containing OD. We also assumes subset is always smaller. This is necessary to make a limit of Power Set. <p> <pre> c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) </pre> If wa assumes reverse order preservation, <p> <pre> o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (* y) x </pre> ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model. <p> <img src="fig/ODandOrdinals.svg"> <p> <hr/> <h2><a name="content038">Various Sets</a></h2> 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 φ HOD / Hereditarily Ordinal Definable OD / equational formula on Ordinals Agda Set / Type / it also has a level </pre> <hr/> <h2><a name="content039">Fixing ZF axom to fit 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="content040">Pure logical axioms</a></h2> <pre> empty, pair, select, ε-induction??infinity </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 (& ( Union (* x , (* x , * 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="content041">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="content042">pair in OD</a></h2> OD is an equation on Ordinals, we can simply write axiom of pair in the OD. <p> <pre> _,_ : HOD → HOD → HOD x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = ? ; <odmax = ? } </pre> It is easy to find out odmax from odmax of x and y. <p> ≡ is an equality of λ terms, but please not that this is equality on Ordinals. <p> <hr/> <h2><a name="content043">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 ≡ & x ) ∨ ( t ≡ & 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 : & t ≡ & 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="content044">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 : HOD) → (A ∋ z) ⇔ (B ∋ z) implies od A == od B. <p> <pre> extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → od A == od 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 = odef-iso {A} {B} (sym diso) (proj1 (eq (* x))) d eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (* x))) d </pre> where <p> <pre> odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y → (def A (od y) → def (od B) y) → def (od A) x → def (od B) x odef-iso refl t = t </pre> <hr/> <h2><a name="content045">The uniqueness of HOD</a></h2> <p> To prove extensionality or other we need ==→o≡. <p> Since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD. We can calculate the minimum using sup if we have bound but it is tedius. Only Select has non minimum odmax. We have the same problem on 'def' itself, but we leave it, that is we assume the assumption of predicates of Agda have a unique form, it is something like the functional extensionality assumption. <p> <hr/> <h2><a name="content046">Validity of Axiom of Extensionality</a></h2> If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, so we assumes <p> <pre> ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y </pre> Using this, we have <p> <pre> extensionality : {A B w : HOD } → ((z : HOD ) → (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> <hr/> <h2><a name="content047">Axiom of infinity</a></h2> <p> It means it has ω as a ZF Set. It is ususally written like this. <p> <pre> ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) </pre> x ∪ { x } is Union (x , (x , x)) in our notation. It contains existential quantifier, so we introduce a function <p> <pre> infinite : ZFSet infinity∅ : ∅ ∈ infinite infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite </pre> <hr/> <h2><a name="content048">ω in HOD</a></h2> <p> To define an OD which arrows & (Union (x , (x , x))) as a predicate, we can use Agda data structure. <p> <pre> data infinite-d : ( x : Ordinal ) → Set n where iφ : infinite-d o∅ isuc : {x : Ordinal } → infinite-d x → infinite-d (& ( Union (* x , (* x , * x ) ) )) </pre> It has simular structure as Data.Nat in Agda, and it defines a correspendence of HOD and the data structure. Now we can define HOD like this. <p> <pre> infinite : HOD infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ? ; <odmax = ? } </pre> So what is the bound of ω? Analyzing the definition, it depends on the value of & (x , x), which cannot know the aboslute value. This is because we don't have constructive definition of & : HOD → Ordinal. <p> <hr/> <h2><a name="content049">HOD and Agda data structure</a></h2> We may have <p> <pre> a HOD <=> Agda Data Strucure </pre> as a data in Agda. Ex. <p> <pre> data ord-pair : (p : Ordinal) → Set n where pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) ) ZFProduct : OD ZFProduct = record { def = λ x → ord-pair x } pi1 : { p : Ordinal } → ord-pair p → Ordinal pi1 ( pair x y) = x π1 : { p : HOD } → def ZFProduct (& p) → HOD π1 lt = * (pi1 lt ) p-iso : { x : HOD } → (p : def ZFProduct (& x) ) → < π1 p , π2 p > ≡ x p-iso {x} p = ord≡→≡ (op-iso p) </pre> <hr/> <h2><a name="content050">HOD Ordrinal mapping</a></h2> <p> We have large freedom on HOD. We reqest no minimality on odmax, so it may arbitrary larger. The address of HOD can be larger at least it have to be larger than the content's address. We only have a relative ordering such as <p> <pre> pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) ) pair<y : {x y : HOD } → y ∋ x → & (x , x) o< osuc (& y) </pre> Basicaly, we cannot know the concrete address of HOD other than empty set. <p> <img src="fig/address-of-HOD.svg"> <p> <hr/> <h2><a name="content051">Possible restriction on HOD</a></h2> We need some restriction on the HOD-Ordinal mapping. Simple one is this. <p> <pre> ωmax : Ordinal <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax </pre> It depends on infinite-d and put no assuption on the other similar construction. A more general one may be <p> <pre> hod-ord< : {x : HOD } → Set n hod-ord< {x} = & x o< next (odmax x) </pre> next : Ordinal → Ordinal means imediate next limit ordinal of x. It supress unecessary space between address of HOD and its bound. <p> In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound. This is the reason of necessity of Axiom of infinite. <p> <hr/> <h2><a name="content052">increment pase of address of HOD</a></h2> Assuming, hod-ord< , we have <p> <pre> pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x) pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1 where lemmab0 : next (odmax (x , x)) ≡ next (& x) </pre> So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove <p> <pre> infinite-bound : ({x : HOD} → & x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅ </pre> We also notice that if we have & (x , x) ≡ osuc (& x), c<→o< can be drived from ⊆→o≤ . <p> <pre> ⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) ) → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) ) → {x y : HOD } → def (od y) ( & x ) → & x o< & y </pre> <hr/> <h2><a name="content053">Non constructive assumptions so far</a></h2> <p> <pre> & : HOD → Ordinal * : Ordinal → HOD c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) oiso : {x : HOD } → * ( & x ) ≡ x diso : {x : Ordinal } → & ( * x ) ≡ x ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ </pre> <hr/> <h2><a name="content054">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="content055">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 HOD is like this. <p> <pre> Union : HOD → HOD Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (* u) x))) } ; odmax = osuc (& U) ; <odmax = ? } </pre> The bound of Union is evident, but its proof is rather complicated. <p> Proof of validity is straight forward. <p> <pre> union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z union→ X z u xx not = ⊥-elim ( not (& u) ( record { proj1 = proj1 xx ; proj2 = subst ( λ k → odef k (& z)) (sym oiso) (proj2 xx) } )) union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) union← X z UX∋z = FExists _ lemma UX∋z where lemma : {y : Ordinal} → odef X y ∧ odef (* y) (& z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) lemma {y} xx not = not (* y) record { proj1 = subst ( λ k → odef 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="content056">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 : HOD → (HOD → HOD ) → HOD </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 ≡ & (ψ (* y ))))) } </pre> in-codomain is a logical relation-ship, and it is written in OD. <p> <pre> Replace : HOD → (HOD → HOD) → HOD Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y)))) ∧ def (in-codomain X ψ) x } ; odmax = rmax ; <odmax = rmax<} where rmax : Ordinal rmax = sup-o X (λ y X∋y → & (ψ (* y))) rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax rmax< lt = proj1 lt </pre> The bbound of Replace is defined by supremum, that is, it is not limited in a limit ordinal of original ZF Set. <p> Once we have a bound, validity of the axiom is an easy task to check the logical relation-ship. <p> <hr/> <h2><a name="content057">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 : HOD ) → HOD ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma } where lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x) lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and)) </pre> We can prove, <p> <pre> ( {y : HOD } → 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 → & ( ZFSubset A (* 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 (& 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 : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → od a == od ( b ∩ a ) </pre> In case of Ord a intro of Power Set axiom becomes valid. <p> <pre> ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t </pre> Using this, we can prove, <p> <pre> power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x) power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t </pre> <hr/> <h2><a name="content058">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 : HOD ) → ¬ (x == od∅ )→ OD x∋minimal : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → def x ( & ( minimal x ne ) ) minimal-1 : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( def (minimal x ne) (& y)) ∧ (def x (& 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 : { ψ : HOD → Set (suc n)} → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) → (x : HOD ) → ψ 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="content059">Axiom of choice and Law of Excluded Middle</a></h2> In our model, since HOD 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 : HOD } → 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="content060">Relation-ship among ZF axiom</a></h2> <img src="fig/axiom-dependency.svg"> <p> <hr/> <h2><a name="content061">Non constructive assumption in our model</a></h2> mapping between HOD and Ordinals <p> <pre> & : HOD → Ordinal * : Ordinal → OD oiso : {x : HOD } → * ( & x ) ≡ x diso : {x : Ordinal } → & ( * x ) ≡ x c<→o< : {x y : HOD } → def y ( & x ) → & x o< & y ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) </pre> Equivalence on OD <p> <pre> ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y </pre> Upper bound <p> <pre> sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ </pre> In order to have bounded ω, <p> <pre> hod-ord< : {x : HOD} → & x o< next (odmax x) </pre> Axiom of choice and strong axiom of regularity. <p> <pre> minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) ) minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) ) </pre> <hr/> <h2><a name="content062">V </a></h2> <p> The cumulative hierarchy <pre> V 0 := ∅ V α + 1 := P ( V α ) V α := ⋃ { V β | β < α } </pre> Using TransFinite induction <p> <pre> V : ( β : Ordinal ) → HOD V β = TransFinite V1 β where V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD V1 x V0 with trio< x o∅ V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a) V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅ V1 x V0 | tri> ¬a ¬b c with Oprev-p x V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) V1 x V0 | tri> ¬a ¬b c | no ¬p = record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (V0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt } </pre> In our system, clearly V ⊆ HOD。 <p> <hr/> <h2><a name="content063">L</a></h2> The constructible Sets <pre> L 0 := ∅ L α + 1 := Df (L α) -- Definable Power Set V α := ⋃ { L β | β < α } </pre> What is Df? In our system, Power x is definable by Sup. <p> <pre> record Definitions : Set (suc n) where field Definition : HOD → HOD open Definitions Df : Definitions → (x : HOD) → HOD Df D x = Power x ∩ Definition D x </pre> <hr/> <h2><a name="content064">L</a></h2> <p> <pre> L : ( β : Ordinal ) → Definitions → HOD L β D = TransFinite L1 β where L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD L1 x L0 with trio< x o∅ L1 x L0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a) L1 x L0 | tri≈ ¬a refl ¬c = Ord o∅ L1 x L0 | tri> ¬a ¬b c with Oprev-p x L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) L1 x L0 | tri> ¬a ¬b c | no ¬p = record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (L0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt } </pre> <hr/> <h2><a name="content065">V=L</a></h2> <p> <pre> V=L0 : Set (suc n) V=L0 = (x : Ordinal) → V x ≡ L x record { Definition = λ y → y } </pre> is obvious. Definitions should have some restrictions, such as it includes Nat. <p> <hr/> <h2><a name="content066">Some other ...</a></h2> <hr/> <h2><a name="content067">So it this correct?</a></h2> 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 HOD 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="content068">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="content069">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="content070">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="content071">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 : HOD ) : Set (suc n) where field filter : OD proper : ¬ ( filter ∋ od∅ ) inL : filter ⊆ L filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q filter2 : { p q : HOD } → 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="content072">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="content073">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"> ZF in Agda</a> <li><a href="#content001"> Programming Mathematics</a> <li><a href="#content002"> Target</a> <li><a href="#content003"> Why Set Theory</a> <li><a href="#content004"> Agda and Intuitionistic Logic </a> <li><a href="#content005"> Introduction of Agda </a> <li><a href="#content006"> data ( Sum type )</a> <li><a href="#content007"> A → B means "A implies B"</a> <li><a href="#content008"> introduction と elimination</a> <li><a href="#content009"> To prove A → B </a> <li><a href="#content010"> A ∧ B</a> <li><a href="#content011"> record</a> <li><a href="#content012"> Mathematical structure</a> <li><a href="#content013"> Limit Ordinal</a> <li><a href="#content014"> A Model and a theory</a> <li><a href="#content015"> postulate と module</a> <li><a href="#content016"> A ∨ B</a> <li><a href="#content017"> Negation</a> <li><a href="#content018"> Equality </a> <li><a href="#content019"> Equivalence relation</a> <li><a href="#content020"> Ordering</a> <li><a href="#content021"> Quantifier</a> <li><a href="#content022"> Can we do math in this way?</a> <li><a href="#content023"> Things which Agda cannot prove</a> <li><a href="#content024"> Classical story of ZF Set Theory</a> <li><a href="#content025"> Ordinals</a> <li><a href="#content026"> Axiom of Ordinals</a> <li><a href="#content027"> Concrete Ordinals or Countable Ordinals</a> <li><a href="#content028"> Model of Ordinals</a> <li><a href="#content029"> Debugging axioms using Model</a> <li><a href="#content030"> Countable Ordinals can contains uncountable set?</a> <li><a href="#content031"> What is Set</a> <li><a href="#content032"> We don't ask the contents of Set. It can be anything.</a> <li><a href="#content033"> Ordinal Definable Set</a> <li><a href="#content034"> OD is not ZF Set</a> <li><a href="#content035"> HOD : Hereditarily Ordinal Definable</a> <li><a href="#content036"> 1 to 1 mapping between an HOD and an Ordinal</a> <li><a href="#content037"> Order preserving in the mapping of OD and Ordinal</a> <li><a href="#content038"> Various Sets</a> <li><a href="#content039"> Fixing ZF axom to fit intuitionistic logic</a> <li><a href="#content040"> Pure logical axioms</a> <li><a href="#content041"> Axiom of Pair</a> <li><a href="#content042"> pair in OD</a> <li><a href="#content043"> Validity of Axiom of Pair</a> <li><a href="#content044"> Equality of OD and Axiom of Extensionality </a> <li><a href="#content045"> The uniqueness of HOD</a> <li><a href="#content046"> Validity of Axiom of Extensionality</a> <li><a href="#content047"> Axiom of infinity</a> <li><a href="#content048"> ω in HOD</a> <li><a href="#content049"> HOD and Agda data structure</a> <li><a href="#content050"> HOD Ordrinal mapping</a> <li><a href="#content051"> Possible restriction on HOD</a> <li><a href="#content052"> increment pase of address of HOD</a> <li><a href="#content053"> Non constructive assumptions so far</a> <li><a href="#content054"> Axiom which have negation form</a> <li><a href="#content055"> Union </a> <li><a href="#content056"> Axiom of replacement</a> <li><a href="#content057"> Validity of Power Set Axiom</a> <li><a href="#content058"> Axiom of regularity, Axiom of choice, ε-induction</a> <li><a href="#content059"> Axiom of choice and Law of Excluded Middle</a> <li><a href="#content060"> Relation-ship among ZF axiom</a> <li><a href="#content061"> Non constructive assumption in our model</a> <li><a href="#content062"> V </a> <li><a href="#content063"> L</a> <li><a href="#content064"> L</a> <li><a href="#content065"> V=L</a> <li><a href="#content066"> Some other ...</a> <li><a href="#content067"> So it this correct?</a> <li><a href="#content068"> How to use Agda Set Theory</a> <li><a href="#content069"> Topos and Set Theory</a> <li><a href="#content070"> Cardinal number and Continuum hypothesis</a> <li><a href="#content071"> Filter</a> <li><a href="#content072"> Programming Mathematics</a> <li><a href="#content073"> link</a> </ol> <hr/> Shinji KONO / Tue Aug 4 18:09:41 2020 </body></html>