Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 290:359402cc6c3d
definition of filter
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 12 Jun 2020 19:19:16 +0900 |
parents | 4ae48eed654a |
children | ef93c56ad311 |
files | OD.agda filter.agda |
diffstat | 2 files changed, 28 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Sun May 10 09:25:18 2020 +0900 +++ b/OD.agda Fri Jun 12 19:19:16 2020 +0900 @@ -53,9 +53,19 @@ eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m -- next assumptions are our axiom --- it defines a subset of OD, which is called HOD, usually defined as +-- In classical Set Theory, HOD is used, as a subset of OD, -- HOD = { x | TC x ⊆ OD } --- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x +-- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x. +-- This is not possible because we don't have V yet. +-- We simply assume V=OD here. +-- +-- We also assumes ODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks. +-- ODs have an ovbious maximum, but Ordinals are not. This means, od→ord is not an on-to mapping. +-- +-- ==→o≡ is necessary to prove axiom of extensionality. +-- +-- In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic, +-- we need explict assumption on sup. record ODAxiom : Set (suc n) where -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
--- a/filter.agda Sun May 10 09:25:18 2020 +0900 +++ b/filter.agda Fri Jun 12 19:19:16 2020 +0900 @@ -35,16 +35,27 @@ record Filter ( L : OD ) : Set (suc n) where field - filter : OD - proper : ¬ ( filter ∋ od∅ ) - inL : filter ⊆ L + filter : OD + ¬f∋∅ : ¬ ( filter ∋ od∅ ) + f∋L : filter ∋ L + f⊆PL : filter ⊆ Power L filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) +record Ideal ( L : OD ) : Set (suc n) where + field + ideal : OD + i∋∅ : ideal ∋ od∅ + ¬i∋L : ¬ ( ideal ∋ L ) + i⊆PL : ideal ⊆ Power L + ideal1 : { p q : OD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q + ideal2 : { p q : OD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) + open Filter +open Ideal L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L -L-filter {L} P {p} lt = filter1 P {p} {L} {!!} lt {!!} +L-filter {L} P {p} lt = {!!} -- filter1 P {p} {L} {!!} lt {!!} prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) @@ -62,8 +73,7 @@ generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) generated-filter {L} P p = record { - proper = {!!} ; - filter = {!!} ; inL = {!!} ; + filter = {!!} ; filter1 = {!!} ; filter2 = {!!} }