Voevodsky describes sets as "well-founded trees with no automorphisms".
We can formalize well-founded trees with W-types.
This is what Aczel did when interpreting CZF into type theory.
We can follow Aczel's interpretation and define "CZF" in Nuprl.
Aczel also studied non-wellfounded sets.
The non-wellfounded trees are the coW-types, and a W-type is just the
well-founded subtype of the corresponding coW-type.
We define ⌜Set{i:l}⌝ to be ⌜W(Type;x.x)⌝ and
⌜coSet{i:l}⌝ to be ⌜coW(Type;x.x)⌝
so a set (or co-set) is
⌜Wsup(T;f)⌝ where ⌜T ∈ Type⌝ and
⌜f ∈ T ⟶ Set{i:l}⌝ (or ⌜f ∈ T ⟶ coSet{i:l}⌝).
Now we need to deal with the "no automorphisms" part.
For that we need an equivalence relation on sets that corresponds to
"s1 and s2" have the same members.
Aczel defined set equality using the recursive definition:
⌜seteq(s1;s2) == let T,f = s1 in let X,g = s2 in (∀t:T. ∃x:X. seteq(f t;g x)) ∧ (∀x:X. ∃t:T. seteq(f t;g x))⌝
This is well-defined for ⌜Set{i:l}⌝ because sets are well-founded.
But it won't work for the type ⌜coSet{i:l}⌝.
If we want one definition of set equality that works for both Set and cSet
we need to use the definition that works for coSet.
That is the bisimulation relation on coW-types
which for coSet becomes
⌜seteq(s1;s2) == coW-equiv(T.T;s1;s2)⌝
This is indeed an equivalence relation on both
⌜coSet{i:l}⌝ and on ⌜Set{i:l}⌝ (see seteq_equiv).
So we would be tempted to
use the quotient type ⌜s1,s2:Set{i:l}//seteq(s1;s2)⌝ for the type of sets.
That would probably not work well for reasons similar to the
constructive reals (there is no canonical member of each equivalence class
so it won't be possible to compute with such quotiented sets).
So we just interpret = in CZF as seteq.
Now set x is a member of ⌜Wsup(T;f)⌝ if ⌜∃t:T. seteq(x;f t)⌝,
so that gives the interpretation of ⌜(x ∈ s)⌝.
Now one wants to verify the axioms of CZF as much as possible.
We have versions of restricted separation
sub-set_wf and setmem-sub-set
(restricted to propositions in universe i).
Notice that we don't need the concept of a class of sets defined
by a formula. Instead we can just use propositions about sets
(and relations on sets, rather than classes of ordered pairs)
that respect the `seteq` relation. We can call these `extensional`
propositions and relations.
The `restricted` classes correspond to propositions in universe i
and unrestricted classes to propositions in universe i+1 (or higher).
The "union-replacement" is (setunionfun_wf, setmem-setunionfun)
Again, the function can be any extensional function from sets to sets.
(Members of the function type ⌜Set{i:l} ⟶ Set{i:l}⌝ are what Bishop
call `operations` on Sets, while those that are extensional
(i.e respect `seteq`) are called `set functions`). .
Of course, pair is easy : setmem-pairset
The foundation axiom is replaced by the induction principle:
set-induction-1.
The "exponentiation" axiom seems to be the same as the
existence of the set Πa:A.B[a] (see setmem-Piset)
and we also have the set Σa:A.B[a] (see setmem-sigmaset).
We define the transitive closure of a set
(setTC-contains, setTC-transitive, setTC-least)
and the TC-induction principle : setTC-induction.
Aczel proves that the type-theoric interpretation of CZF also satisfies the
REA ("Regular Extension Axiom").
We prove that in Nuprl: RegularExtension.
Aczel uses that to prove the existence of inductively defined sets
where the inductive definition is "bounded".
See Error :bounded-inductive-definition
.
⋅
Definition: coSet
coSet{i:l} == coW(Type;x.x)
Lemma: coSet_wf
coSet{i:l} ∈ 𝕌'
Lemma: coSet_subtype
coSet{i:l} ⊆r (T:Type × (T ⟶ coSet{i:l}))
Lemma: subtype_coSet
(T:Type × (T ⟶ coSet{i:l})) ⊆r coSet{i:l}
Lemma: coSet-subtype-corec
coSet{i:l} ⊆r corec(T.a:Type × (a ⟶ T))
Lemma: corec-subtype-coSet
corec(T.a:Type × (a ⟶ T)) ⊆r coSet{i:l}
Lemma: coSet-corec
coSet{i:l} ≡ corec(T.a:Type × (a ⟶ T))
Definition: mk-coset
mk-coset(T;f) == <T, f>
Lemma: mk-coset_wf
∀[T:Type]. ∀[f:T ⟶ coSet{i:l}]. (mk-coset(T;f) ∈ coSet{i:l})
Definition: set-dom
set-dom(s) == fst(s)
Lemma: set-dom_wf
∀[s:coSet{i:l}]. (set-dom(s) ∈ Type)
Definition: set-item
set-item(s;x) == (snd(s)) x
Lemma: set-item_wf
∀[s:coSet{i:l}]. ∀[x:set-dom(s)]. (set-item(s;x) ∈ coSet{i:l})
Definition: set-eq
set-eq(s;s') ==
νR.λs,s'. ((∀i:set-dom(s). ∃j:set-dom(s'). (R set-item(s;i) set-item(s';j)))
∧ (∀j:set-dom(s'). ∃i:set-dom(s). (R set-item(s;i) set-item(s';j))))
s
s'
Lemma: set-eq_wf
∀[s,s':coSet{i:l}]. (set-eq(s;s') ∈ ℙ)
Definition: seteq
seteq(s1;s2) == coW-equiv(T.T;s1;s2)
Lemma: seteq_wf
∀[s1,s2:coSet{i:l}]. (seteq(s1;s2) ∈ ℙ)
Lemma: seteq-equiv
EquivRel(coSet{i:l};x,y.seteq(x;y))
Definition: coSet-bisimulation
coSet-bisimulation{i:l}(x,y.R[x; y]) ==
∀T:𝕌'
((((a:Type × (a ⟶ T)) ⊆r T) ∧ (coSet{i:l} ⊆r T))
⇒ (∀x,y:coSet{i:l}. (R[x; y] ⇒ (x = y ∈ T)))
⇒ (∀x,y:coSet{i:l}. (R[x; y] ⇒ (x = y ∈ (a:Type × (a ⟶ T))))))
Lemma: coSet-bisimulation_wf
∀[R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ']. (coSet-bisimulation{i:l}(x,y.R[x;y]) ∈ ℙ{i''})
Lemma: coSet-equality
∀x,y:coSet{i:l}.
(x = y ∈ coSet{i:l} ⇐⇒ ∃R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'. (coSet-bisimulation{i:l}(x,y.R[x;y]) ∧ R[x;y]))
Lemma: coSet-equality2
∀x,y:coSet{i:l}.
((∀T:𝕌'. ((((a:Type × (a ⟶ T)) ⊆r T) ∧ (coSet{i:l} ⊆r T)) ⇒ (x = y ∈ T) ⇒ (x = y ∈ (a:Type × (a ⟶ T)))))
⇒ (x = y ∈ coSet{i:l}))
Definition: setmem
(x ∈ s) == coWmem(T.T;x;s)
Lemma: setmem_wf
∀[x,s:coSet{i:l}]. ((x ∈ s) ∈ ℙ)
Lemma: setmem-iff
∀x,s:coSet{i:l}. ((x ∈ s) ⇐⇒ ∃t:set-dom(s). seteq(x;set-item(s;t)))
Lemma: set-item-mem
∀s:coSet{i:l}. ∀x:set-dom(s). (set-item(s;x) ∈ s)
Lemma: co-seteq-iff
∀x,y:coSet{i:l}. (seteq(x;y) ⇐⇒ ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ (z ∈ y)))
Lemma: setmem-mk-coset
∀[T,f,x:Top]. ((x ∈ mk-coset(T;f)) ~ ∃t:T. seteq(x;f t))
Definition: comem
comem{i:l}(x;s) == ∃t:set-dom(s). (x = set-item(s;t) ∈ coSet{i:l})
Lemma: comem_wf
∀[s,x:coSet{i:l}]. (comem{i:l}(x;s) ∈ ℙ')
Lemma: fix_wf_coSet
∀[G:⋂W:𝕌'. (W ⟶ (T:Type × (T ⟶ W)))]. (fix(G) ∈ coSet{i:l})
Lemma: fix_wf_coSet_system
∀[I:𝕌']. ∀[G:⋂C:{C:𝕌'| ((T:Type × (T ⟶ C)) ⊆r C) ∧ (coSet{i:l} ⊆r C)} . ((I ⟶ C) ⟶ I ⟶ (T:Type × (T ⟶ C)))].
(fix(G) ∈ I ⟶ coSet{i:l})
Lemma: fix_wf_coSet_system_weak
∀[I:𝕌']. ∀[G:⋂C:𝕌'. ((I ⟶ C) ⟶ I ⟶ (T:Type × (T ⟶ C)))]. (fix(G) ∈ I ⟶ coSet{i:l})
Definition: graph-cosets
graph-cosets(I;i,j.E[i; j]) == fix((λS,i. <j:I × E[i; j], λp.(S (fst(p)))>))
Lemma: graph-cosets_wf
∀[I:Type]. ∀[E:I ⟶ I ⟶ ℙ]. (graph-cosets(I;i,j.E[i;j]) ∈ I ⟶ coSet{i:l})
Lemma: comem-graph-cosets
∀[I:Type]. ∀[E:I ⟶ I ⟶ ℙ].
∀i:I. ∀x:coSet{i:l}.
(comem{i:l}(x;graph-cosets(I;i,j.E[i;j]) i) ⇐⇒ ∃j:I. (E[i;j] ∧ (x = (graph-cosets(I;i,j.E[i;j]) j) ∈ coSet{i:l})))
Definition: loopset
loopset() == fix((λS.<Unit, λp.S>))
Lemma: loopset_wf
loopset() ∈ coSet{i:l}
Lemma: loopset-sq
loopset() ~ mk-coset(Unit;λp.loopset())
Definition: Set
Set{i:l} == W(Type;x.x)
Lemma: Set_wf
Set{i:l} ∈ 𝕌'
Lemma: set-ext
Set{i:l} ≡ T:Type × (T ⟶ Set{i:l})
Lemma: subtype-set
(T:Type × (T ⟶ Set{i:l})) ⊆r Set{i:l}
Lemma: set-subtype
Set{i:l} ⊆r (T:Type × (T ⟶ Set{i:l}))
Lemma: set-subtype-coSet
Set{i:l} ⊆r coSet{i:l}
Definition: mkset
{f[t] | t ∈ T} == <T, λt.f[t]>
Lemma: mkset_wf
∀[T:Type]. ∀[f:T ⟶ Set{i:l}]. ({f[t] | t ∈ T} ∈ Set{i:l})
Definition: mk-set
f"(T) == Wsup(T;f)
Lemma: mk-set_wf
∀[T:Type]. ∀[f:T ⟶ Set{i:l}]. (f"(T) ∈ Set{i:l})
Lemma: dom_mk_set_lemma
∀f,T:Top. (set-dom(f"(T)) ~ T)
Lemma: item_mk_set_lemma
∀x,f,T:Top. (set-item(f"(T);x) ~ f x)
Lemma: set-induction-1
∀[P:Set{i:l} ⟶ ℙ']. ((∀T:Type. ∀f:T ⟶ Set{i:l}. ((∀t:T. P[f[t]]) ⇒ P[f"(T)])) ⇒ (∀s:Set{i:l}. P[s]))
Lemma: set-induction-1-ext
∀[P:Set{i:l} ⟶ ℙ']. ((∀T:Type. ∀f:T ⟶ Set{i:l}. ((∀t:T. P[f[t]]) ⇒ P[f"(T)])) ⇒ (∀s:Set{i:l}. P[s]))
Definition: Set-ind
Set-ind() == λh,s. W_ind(λa,f,x. (h a f x);s)
Lemma: Set-ind_wf
Set-ind() ∈ ∀[P:Set{i:l} ⟶ ℙ']. ((∀T:Type. ∀f:T ⟶ Set{i:l}. ((∀t:T. P[f[t]]) ⇒ P[f"(T)])) ⇒ (∀s:Set{i:l}. P[s]))
Lemma: set-induction
∀[P:Set{i:l} ⟶ ℙ']. ((∀T:Type. ∀f:T ⟶ Set{i:l}. ((∀t:T. P[f[t]]) ⇒ P[f"(T)])) ⇒ (∀s:Set{i:l}. P[s]))
Definition: isSet
isSet(w) == coW-wfdd(x.x;w)
Lemma: isSet_wf
∀[a:coSet{i:l}]. (isSet(a) ∈ ℙ)
Lemma: isSet_functionality
∀a1,a2:coSet{i:l}. (seteq(a1;a2) ⇒ (isSet(a1) ⇐⇒ isSet(a2)))
Lemma: coSet-is-Set
∀[a:coSet{i:l}]. a ∈ Set{i:l} supposing isSet(a)
Lemma: Set-isSet
∀[a:Set{i:l}]. isSet(a)
Lemma: coSet-seteq-Set
∀[s:Set{i:l}]. ∀[z:coSet{i:l}]. z ∈ Set{i:l} supposing seteq(z;s)
Lemma: set-item_wf2
∀[s:Set{i:l}]. ∀[t:set-dom(s)]. (set-item(s;t) ∈ Set{i:l})
Lemma: seteqweaken1
∀s1,s2:coSet{i:l}. ((s1 = s2 ∈ coSet{i:l}) ⇒ seteq(s1;s2))
Lemma: seteqweaken1_ext
∀s1,s2:coSet{i:l}. ((s1 = s2 ∈ coSet{i:l}) ⇒ seteq(s1;s2))
Definition: seteqweaken
seteqweaken(s2) ==
λ_,moves. let u,v = moves[||moves|| - 2]
in let u',v' = moves[||moves|| - 1]
in if copath-length(u) <z copath-length(u') then <u', u'> else <v', v'> fi
Lemma: seteqweaken_wf
∀s1,s2:coSet{i:l}. (seteqweaken(s2) ∈ (s1 = s2 ∈ coSet{i:l}) ⇒ seteq(s1;s2))
Lemma: seteq_weakening
∀s1,s2:coSet{i:l}. ((s1 = s2 ∈ coSet{i:l}) ⇒ seteq(s1;s2))
Lemma: seteqinv1
∀s1,s2:coSet{i:l}. (seteq(s1;s2) ⇒ seteq(s2;s1))
Lemma: seteqinv1_ext
∀s1,s2:coSet{i:l}. (seteq(s1;s2) ⇒ seteq(s2;s1))
Definition: seteqinv
seteqinv() == λ_,f,eq,moves. let u,v = eq λp.let u,v = p in <v, u> o moves in <v, u>
Lemma: seteqinv_wf
seteqinv() ∈ ∀s1,s2:coSet{i:l}. (seteq(s1;s2) ⇒ seteq(s2;s1))
Lemma: seteq_inversion
∀s1,s2:coSet{i:l}. (seteq(s1;s2) ⇒ seteq(s2;s1))
Lemma: seteqtrans1
∀s1,s2,s3:coSet{i:l}. (seteq(s1;s2) ⇒ seteq(s2;s3) ⇒ seteq(s1;s3))
Lemma: seteqtrans1_ext
∀s1,s2,s3:coSet{i:l}. (seteq(s1;s2) ⇒ seteq(s2;s3) ⇒ seteq(s1;s3))
Definition: seteqtrans
seteqtrans() == λ_,_,_,eq1,eq2. coW-trans(eq1; eq2)
Lemma: seteqtrans_wf
seteqtrans() ∈ ∀s1,s2,s3:coSet{i:l}. (seteq(s1;s2) ⇒ seteq(s2;s3) ⇒ seteq(s1;s3))
Lemma: seteq_transitivity
∀s1,s2,s3:coSet{i:l}. (seteq(s1;s2) ⇒ seteq(s2;s3) ⇒ seteq(s1;s3))
Lemma: seteq_equiv
EquivRel(coSet{i:l};s1,s2.seteq(s1;s2))
Lemma: seteq_functionality
∀x1,x2,y1,y2:coSet{i:l}. (seteq(x1;x2) ⇒ seteq(y1;y2) ⇒ (seteq(x1;y1) ⇐⇒ seteq(x2;y2)))
Lemma: setmemfunclemma
∀x1,s1,x2,s2:coSet{i:l}. (seteq(x1;x2) ⇒ seteq(s1;s2) ⇒ {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})
Lemma: setmemfunclemma_ext
∀x1,s1,x2,s2:coSet{i:l}. (seteq(x1;x2) ⇒ seteq(s1;s2) ⇒ {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})
Definition: setmemfunc
setmemfunc(x1; s1; x2; s2) ==
λ%,%1. <λ%5.let x,y = s2
in let b,y1 = %5
in let q1,y2 = %1
<2
, λi.if i=0
then <(), ()>
else if i - 1=0 then <copath-cons(b;()), ()> else (⋅ (i - 1 - 1))
>
in <copath-hd(y2)
, seteqtrans() x2 x1 (y copath-hd(y2)) (seteqinv() x1 x2 %)
coW-trans(y1;
λmoves.let u,v = %1
let k,g = moves
in <(k + 1) + 1
, λi.if i=0
then <(), ()>
else if i - 1=0
then <copath-cons(b;()), ()>
else let u,v = g (i - 1 - 1)
in <copath-cons(b;u)
, copath-cons(copath-hd(y2);v)
>
>
in <copath-tl(u), copath-tl(v)>)
>
, λ%5.let x,y = s1
in let b,y1 = %5
in let u,y2 = %1
<2
, λi.if i=0
then <(), ()>
else if i - 1=0 then <(), copath-cons(b;())> else let u,v = ⋅ (i - 1 - 1) in <v, u>
>
in <copath-hd(u)
, seteqtrans() x1 x2 (y copath-hd(u)) %
coW-trans(y1;
λmoves.let u,v = %1
let k,g = moves
in <(k + 1) + 1
, λi.if i=0
then <(), ()>
else if i - 1=0
then <(), copath-cons(b;())>
else let u@0,v = g (i - 1 - 1)
in <copath-cons(copath-hd(u);v)
, copath-cons(b;u@0)
>
>
in <copath-tl(v), copath-tl(u)>)
>
>
Lemma: setmemfunc_wf
∀[x1,s1,x2,s2:coSet{i:l}]. (setmemfunc(x1; s1; x2; s2) ∈ seteq(x1;x2) ⇒ seteq(s1;s2) ⇒ {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})
Lemma: setmem_functionality
∀x1,s1,x2,s2:coSet{i:l}. (seteq(x1;x2) ⇒ seteq(s1;s2) ⇒ {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})
Lemma: setmem_functionality_1
∀s,x1,x2:coSet{i:l}. (seteq(x1;x2) ⇒ ((x1 ∈ s) ⇐⇒ (x2 ∈ s)))
Lemma: coSet-mem-Set-implies-Set
∀[z:coSet{i:l}]. z ∈ Set{i:l} supposing ∃s:Set{i:l}. (z ∈ s)
Lemma: coSet-subtype-Set
∀B:Set{i:l}. ({u:coSet{i:l}| (u ∈ B)} ⊆r Set{i:l})
Lemma: seteq-iff
∀s1,s2:Set{i:l}. (seteq(s1;s2) ⇐⇒ ∀x:Set{i:l}. ((x ∈ s1) ⇐⇒ (x ∈ s2)))
Lemma: setmem-irreflexive
∀s:Set{i:l}. (¬(s ∈ s))
Lemma: setmem-mk-set-sq
∀[T,f,x:Top]. ((x ∈ f"(T)) ~ ∃b:T. seteq(x;f b))
Lemma: setmem-mkset-sq
∀[T,f,x:Top]. ((x ∈ {f[b] | b ∈ T}) ~ ∃b:T. seteq(x;f[b]))
Lemma: setmem-mk-set
∀T:Type. ∀f:T ⟶ Set{i:l}. ∀t:T. (f t ∈ f"(T))
Lemma: setmem-coset
∀T:Type. ∀f:T ⟶ coSet{i:l}. ∀t:T. (f t ∈ mk-coset(T;f))
Lemma: setmem-loopset
∀z:coSet{i:l}. ((z ∈ loopset()) ⇐⇒ seteq(z;loopset()))
Definition: set-predicate
set-predicate{i:l}(s;a.P[a]) == ∀a1,a2:coSet{i:l}. ((a1 ∈ s) ⇒ (a2 ∈ s) ⇒ seteq(a1;a2) ⇒ P[a1] ⇒ P[a2])
Lemma: set-predicate_wf
∀[s:coSet{i:l}]. ∀[P:{x:coSet{i:l}| (x ∈ s)} ⟶ ℙ']. (set-predicate{i:l}(s;x.P[x]) ∈ ℙ')
Lemma: set-predicate_wf2
∀[s:Set{i:l}]. ∀[P:{x:Set{i:l}| (x ∈ s)} ⟶ ℙ']. (set-predicate{i:l}(s;x.P[x]) ∈ ℙ')
Lemma: set-predicate-iff
∀[s:Set{i:l}]. ∀[P:{x:Set{i:l}| (x ∈ s)} ⟶ ℙ'].
(set-predicate{i:l}(s;x.P[x]) ⇐⇒ ∀a1,a2:Set{i:l}. ((a1 ∈ s) ⇒ (a2 ∈ s) ⇒ seteq(a1;a2) ⇒ P[a1] ⇒ P[a2]))
Lemma: isSet-set-predicate
∀s:coSet{i:l}. set-predicate{i:l}(s;x.isSet(x))
Definition: sub-set
{a ∈ s | P[a]} == let T,f = s in <t:T × P[f t], λp.(f (fst(p)))>
Lemma: sub-set_wf
∀[s:coSet{i:l}]. ∀[P:{a:coSet{i:l}| (a ∈ s)} ⟶ ℙ]. ({a ∈ s | P[a]} ∈ coSet{i:l})
Lemma: sub-set_wf2
∀[s:Set{i:l}]. ∀[P:{a:Set{i:l}| (a ∈ s)} ⟶ ℙ]. ({a ∈ s | P[a]} ∈ Set{i:l})
Lemma: setmem-sub-set
∀s:Set{i:l}
∀[P:{a:Set{i:l}| (a ∈ s)} ⟶ ℙ]
(set-predicate{i:l}(s;a.P[a]) ⇒ (∀a:Set{i:l}. ((a ∈ {a ∈ s | P[a]}) ⇐⇒ (a ∈ s) ∧ P[a])))
Lemma: setmem-sub-coset
∀s:coSet{i:l}
∀[P:{a:coSet{i:l}| (a ∈ s)} ⟶ ℙ]
(set-predicate{i:l}(s;a.P[a]) ⇒ (∀a:coSet{i:l}. ((a ∈ {a ∈ s | P[a]}) ⇐⇒ (a ∈ s) ∧ P[a])))
Definition: set-function
set-function{i:l}(s; x.f[x]) == ∀x,y:coSet{i:l}. ((x ∈ s) ⇒ (y ∈ s) ⇒ seteq(x;y) ⇒ seteq(f[x];f[y]))
Lemma: set-function_wf
∀[s:coSet{i:l}]. ∀[f:{x:coSet{i:l}| (x ∈ s)} ⟶ coSet{i:l}]. (set-function{i:l}(s; x.f[x]) ∈ ℙ')
Definition: set-part
set-part(s) == {x ∈ s | isSet(x)}
Lemma: set-part_wf
∀[s:coSet{i:l}]. (set-part(s) ∈ Set{i:l})
Lemma: setmem-set-part
∀s,x:coSet{i:l}. ((x ∈ set-part(s)) ⇐⇒ (x ∈ s) ∧ isSet(x))
Definition: setunionfun
⋃x∈s.f[x] == let T,g = s in <t:T × set-dom(f[g t]), λp.let t,d = p in set-item(f[g t];d)>
Lemma: setunionfun_wf
∀[s:coSet{i:l}]. ∀[f:{x:coSet{i:l}| (x ∈ s)} ⟶ coSet{i:l}]. ( ⋃x∈s.f[x] ∈ coSet{i:l})
Lemma: setunionfun_wf2
∀[s:Set{i:l}]. ∀[f:{x:Set{i:l}| (x ∈ s)} ⟶ Set{i:l}]. ( ⋃x∈s.f[x] ∈ Set{i:l})
Lemma: setmem-unionfun-implies
∀s:coSet{i:l}. ∀f:{x:coSet{i:l}| (x ∈ s)} ⟶ coSet{i:l}. ∀y:coSet{i:l}.
((y ∈ ⋃x∈s.f[x]) ⇒ (∃x:coSet{i:l}. ((x ∈ s) ∧ (y ∈ f[x]))))
Lemma: setmem-setunionfun
∀s:coSet{i:l}. ∀f:{x:coSet{i:l}| (x ∈ s)} ⟶ coSet{i:l}.
(set-function{i:l}(s; x.f[x]) ⇒ (∀y:coSet{i:l}. ((y ∈ ⋃x∈s.f[x]) ⇐⇒ ∃x:coSet{i:l}. ((x ∈ s) ∧ (y ∈ f[x])))))
Definition: unionset
⋃(s) == ⋃x∈s.x
Lemma: unionset_wf
∀[s:coSet{i:l}]. (⋃(s) ∈ coSet{i:l})
Lemma: unionset_wf2
∀[s:Set{i:l}]. (⋃(s) ∈ Set{i:l})
Lemma: setmem-unionset
∀s,x:coSet{i:l}. ((x ∈ ⋃(s)) ⇐⇒ ∃a:coSet{i:l}. ((a ∈ s) ∧ (x ∈ a)))
Lemma: unionset_functionality
∀a,b:coSet{i:l}. (seteq(a;b) ⇒ seteq(⋃(a);⋃(b)))
Lemma: setmem-mkset
∀T:Type. ∀f:T ⟶ Set{i:l}. ∀x:Set{i:l}. ((x ∈ {f[t] | t ∈ T}) ⇐⇒ ∃t:T. seteq(x;f[t]))
Definition: emptyset
{} == {⋅ | x ∈ Void}
Lemma: emptyset_wf
{} ∈ Set{i:l}
Lemma: setmem-emptyset
∀x:coSet{i:l}. ((x ∈ {}) ⇐⇒ False)
Definition: singleset
{a} == <Unit, λx.a>
Lemma: singleset_wf
∀[a:coSet{i:l}]. ({a} ∈ coSet{i:l})
Lemma: singleset_wf2
∀[a:Set{i:l}]. ({a} ∈ Set{i:l})
Lemma: setmem-singleset
∀a,x:coSet{i:l}. ((x ∈ {a}) ⇐⇒ seteq(x;a))
Lemma: singleset_functionality
∀a,b:coSet{i:l}. (seteq(a;b) ⇒ seteq({a};{b}))
Definition: singleitem
singleitem(s) == ⋃(s)
Lemma: singleitem_wf
∀[s:coSet{i:l}]. (singleitem(s) ∈ coSet{i:l})
Lemma: singleitem_wf2
∀[s:Set{i:l}]. (singleitem(s) ∈ Set{i:l})
Lemma: singleitem_functionality
∀a,b:coSet{i:l}. (seteq(a;b) ⇒ seteq(singleitem(a);singleitem(b)))
Lemma: singleitem-singleset
∀a:coSet{i:l}. seteq(singleitem({a});a)
Definition: pairset
{a,b} == <𝔹, λx.if x then a else b fi >
Lemma: pairset_wf
∀[a,b:coSet{i:l}]. ({a,b} ∈ coSet{i:l})
Lemma: pairset_wf2
∀[a,b:Set{i:l}]. ({a,b} ∈ Set{i:l})
Lemma: setmem-pairset
∀a,b,x:coSet{i:l}. ((x ∈ {a,b}) ⇐⇒ seteq(x;a) ∨ seteq(x;b))
Lemma: pairset_functionality
∀a,b,a',b':coSet{i:l}. (seteq(a;a') ⇒ seteq(b;b') ⇒ seteq({a,b};{a',b'}))
Definition: orderedpairset
(a,b) == {{a},{a,b}}
Lemma: orderedpairset_wf
∀[a,b:coSet{i:l}]. ((a,b) ∈ coSet{i:l})
Lemma: orderedpairset_wf2
∀[a,b:Set{i:l}]. ((a,b) ∈ Set{i:l})
Lemma: seteq-orderedpairs-iff
∀a,b,a',b':coSet{i:l}. (seteq((a,b);(a',b')) ⇐⇒ seteq(a;a') ∧ seteq(b;b'))
Lemma: orderedpairset_functionality
∀a,b,a',b':coSet{i:l}. (seteq(a;a') ⇒ seteq(b;b') ⇒ seteq((a,b);(a',b')))
Definition: set-add
a + b == let T,f = a in let S,g = b in <T + S, λx.case x of inl(t) => f t | inr(s) => g s>
Lemma: set-add_wf
∀[a,b:coSet{i:l}]. (a + b ∈ coSet{i:l})
Lemma: set-add_wf2
∀[a,b:Set{i:l}]. (a + b ∈ Set{i:l})
Lemma: setmem-set-add
∀a,b,x:coSet{i:l}. ((x ∈ a + b) ⇐⇒ (x ∈ a) ∨ (x ∈ b))
Lemma: set-add_functionality
∀a,b,a',b':coSet{i:l}. (seteq(a;a') ⇒ seteq(b;b') ⇒ seteq(a + b;a' + b'))
Definition: plus-set
(a)+ == {a} + a
Lemma: plus-set_wf
∀[a:coSet{i:l}]. ((a)+ ∈ coSet{i:l})
Lemma: plus-set_wf2
∀[a:Set{i:l}]. ((a)+ ∈ Set{i:l})
Lemma: setmem-plus-set
∀a,x:coSet{i:l}. ((x ∈ (a)+) ⇐⇒ (x ∈ a) ∨ seteq(x;a))
Lemma: plus-set_functionality
∀a,a':coSet{i:l}. (seteq(a;a') ⇒ seteq((a)+;(a')+))
Definition: cosetTC
cosetTC(a) == mk-coset({p:copath(T.T;a)| 0 < copath-length(p)} ;λp.copath-at(a;p))
Lemma: cosetTC_wf
∀[a:coSet{i:l}]. (cosetTC(a) ∈ coSet{i:l})
Lemma: cosetTC_wf2
∀[a:Set{i:l}]. (cosetTC(a) ∈ Set{i:l})
Definition: setTC
setTC(a) == a + ⋃x∈a.setTC(x)
Lemma: setTC_wf
∀[a:Set{i:l}]. (setTC(a) ∈ Set{i:l})
Definition: allsetmem
∀a∈A.P[a] == ∀i:set-dom(A). P[set-item(A;i)]
Lemma: allsetmem_wf
∀[A:coSet{i:l}]. ∀[P:{a:coSet{i:l}| (a ∈ A)} ⟶ ℙ]. (∀a∈A.P[a] ∈ ℙ)
Lemma: implies-allsetmem
∀A:coSet{i:l}. ∀[P:{a:coSet{i:l}| (a ∈ A)} ⟶ ℙ]. ((∀a:coSet{i:l}. ((a ∈ A) ⇒ P[a])) ⇒ ∀a∈A.P[a])
Lemma: allsetmem-iff
∀A:coSet{i:l}
∀[P:{a:coSet{i:l}| (a ∈ A)} ⟶ ℙ]. (set-predicate{i:l}(A;a.P[a]) ⇒ (∀a∈A.P[a] ⇐⇒ ∀a:coSet{i:l}. ((a ∈ A) ⇒ P[a])))
Lemma: allsetmem_functionality
∀A:coSet{i:l}. ∀P:{a:coSet{i:l}| (a ∈ A)} ⟶ ℙ. ∀B:coSet{i:l}.
(set-predicate{i:l}(A;a.P[a]) ⇒ seteq(A;B) ⇒ (∀a∈A.P[a] ⇐⇒ ∀a∈B.P[a]))
Definition: existssetmem
∃a∈A.P[a] == ∃i:set-dom(A). P[set-item(A;i)]
Lemma: existssetmem_wf
∀[A:coSet{i:l}]. ∀[P:{a:coSet{i:l}| (a ∈ A)} ⟶ ℙ]. (∃a∈A.P[a] ∈ ℙ)
Lemma: existssetmem-implies
∀A:coSet{i:l}. ∀[P:{a:coSet{i:l}| (a ∈ A)} ⟶ ℙ]. (∃a∈A.P[a] ⇒ (∃a:coSet{i:l}. ((a ∈ A) ∧ P[a])))
Lemma: existssetmem-iff
∀A:coSet{i:l}
∀[P:{a:coSet{i:l}| (a ∈ A)} ⟶ ℙ]. (set-predicate{i:l}(A;a.P[a]) ⇒ (∃a∈A.P[a] ⇐⇒ ∃a:coSet{i:l}. ((a ∈ A) ∧ P[a])))
Lemma: existssetmem_functionality
∀A:coSet{i:l}. ∀P:{a:coSet{i:l}| (a ∈ A)} ⟶ ℙ. ∀B:coSet{i:l}.
(set-predicate{i:l}(A;a.P[a]) ⇒ seteq(A;B) ⇒ (∃a∈A.P[a] ⇐⇒ ∃a∈B.P[a]))
Definition: intersectionset
⋂(s) == {x ∈ ⋃(s) | ∀z∈s.(x ∈ z)}
Lemma: intersectionset_wf
∀[s:coSet{i:l}]. (⋂(s) ∈ coSet{i:l})
Lemma: intersectionset_wf2
∀[s:Set{i:l}]. (⋂(s) ∈ Set{i:l})
Lemma: setmem-intersectionset
∀s,x:coSet{i:l}. ((∃a:coSet{i:l}. (a ∈ s)) ⇒ ((x ∈ ⋂(s)) ⇐⇒ ∀z:coSet{i:l}. ((z ∈ s) ⇒ (x ∈ z))))
Lemma: intersectionset_functionality
∀a,b:coSet{i:l}. (seteq(a;b) ⇒ seteq(⋂(a);⋂(b)))
Definition: setsubset
(a ⊆ b) == ∀x∈a.(x ∈ b)
Lemma: setsubset_wf
∀[a,b:coSet{i:l}]. ((a ⊆ b) ∈ ℙ)
Lemma: setsubset-iff
∀a,b:coSet{i:l}. ((a ⊆ b) ⇐⇒ ∀x:coSet{i:l}. ((x ∈ a) ⇒ (x ∈ b)))
Lemma: setsubset-iff2
∀a:Set{i:l}. ∀b:coSet{i:l}. ((a ⊆ b) ⇐⇒ ∀x:Set{i:l}. ((x ∈ a) ⇒ (x ∈ b)))
Lemma: setsubset_functionality
∀a,b,a',b':coSet{i:l}. (seteq(a;a') ⇒ seteq(b;b') ⇒ ((a ⊆ b) ⇐⇒ (a' ⊆ b')))
Lemma: seteq-iff-setsubset
∀a,b:coSet{i:l}. (seteq(a;b) ⇐⇒ (a ⊆ b) ∧ (b ⊆ a))
Lemma: setsubset_transitivity
∀a,b,c:coSet{i:l}. ((a ⊆ b) ⇒ (b ⊆ c) ⇒ (a ⊆ c))
Lemma: set-part-greatest
∀s:coSet{i:l}. ((set-part(s) ⊆ s) ∧ (∀x:Set{i:l}. ((x ⊆ s) ⇒ (x ⊆ set-part(s)))))
Lemma: cosetTC_functionality_subset
∀a,b:coSet{i:l}. ((a ⊆ b) ⇒ (cosetTC(a) ⊆ cosetTC(b)))
Lemma: cosetTC_functionality
∀a,b:coSet{i:l}. (seteq(a;b) ⇒ seteq(cosetTC(a);cosetTC(b)))
Lemma: cosetTC-set-function
∀s:coSet{i:l}. set-function{i:l}(s; a.cosetTC(a))
Lemma: cosetTC-contains
∀a:coSet{i:l}. (a ⊆ cosetTC(a))
Definition: orderedpair-fsts
orderedpair-fsts(pr) == ⋂(pr)
Lemma: orderedpair-fsts_wf
∀[pr:coSet{i:l}]. (orderedpair-fsts(pr) ∈ coSet{i:l})
Lemma: orderedpair-fsts_wf2
∀[pr:Set{i:l}]. (orderedpair-fsts(pr) ∈ Set{i:l})
Lemma: orderedpair-fsts_functionality
∀a,b:coSet{i:l}. (seteq(a;b) ⇒ seteq(orderedpair-fsts(a);orderedpair-fsts(b)))
Lemma: orderedpair-first
∀a,b:coSet{i:l}. seteq(orderedpair-fsts((a,b));{a})
Definition: orderedpair-fst
fst(pr) == singleitem(orderedpair-fsts(pr))
Lemma: orderedpair-fst_wf
∀[pr:coSet{i:l}]. (fst(pr) ∈ coSet{i:l})
Lemma: orderedpair-fst_wf2
∀[pr:Set{i:l}]. (fst(pr) ∈ Set{i:l})
Lemma: orderedpair-fst_functionality
∀a,b:coSet{i:l}. (seteq(a;b) ⇒ seteq(fst(a);fst(b)))
Lemma: fst-orderedpairset
∀a,b:coSet{i:l}. seteq(fst((a,b));a)
Definition: orderedpair-snds
snds(pr) == {x ∈ ⋃(pr) | seteq(pr;(fst(pr),x))}
Lemma: orderedpair-snds_wf
∀[pr:coSet{i:l}]. (snds(pr) ∈ coSet{i:l})
Lemma: orderedpair-snds_wf2
∀[pr:Set{i:l}]. (snds(pr) ∈ Set{i:l})
Lemma: orderedpair-snds_functionality
∀a,b:coSet{i:l}. (seteq(a;b) ⇒ seteq(snds(a);snds(b)))
Lemma: orderedpair-second
∀a,b:coSet{i:l}. seteq(snds((a,b));{b})
Definition: orderedpair-snd
snd(pr) == singleitem(snds(pr))
Lemma: orderedpair-snd_wf
∀[pr:coSet{i:l}]. (snd(pr) ∈ coSet{i:l})
Lemma: orderedpair-snd_wf2
∀[pr:Set{i:l}]. (snd(pr) ∈ Set{i:l})
Lemma: orderedpair-snd_functionality
∀a,b:coSet{i:l}. (seteq(a;b) ⇒ seteq(snd(a);snd(b)))
Lemma: snd-orderedpairset
∀a,b:coSet{i:l}. seteq(snd((a,b));b)
Definition: transitive-set
We define ⌜transitive-set(s)⌝ using the ∀x∈s..... so that it will have
type ⌜ℙ⌝ rather than ⌜ℙ'⌝ (universe i+1)
if had been defined: ∀x:Set{i:l}. ((x ∈ s) ⇒ (x ⊆ s)).
But these are equivalent. See transitive-set-iff.⋅
transitive-set(s) == ∀x∈s.(x ⊆ s)
Lemma: transitive-set_wf
∀[s:coSet{i:l}]. (transitive-set(s) ∈ ℙ)
Lemma: transitive-set-iff
∀s:coSet{i:l}. (transitive-set(s) ⇐⇒ ∀x:coSet{i:l}. ((x ∈ s) ⇒ (x ⊆ s)))
Lemma: transitive-set-iff2
∀s:Set{i:l}. (transitive-set(s) ⇐⇒ ∀x:Set{i:l}. ((x ∈ s) ⇒ (x ⊆ s)))
Lemma: transitive-set_functionality
∀s1,s2:coSet{i:l}. (seteq(s1;s2) ⇒ (transitive-set(s1) ⇐⇒ transitive-set(s2)))
Lemma: plus-set-transitive
∀a:coSet{i:l}. (transitive-set(a) ⇒ transitive-set((a)+))
Lemma: emptyset-transitive
transitive-set({})
Lemma: loopset-transitive
transitive-set(loopset())
Definition: natset
natset(n) == primrec(n;{};λi,r. (r)+)
Lemma: natset_wf
∀[n:ℕ]. (natset(n) ∈ Set{i:l})
Lemma: natset-transitive
∀n:ℕ. transitive-set(natset(n))
Lemma: setmem-natset
∀n:ℕ. ∀x:Set{i:l}. ((x ∈ natset(n)) ⇐⇒ ∃i:ℕn. seteq(x;natset(i)))
Lemma: natset-setmem-natset
∀n,m:ℕ. ((natset(n) ∈ natset(m)) ⇐⇒ n < m)
Lemma: natset-subset-natset
∀n,m:ℕ. ((natset(n) ⊆ natset(m)) ⇐⇒ n ≤ m)
Lemma: natset-seteq-natset
∀n,m:ℕ. (seteq(natset(n);natset(m)) ⇐⇒ n = m ∈ ℤ)
Definition: omegaset
omegaset() == {natset(n) | n ∈ ℕ}
Lemma: omegaset_wf
omegaset() ∈ Set{i:l}
Lemma: cosetTC-transitive
∀a:coSet{i:l}. transitive-set(cosetTC(a))
Lemma: cosetTC-least
∀a,s:coSet{i:l}. ((a ⊆ s) ⇒ transitive-set(s) ⇒ (cosetTC(a) ⊆ s))
Lemma: cosetTC-contained
∀s:coSet{i:l}. (transitive-set(s) ⇒ (cosetTC(s) ⊆ s))
Lemma: cosetTC-unique
∀a,s:coSet{i:l}.
((a ⊆ s)
⇒ transitive-set(s)
⇒ (∀s':coSet{i:l}. ((a ⊆ s') ⇒ transitive-set(s') ⇒ (s ⊆ s')))
⇒ seteq(s;cosetTC(a)))
Definition: transmem
(x ∈∈ y) == x TC(λx,y. (x ∈ y)) y
Lemma: transmem_wf
∀[x,y:coSet{i:l}]. ((x ∈∈ y) ∈ ℙ')
Lemma: setmem-transmem
∀x,y:coSet{i:l}. ((x ∈ y) ⇒ (x ∈∈ y))
Lemma: transmem_transitivity
Trans(coSet{i:l};x,y.(x ∈∈ y))
Lemma: setTC_functionality_subset
∀b,a:Set{i:l}. ((a ⊆ b) ⇒ (setTC(a) ⊆ setTC(b)))
Lemma: setTC_functionality
∀a,b:Set{i:l}. (seteq(a;b) ⇒ seteq(setTC(a);setTC(b)))
Lemma: setTC-set-function
∀s:Set{i:l}. set-function{i:l}(s; a.setTC(a))
Lemma: setTC-contains
∀a:Set{i:l}. (a ⊆ setTC(a))
Lemma: setTC-transitive
∀a:Set{i:l}. transitive-set(setTC(a))
Lemma: setTC-least
∀a:Set{i:l}. ∀s:coSet{i:l}. ((a ⊆ s) ⇒ transitive-set(s) ⇒ (setTC(a) ⊆ s))
Lemma: setTC-unique
∀a,s:Set{i:l}.
((a ⊆ s) ⇒ transitive-set(s) ⇒ (∀s':Set{i:l}. ((a ⊆ s') ⇒ transitive-set(s') ⇒ (s ⊆ s'))) ⇒ seteq(s;setTC(a)))
Lemma: setTC-cosetTC
∀a:Set{i:l}. seteq(setTC(a);cosetTC(a))
Lemma: setTC-induction
∀[P:Set{i:l} ⟶ ℙ']. ((∀a:Set{i:l}. ((∀x:Set{i:l}. ((x ∈ setTC(a)) ⇒ P[x])) ⇒ P[a])) ⇒ (∀s:Set{i:l}. P[s]))
Definition: productset
a x b == let A,f = a in let B,g = b in <A × B, λp.let x,y = p in (f x,g y)>
Lemma: productset_wf
∀[a,b:coSet{i:l}]. (a x b ∈ coSet{i:l})
Lemma: productset_wf2
∀[a,b:Set{i:l}]. (a x b ∈ Set{i:l})
Lemma: setmem-productset
∀a,b,p:coSet{i:l}. ((p ∈ a x b) ⇐⇒ ∃u,v:coSet{i:l}. ((u ∈ a) ∧ (v ∈ b) ∧ seteq(p;(u,v))))
Definition: sigmaset
Σa:A.B[a] == let T,f = A in <t:T × set-dom(B[f t]), λp.let t,s = p in (f t,set-item(B[f t];s))>
Lemma: sigmaset_wf
∀[A:coSet{i:l}]. ∀[B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}]. (Σa:A.B[a] ∈ coSet{i:l})
Lemma: sigmaset_wf2
∀[A:Set{i:l}]. ∀[B:{a:Set{i:l}| (a ∈ A)} ⟶ Set{i:l}]. (Σa:A.B[a] ∈ Set{i:l})
Lemma: setmem-sigmaset
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}.
((∀a1,a2:coSet{i:l}. ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2])))
⇒ (∀x:coSet{i:l}. ((x ∈ Σa:A.B[a]) ⇐⇒ ∃a:coSet{i:l}. ((a ∈ A) ∧ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ seteq(x;(a,b))))))))
Definition: piset
piset(A;a.B[a]) == let T,f = A in <t:T ⟶ set-dom(B[f t]), λg.<T, λt.(f t,set-item(B[f t];g t))>>
Lemma: piset_wf
∀[A:coSet{i:l}]. ∀[B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}]. (piset(A;a.B[a]) ∈ coSet{i:l})
Lemma: piset_wf2
∀[A:Set{i:l}]. ∀[B:{a:Set{i:l}| (a ∈ A)} ⟶ Set{i:l}]. (piset(A;a.B[a]) ∈ Set{i:l})
Lemma: setmem-piset-1
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}. ∀x:coSet{i:l}.
((x ∈ piset(A;a.B[a]))
⇐⇒ ∃f:t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃t:set-dom(A). seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];f t)))))
Lemma: implies-setmem-piset
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}. ∀x:coSet{i:l}.
((∀a1,a2:coSet{i:l}. ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2])))
⇒ ((x ⊆ Σa:A.B[a])
∧ (∀a:coSet{i:l}. ((a ∈ A) ⇒ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ x)))))
∧ (∀a,b1,b2:coSet{i:l}. ((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2))))
⇒ (x ∈ piset(A;a.B[a])))
Lemma: setmem-piset-implies
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}. ∀x:coSet{i:l}.
((∀a1,a2:coSet{i:l}. ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2])))
⇒ (x ∈ piset(A;a.B[a]))
⇒ ((x ⊆ Σa:A.B[a]) ∧ (∀a:coSet{i:l}. ((a ∈ A) ⇒ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ x)))))))
Definition: singlevalued-graph
singlevalued-graph(A;a.B[a];grph) == ∀a∈A.∀b1∈B[a].∀b2∈B[a].((a,b1) ∈ grph) ⇒ ((a,b2) ∈ grph) ⇒ seteq(b1;b2)
Lemma: singlevalued-graph_wf
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}. ∀x:coSet{i:l}. (singlevalued-graph(A;a.B[a];x) ∈ ℙ)
Lemma: singlevalued-graph-iff
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}.
((∀a1,a2:coSet{i:l}. ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2])))
⇒ (∀x:coSet{i:l}
(singlevalued-graph(A;a.B[a];x)
⇐⇒ ∀a,b1,b2:coSet{i:l}.
((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2)))))
Lemma: singlevalued-graph_functionality
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}.
((∀a1,a2:coSet{i:l}. ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2])))
⇒ (∀g1,g2:coSet{i:l}. (seteq(g1;g2) ⇒ (singlevalued-graph(A;a.B[a];g1) ⇐⇒ singlevalued-graph(A;a.B[a];g2)))))
Definition: Piset
Πa:A.B[a] == {g ∈ piset(A;a.B[a]) | singlevalued-graph(A;a.B[a];g)}
Lemma: Piset_wf
∀[A:coSet{i:l}]. ∀[B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}]. (Πa:A.B[a] ∈ coSet{i:l})
Lemma: Piset_wf2
∀[A:Set{i:l}]. ∀[B:{a:Set{i:l}| (a ∈ A)} ⟶ Set{i:l}]. (Πa:A.B[a] ∈ Set{i:l})
Definition: function-graph
function-graph{i:l}(A;a.B[a];grph) ==
(grph ⊆ Σa:A.B[a])
∧ (∀a:coSet{i:l}. ((a ∈ A) ⇒ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ grph)))))
∧ (∀a,b1,b2:coSet{i:l}.
((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ grph) ⇒ ((a,b2) ∈ grph) ⇒ seteq(b1;b2)))
Lemma: function-graph_wf
∀[A:coSet{i:l}]. ∀[B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}]. ∀[grph:coSet{i:l}].
(function-graph{i:l}(A;a.B[a];grph) ∈ ℙ')
Lemma: setmem-Piset
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}. ∀x:coSet{i:l}.
((∀a1,a2:coSet{i:l}. ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2])))
⇒ ((x ∈ Πa:A.B[a]) ⇐⇒ function-graph{i:l}(A;a.B[a];x)))
Definition: funset
A ⟶ B == Πa:A.B
Lemma: funset_wf
∀[A,B:coSet{i:l}]. (A ⟶ B ∈ coSet{i:l})
Lemma: funset_wf2
∀[A,B:Set{i:l}]. (A ⟶ B ∈ Set{i:l})
Lemma: setmem-funset
∀A,B,x:coSet{i:l}. ((x ∈ A ⟶ B) ⇐⇒ function-graph{i:l}(A;_.B;x))
Definition: imageset
imageset(B;f) == {b ∈ B | ∃pr∈f.seteq(b;snd(pr))}
Lemma: imageset_wf
∀[B,f:coSet{i:l}]. (imageset(B;f) ∈ coSet{i:l})
Lemma: imageset_wf2
∀[B,f:Set{i:l}]. (imageset(B;f) ∈ Set{i:l})
Lemma: setmem-imageset
∀B,f,x:coSet{i:l}. ((x ∈ imageset(B;f)) ⇐⇒ (x ∈ B) ∧ (∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(x;snd(pr)))))
Lemma: imageset_functionality
∀B1,B2,f1,f2:coSet{i:l}. (seteq(B1;B2) ⇒ seteq(f1;f2) ⇒ seteq(imageset(B1;f1);imageset(B2;f2)))
Definition: setimages
setimages(A;B) == ⋃f∈A ⟶ B.{imageset(B;f)}
Lemma: setimages_wf
∀[A,B:coSet{i:l}]. (setimages(A;B) ∈ coSet{i:l})
Lemma: setimages_wf2
∀[A,B:Set{i:l}]. (setimages(A;B) ∈ Set{i:l})
Lemma: setmem-setimages
∀A,B,x:coSet{i:l}.
((x ∈ setimages(A;B))
⇐⇒ ∃f:coSet{i:l}
(function-graph{i:l}(A;_.B;f) ∧ (∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr)))))))
Definition: itersetfun
itersetfun(s.G[s];a) == G[ ⋃x∈a.itersetfun(s.G[s];x)]
Lemma: itersetfun_wf
∀[G:Set{i:l} ⟶ Set{i:l}]. ∀[a:Set{i:l}]. (itersetfun(x.G[x];a) ∈ Set{i:l})
Lemma: itersetfun_functionality_subset
∀G:Set{i:l} ⟶ Set{i:l}
((∀a,b:Set{i:l}. ((a ⊆ b) ⇒ (G[a] ⊆ G[b])))
⇒ (∀b,a:Set{i:l}. ((a ⊆ b) ⇒ (itersetfun(x.G[x];a) ⊆ itersetfun(x.G[x];b)))))
Lemma: itersetfun_functionality
∀G:Set{i:l} ⟶ Set{i:l}
((∀a,b:Set{i:l}. ((a ⊆ b) ⇒ (G[a] ⊆ G[b])))
⇒ (∀b,a:Set{i:l}. (seteq(a;b) ⇒ seteq(itersetfun(x.G[x];a);itersetfun(x.G[x];b)))))
Lemma: itersetfun-subset-fixpoint
∀G:Set{i:l} ⟶ Set{i:l}
((∀a,b:Set{i:l}. ((a ⊆ b) ⇒ (G[a] ⊆ G[b])))
⇒ (∀X:Set{i:l}. ((G[X] ⊆ X) ⇒ (∀a:Set{i:l}. (itersetfun(x.G[x];a) ⊆ X)))))
Definition: coset-relation
coSetRelation(R) == ∀x,x',y,y':coSet{i:l}. (seteq(x;x') ⇒ seteq(y;y') ⇒ (R x y) ⇒ (R x' y'))
Lemma: coset-relation_wf
∀[R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ']. (coSetRelation(R) ∈ ℙ')
Definition: set-relation
This says that the relation R respects the extensional equality ⌜seteq(x;y)⌝.⋅
SetRelation(R) == ∀x,x',y,y':Set{i:l}. (seteq(x;x') ⇒ seteq(y;y') ⇒ (R x y) ⇒ (R x' y'))
Lemma: set-relation_wf
∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. (SetRelation(R) ∈ ℙ')
Definition: set-relation-on
SetRelationOn(A;R) == ∀x,x',y,y':{u:Set{i:l}| (u ∈ A)} . (seteq(x;x') ⇒ seteq(y;y') ⇒ (R x y) ⇒ (R x' y'))
Lemma: set-relation-on_wf
∀[A:Set{i:l}]. ∀[R:{u:Set{i:l}| (u ∈ A)} ⟶ {u:Set{i:l}| (u ∈ A)} ⟶ ℙ']. (SetRelationOn(A;R) ∈ ℙ')
Definition: mv-map
This says that the relation R relates every member of A
to at least one member of B. So it is a "multi-valued map" from A to B.⋅
R:(A ⇒ B) == ∀x:coSet{i:l}. ((x ∈ A) ⇒ (∃y:coSet{i:l}. ((y ∈ B) ∧ (R x y))))
Lemma: mv-map_wf
∀[A,B:coSet{i:l}]. ∀[R:{u:coSet{i:l}| (u ∈ A)} ⟶ {v:coSet{i:l}| (v ∈ B)} ⟶ ℙ']. ( R:(A ⇒ B) ∈ ℙ')
Definition: onto-map
This says that relation R maps A onto B. ⋅
R:(A ─>> B) == ∀y:coSet{i:l}. ((y ∈ B) ⇒ (∃x:coSet{i:l}. ((x ∈ A) ∧ (R x y))))
Lemma: onto-map_wf
∀[A,B:coSet{i:l}]. ∀[R:{u:coSet{i:l}| (u ∈ A)} ⟶ {v:coSet{i:l}| (v ∈ B)} ⟶ ℙ']. (R:(A ─>> B) ∈ ℙ')
Definition: setrel
Any set R determines a relation on sets.
It is extensional (i.e. set-relation-setrel).⋅
setrel(R) == λx,y. ((x,y) ∈ R)
Lemma: setrel_wf
∀[R:coSet{i:l}]. (setrel(R) ∈ coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ)
Lemma: set-relation-setrel
∀R:coSet{i:l}. SetRelation(setrel(R))
Lemma: coset-relation-setrel
∀R:coSet{i:l}. coSetRelation(setrel(R))
Lemma: set-relation-on-setrel
∀R,A:Set{i:l}. SetRelationOn(A;setrel(R))
Definition: regularset
A transitive set A is regular if for every set R that is a multi-valued
map from a member, B, to the whole set A, the range of the map R
is a set b in A. ⋅
regular(A) ==
transitive-set(A)
∧ (∀B:coSet{i:l}
((B ∈ A)
⇒ (∀R:coSet{i:l}
( setrel(R):(B ⇒ A) ⇒ (∃b:coSet{i:l}. ((b ∈ A) ∧ setrel(R):(B ⇒ b) ∧ setrel(R):(B ─>> b)))))))
Lemma: regularset_wf
∀[A:coSet{i:l}]. (regular(A) ∈ ℙ')
Definition: Regularcoset
cRegular(A) ==
transitive-set(A)
∧ (∀B:coSet{i:l}
((B ∈ A)
⇒ (∀R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
(coSetRelation(R) ⇒ R:(B ⇒ A) ⇒ (∃b:coSet{i:l}. ((b ∈ A) ∧ R:(B ⇒ b) ∧ R:(B ─>> b)))))))
Lemma: Regularcoset_wf
∀[A:coSet{i:l}]. (cRegular(A) ∈ ℙ{i''})
Definition: Regularset
Regular(A) is a generalization of regular(A) where the relation R
can be any extensional relation (not necessarily given by a set).
So, Regular(A) ⇒ regular(A) (see Regularset-regularset).
Aczel's "regular extension axiom" is that every set is a subset of
a regular set (in fact of a Regular set).
see RegularExtension ⋅
Regular(A) ==
transitive-set(A)
∧ (∀B:Set{i:l}
((B ∈ A)
⇒ (∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
(SetRelation(R) ⇒ R:(B ⇒ A) ⇒ (∃b:Set{i:l}. ((b ∈ A) ∧ R:(B ⇒ b) ∧ R:(B ─>> b)))))))
Lemma: Regularset_wf
∀[A:Set{i:l}]. (Regular(A) ∈ ℙ{i''})
Lemma: Regularset-regularset
∀A:Set{i:l}. (Regular(A) ⇒ regular(A))
Lemma: Regularcoset-regularset
∀A:coSet{i:l}. (cRegular(A) ⇒ regular(A))
Definition: regextfun
regextfun(f;w)==r let t,g = w in λu.regextfun(f;g u)"(set-dom(f t))
Lemma: regextfun_wf
∀[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[w:coW(T;x.set-dom(f x))]. (regextfun(f;w) ∈ coSet{i:l})
Lemma: regextfun_wf2
∀[T:Type]. ∀[f:T ⟶ Set{i:l}]. ∀[w:W(T;x.set-dom(f x))]. (regextfun(f;w) ∈ Set{i:l})
Definition: regext
By forming a set indexed by a suitable W type, we get a Regular set r for which
(a ⊆ r) provided that set a is transitive.
See subset-regext and regext-Regularset.⋅
regext(a) == let T,f = a in λw.regextfun(f;w)"(W(T;x.set-dom(f x)))
Lemma: regext_wf
∀[a:coSet{i:l}]. (regext(a) ∈ coSet{i:l})
Lemma: regext_wf2
∀[a:Set{i:l}]. (regext(a) ∈ Set{i:l})
Lemma: regext-transitive
∀a:coSet{i:l}. transitive-set(regext(a))
Lemma: regext-lemma1
∀T:Type. ∀f:T ⟶ coSet{i:l}. ∀B:coSet{i:l}.
((∃t:T. ∃g:set-dom(f t) ⟶ coSet{i:l}. seteq(B;mk-coset(set-dom(f t);g)))
⇒ (∀R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
(coSetRelation(R)
⇒ R:(B ⇒ regext(mk-coset(T;f)))
⇒ (∃b:coSet{i:l}. ((b ∈ regext(mk-coset(T;f))) ∧ R:(B ⇒ b) ∧ R:(B ─>> b))))))
Lemma: regext-lemma
∀T:Type. ∀f:T ⟶ Set{i:l}. ∀B:Set{i:l}.
((∃t:T. ∃g:set-dom(f t) ⟶ Set{i:l}. seteq(B;g"(set-dom(f t))))
⇒ (∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
(SetRelation(R)
⇒ R:(B ⇒ regext(f"(T)))
⇒ (∃b:Set{i:l}. ((b ∈ regext(f"(T))) ∧ R:(B ⇒ b) ∧ R:(B ─>> b))))))
Lemma: regext-Regularcoset
∀a:coSet{i:l}. cRegular(regext(a))
Lemma: regext-Regularset
∀a:Set{i:l}. Regular(regext(a))
Lemma: subset-regext
∀a:Set{i:l}. (transitive-set(a) ⇒ (a ⊆ regext(a)))
Lemma: RegularExtension
∀a:Set{i:l}. ∃r:Set{i:l}. ((a ⊆ r) ∧ Regular(r))
Lemma: regularExtension
∀a:Set{i:l}. ∃r:Set{i:l}. ((a ⊆ r) ∧ regular(r))
Lemma: regext-loopset-empty
Now we do get ⌜(loopset() ⊆ co-regext(loopset()))⌝, because the type
⌜coW(Unit;x.Unit)⌝ has a single member (while the corresponding W type
⌜W(Unit;x.Unit)⌝ is empty). So the needed property
⌜∀a:coSet{i:l}. (transitive-set(a) ⇒ (a ⊆ co-regext(a)))⌝ could be true??..⋅
seteq(regext(loopset());{})
Definition: co-regext
co-regext(a) == let T,f = a in mk-coset(coW(T;x.set-dom(f x));λw.regextfun(f;w))
Lemma: co-regext_wf
∀[a:coSet{i:l}]. (co-regext(a) ∈ coSet{i:l})
Lemma: co-regext-transitive
∀a:coSet{i:l}. transitive-set(co-regext(a))
Lemma: co-regext-lemma
∀T:Type. ∀f:T ⟶ coSet{i:l}. ∀B:coSet{i:l}.
((∃t:T. ∃g:set-dom(f t) ⟶ coSet{i:l}. seteq(B;mk-coset(set-dom(f t);g)))
⇒ (∀R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
(coSetRelation(R)
⇒ R:(B ⇒ co-regext(mk-coset(T;f)))
⇒ (∃b:coSet{i:l}. ((b ∈ co-regext(mk-coset(T;f))) ∧ R:(B ⇒ b) ∧ R:(B ─>> b))))))
Lemma: co-regext-Regularcoset
The proof that ⌜co-regext(a)⌝ is regular goes through as before, just
using co- versions of everything.⋅
∀a:coSet{i:l}. cRegular(co-regext(a))
Lemma: co-regext-loopset
Now we do get ⌜(loopset() ⊆ co-regext(loopset()))⌝, because the type
⌜coW(Unit;x.Unit)⌝ has a single member (while the corresponding W type
⌜W(Unit;x.Unit)⌝ is empty). So the needed property
⌜∀a:coSet{i:l}. (transitive-set(a) ⇒ (a ⊆ co-regext(a)))⌝ could be true??..⋅
seteq(co-regext(loopset());loopset())
Lemma: subset-co-regext-1
∀a:coSet{i:l}. (transitive-set(a) ⇒ (∀x:Set{i:l}. ((x ∈ a) ⇒ (x ∈ co-regext(a)))))
Definition: regextW
regextW(G;t)==r Wsup(t;λi.regextW(G;G t i))
Lemma: regextW_wf
∀[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[G:i:T ⟶ j:set-dom(f i) ⟶ T]. ∀[t:T]. (regextW(G;t) ∈ coW(T;x.set-dom(f x)))
Lemma: subset-co-regext
∀a:coSet{i:l}. (transitive-set(a) ⇒ (a ⊆ co-regext(a)))
Definition: relclosed-set
closed(x,a.R[x; a])s == ∀x,a:Set{i:l}. ((x ⊆ s) ⇒ R[x; a] ⇒ (a ∈ s))
Lemma: relclosed-set_wf
∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. ∀[s:Set{i:l}]. (closed(x,a.R[x;a])s ∈ ℙ')
Definition: mem-mk-set
mem-mk-set(f;t) == <t, seteqweaken(f t) Ax>
Lemma: mem-mk-set_wf
∀[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[t:T]. (mem-mk-set(f;t) ∈ (f t ∈ mk-coset(T;f)))
Lemma: mem-mk-set_wf2
∀[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[t:T]. (mem-mk-set(f;t) ∈ (f t ∈ f"(T)))
Definition: setimage
setimage{i:l}(x;b) ==
∃f:(z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
((∀z1,z2:z:coSet{i:l} × (z ∈ b). (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2)))
∧ (∀y:coSet{i:l}. ((y ∈ x) ⇐⇒ ∃z:z:coSet{i:l} × (z ∈ b). seteq(y;f z))))
Lemma: setimage_wf
∀[x,b:coSet{i:l}]. (setimage{i:l}(x;b) ∈ ℙ')
Definition: set-image
set-image(f;b) == let T,g = b in <T, λt.(f <g t, mem-mk-set(g;t)>)>
Lemma: set-image_wf
∀[b:coSet{i:l}]. ∀[f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}]. (set-image(f;b) ∈ coSet{i:l})
Lemma: set-image_wf2
∀[b:coSet{i:l}]. ∀[f:(x:coSet{i:l} × (x ∈ b)) ⟶ Set{i:l}]. (set-image(f;b) ∈ Set{i:l})
Lemma: setmem-image
∀b:coSet{i:l}. ∀f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}.
((∀z1,z2:x:coSet{i:l} × (x ∈ b). (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2)))
⇒ (∀y:coSet{i:l}. ((y ∈ set-image(f;b)) ⇐⇒ ∃x:x:coSet{i:l} × (x ∈ b). seteq(y;f x))))
Lemma: setimage-iff
∀x,b:coSet{i:l}.
(setimage{i:l}(x;b)
⇐⇒ ∃f:(z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
((∀z1,z2:z:coSet{i:l} × (z ∈ b). (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))) ∧ seteq(x;set-image(f;b))))
Definition: fun-graph
fun-graph(b;f) == let T,g = b in <T, λt.(g t,f <g t, mem-mk-set(g;t)>)>
Lemma: fun-graph_wf
∀[b:coSet{i:l}]. ∀[f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}]. (fun-graph(b;f) ∈ coSet{i:l})
Lemma: fun-graph_wf2
∀[b:Set{i:l}]. ∀[f:(x:Set{i:l} × (x ∈ b)) ⟶ Set{i:l}]. (fun-graph(b;f) ∈ Set{i:l})
Lemma: setmem-fun-graph
∀b:coSet{i:l}. ∀f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}.
((∀z1,z2:x:coSet{i:l} × (x ∈ b). (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2)))
⇒ (∀y:coSet{i:l}. ((y ∈ fun-graph(b;f)) ⇐⇒ ∃p:x:coSet{i:l} × (x ∈ b). seteq(y;(fst(p),f p)))))
Lemma: function-graph-fun-graph
∀b:coSet{i:l}. ∀f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}.
((∀z1,z2:x:coSet{i:l} × (x ∈ b). (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2)))
⇒ (∀x:coSet{i:l}. ((set-image(f;b) ⊆ x) ⇒ function-graph{i:l}(b;_.x;fun-graph(b;f)))))
Lemma: setmem-setimages-2
∀A,b,x:coSet{i:l}. ((A ∈ setimages(b;x)) ⇐⇒ setimage{i:l}(A;b) ∧ (A ⊆ x))
Lemma: setimages_functionality
∀b1,b2,x1,x2:coSet{i:l}. (seteq(b1;b2) ⇒ seteq(x1;x2) ⇒ seteq(setimages(b1;x1);setimages(b2;x2)))
Definition: bounded-relation
Bounded(x,a.R[x; a]) ==
(∀x1,x2,a1,a2:Set{i:l}. (seteq(x1;x2) ⇒ seteq(a1;a2) ⇒ R[x1; a1] ⇒ R[x2; a2]))
∧ (∀x:Set{i:l}. ∃y:Set{i:l}. ∀a:Set{i:l}. (R[x; a] ⇐⇒ (a ∈ y)))
∧ (∃B:Set{i:l}. ∀x,a:Set{i:l}. (R[x; a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b)))))
Lemma: bounded-relation_wf
∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. (Bounded(x,a.R[x;a]) ∈ ℙ')
Definition: inductively-defined
inductively-defined{i:l}(x,a.R[x; a];s) == closed(x,a.R[x; a])s ∧ (∀s':Set{i:l}. (closed(x,a.R[x; a])s' ⇒ (s ⊆ s')))
Lemma: inductively-defined_wf
∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. ∀[s:Set{i:l}]. (inductively-defined{i:l}(x,a.R[x;a];s) ∈ ℙ')
Lemma: inductively-defined-unique
∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ'. ∀s1,s2:Set{i:l}.
(inductively-defined{i:l}(x,a.R[x;a];s1) ⇒ inductively-defined{i:l}(x,a.R[x;a];s2) ⇒ seteq(s1;s2))
Definition: least-closed-set
By iterating over all the members of a regular set containg the transitive
closure of set B we can form the least set closed under function G,
provided that B is a bound for G in a suitable sense.
(Spelled out in the lemma least-closed-set-inductively-defined).⋅
least-closed-set(B;G) == ⋃a∈regext(setTC(B)).itersetfun(x.G x;a)
Lemma: least-closed-set_wf
∀[B:Set{i:l}]. ∀[G:Set{i:l} ⟶ Set{i:l}]. (least-closed-set(B;G) ∈ Set{i:l})
Lemma: least-closed-set-inductively-defined
∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']
∀B:Set{i:l}. ∀G:Set{i:l} ⟶ Set{i:l}.
((∀x,a:Set{i:l}. (R[x;a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b)))))
⇒ (∀x,z:Set{i:l}. ((z ∈ G x) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ R[A;z])))
⇒ inductively-defined{i:l}(x,a.R[x;a];least-closed-set(B;G)))
Definition: closure-set
closure-set(B;Y;x) is the set of things we need to add to set x
(iteratively) to eventually close x under function Y.
The bound B makes this possible.⋅
closure-set(B;Y;x) == ⋃b∈B. ⋃A∈setimages(b;x).Y A
Lemma: closure-set_wf
∀[B:Set{i:l}]. ∀[Y:Set{i:l} ⟶ Set{i:l}]. ∀[x:Set{i:l}]. (closure-set(B;Y;x) ∈ Set{i:l})
Lemma: setmem-closure-set
∀B:Set{i:l}. ∀Y:Set{i:l} ⟶ Set{i:l}. ∀x:Set{i:l}.
((∀b:Set{i:l}. ((b ∈ B) ⇒ set-function{i:l}(setimages(b;x); A.Y A)))
⇒ (∀z:Set{i:l}
((z ∈ closure-set(B;Y;x)) ⇐⇒ ∃b:coSet{i:l}. ((b ∈ B) ∧ (∃A:coSet{i:l}. ((A ∈ setimages(b;x)) ∧ (z ∈ Y A)))))))
Lemma: closure-set-property
∀B,x:Set{i:l}. ∀Y:x1:Set{i:l} ⟶ Set{i:l}.
((∀x1,x2,a1,a2:Set{i:l}. (seteq(x1;x2) ⇒ seteq(a1;a2) ⇒ (a1 ∈ Y x1) ⇒ (a2 ∈ Y x2)))
⇒ (∀x,a:Set{i:l}. ((a ∈ Y x) ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b)))))
⇒ (∀z:Set{i:l}. ((z ∈ closure-set(B;Y;x)) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ (z ∈ Y A)))))
Definition: inductive-set
If bdd witnesses ⌜Bounded(A,a.R[A;a])⌝ then
for _,S,B,_ = bdd, B is a bound on the "cardinality" of the A's
and ⌜λA.(fst((S A)))⌝ is the set {a | R[A;a]}.
For any set x, the set ⌜closure-set(B;λA.(fst((S A)));x)⌝ will contain
all the sets a for which R[A;a] for some ⌜(A ⊆ x)⌝.
So, the set defined inductively by R is the closure of the
function ⌜λx.closure-set(B;λA.(fst((S A)));x)⌝.
This is proved in inductive-set-property.⋅
inductive-set(bdd) == let _,S,B,_ = bdd in least-closed-set(B;λx.closure-set(B;λz.(fst((S z)));x))
Lemma: inductive-set_wf
∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. ∀[bdd:Bounded(x,a.R[x;a])]. (inductive-set(bdd) ∈ Set{i:l})
Lemma: inductive-set-property
∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. ∀bdd:Bounded(x,a.R[x;a]). inductively-defined{i:l}(x,a.R[x;a];inductive-set(bdd))
Definition: funclosed-set
f-closed(s) == ∀x:Set{i:l}. ((x ⊆ s) ⇒ (f x ⊆ s))
Lemma: funclosed-set_wf
∀[f:Set{i:l} ⟶ Set{i:l}]. ∀[s:Set{i:l}]. (f-closed(s) ∈ ℙ')
Lemma: relclosed-iff-funclosed
∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ
((∀x:Set{i:l}. ∃y:Set{i:l}. ∀a:Set{i:l}. (R[x;a] ⇐⇒ (a ∈ y)))
⇒ (∃f:Set{i:l} ⟶ Set{i:l}. ∀s:Set{i:l}. (closed(x,a.R[x;a])s ⇐⇒ f-closed(s))))
Definition: injectively-presented
InjectivelyPresented(s) == Inj(set-dom(s);Set{i:l};λx.set-item(s;x))
Lemma: injectively-presented_wf
∀[s:Set{i:l}]. (InjectivelyPresented(s) ∈ ℙ')
Lemma: injectively-presented-emptyset
InjectivelyPresented({})
Lemma: injectively-presented-singleset
∀a:Set{i:l}. InjectivelyPresented({a})
Definition: injectively-presentable
InjectivelyPresentable(a) == ∃b:Set{i:l}. (InjectivelyPresented(b) ∧ seteq(a;b))
Lemma: injectively-presentable_wf
∀[a:Set{i:l}]. (InjectivelyPresentable(a) ∈ ℙ')
Lemma: injectively-presented-presentable
∀a:Set{i:l}. (InjectivelyPresented(a) ⇒ InjectivelyPresentable(a))
Definition: WtoSet
WtoSet(a.B[a];x) == let a,f = x in λb.WtoSet(a.B[a];f b)"(B[a])
Lemma: WtoSet_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[x:W(A;a.B[a])]. (WtoSet(a.B[a];x) ∈ Set{i:l})
Lemma: WtoSet-order-preserving
∀[A:Type]. ∀[B:A ⟶ Type].
∀x,y:W(A;a.B[a]). ∀b:𝔹. ((x Wcmp(A;a.B[a];b) y) ⇒ (WtoSet(a.B[a];x) Wcmp(Type;a.a;b) WtoSet(a.B[a];y)))
Home
Index