self-duality of conditional completeness

Johan G. F. Belinfante
2010 September 16

<<goedel.10sep14a

summary

That the property of being conditionally complete is selfdual is proved in Kelley’s book on topology (see page 14).

"John L. Kelley, General Topology, D. Van Nostrand Co., Inc., Princeton, New Jersey, 1955.";

Kelley’s statement of this theorem is already quite general: he does not restrict the result to lattices, and his definition of a partial order assumes only transitivity.  But even this assumption is not needed in the proof.  In this notebook the theorem about selfduality of the conditional completeness property is derived for any set.

the class of conditionally complete relations

The class CC of conditionally complete relations is defined by the following rewrite rule:

image[V,intersection[CC,set[x_]]]:=intersection[complement[image[V,intersection[x,complement[cart[V,V]]]]],complement[image[V,intersection[complement[domain[LUB[x]]],complement[set[0]],domain[UB[x]]]]],image[V,set[x]]]

Theorem.  The class CC is a subclass of the class P[cart[V, V]] of all small relations.

Map[equal[V,#]&,complement[dif[CC,P[cart[V,V]]]]//Renormality]

subclass[U[CC],cart[V,V]]:=True

Theorem.  The empty relation is conditionally complete.

member[0,CC]//AssertTest

member[0,CC]:=True

a wrapper for conditionally complete relations

A wrapper cc[x] for conditionally complete relations is defined by the following rewrite rule.  (This rewrite rule was suggested by replacing the class GROUPS in the definition of the gp[x] wrapper by the class CC of conditionally complete relations.)

image[V,intersection[cc[x_],set[y_]]]:=intersection[complement[image[V,intersection[x,complement[cart[V,V]]]]],complement[image[V,intersection[complement[domain[LUB[x]]],complement[set[0]],domain[UB[x]]]]],image[V,intersection[x,set[y]]],image[V,set[x]]]

Theorem.

member[x,CC]//AssertTest//Reverse

and[member[x_,V],subclass[x_,cart[V,V]],subclass[domain[UB[x_]],union[domain[LUB[x_]],set[0]]]]:=member[x,CC]

Theorem.   Normalization rule for cc[x].

Map[fix,SubstTest[reify,y,image[V,intersection[t,set[y]]],t->cc[x]]]//Reverse

intersection[x_,complement[image[V,intersection[x_,complement[cart[V,V]]]]],complement[image[V,intersection[complement[domain[LUB[x_]]],complement[set[0]],domain[UB[x_]]]]],image[V,set[x_]]]:=cc[x]

Lemma.

equiv[or[equal[0,x],member[x,CC]],member[x,CC]]

or[equal[0,x_],member[x_,CC]]:=member[x,CC]

Theorem.  Wrapper removal rule.

SubstTest[equal,x,intersection[x,image[V,intersection[t,set[x]]]],t->CC]//Reverse

equal[x_,cc[x_]]:=member[x,CC]

Theorem.  The class cc[x] is a relation.

Map[empty,SubstTest[dif,intersection[x,complement[image[V,intersection[x,complement[cart[V,V]]]]],complement[image[V,intersection[complement[domain[LUB[x]]],complement[set[0]],domain[UB[x]]]]],image[v,set[x]]],cart[V,V],v->V]]//Reverse

subclass[cc[x_],cart[V,V]]:=True

Theorem.  The members of the class CC are conditionally complete.

SubstTest[implies,and[p,q],p,{p->subclass[domain[UB[x]],union[domain[LUB[x]],set[0]]],q->member[x,P[cart[V,V]]]}]//Reverse

or[not[member[x_,CC]],subclass[domain[UB[x_]],union[domain[LUB[x_]],set[0]]]]:=True

Theorem.  Wrapper introduction rule.  The class cc[x] is conditionally complete.

SubstTest[member,intersection[x,image[V,intersection[t,set[x]]]],t,t->CC]//Reverse

member[cc[x_],CC]:=True

Theorem.

SubstTest[implies,member[t,CC],subclass[domain[UB[t]],union[domain[LUB[t]],set[0]]],t->cc[x]]//Reverse

subclass[domain[UB[cc[x_]]],union[domain[LUB[cc[x_]]],set[0]]]:=True

Theorem.  Sethood.

SubstTest[member,intersection[x,image[V,intersection[set[x],t]]],V,t->CC]//Reverse

member[cc[x_],V]:=True

ub and lb rules for cc[x]

Theorem.  Sethood rule for upper bounds of cc[x].

SubstTest[or,empty[y],member[ub[setpart[t],y],V],t->cc[x]]//Reverse

or[equal[0,y_],member[ub[cc[x_],y_],V]]:=True

Corollary.  A dual result.

SubstTest[or,empty[y],member[lb[setpart[t],y],V],t->cc[x]]//Reverse

or[equal[0,y_],member[lb[cc[x_],y_],V]]:=True

Theorem.

SubstTest[and,subclass[u,v],subclass[v,u],{u->domain[UB[cc[x]]],v->union[domain[LUB[cc[x]]],set[0]]}]

union[domain[LUB[cc[x_]]],set[0]]:=domain[UB[cc[x]]]

the self-duality theorem

Lemma.

(SubstTest[implies,and[member[t,u],equal[u,v]],member[t,v],{t->lb[s,y],u->domain[UB[s]],v->union[domain[LUB[s]],set[0]]}]//Reverse)/.s->cc[x]

(%/.{x->x_,y->y_})/.Equal->SetDelayed

Lemma.

Map[not,SubstTest[and,implies[p1,p3],implies[p1,p4],implies[and[p2,p3,p4],p5],implies[and[p3,p5],p6],not[implies[and[p1,p2],p6]],{p1->not[equal[0,t]],p2->not[equal[0,lb[cc[x],t]]],p3->member[lb[cc[x],t],V],p4->not[equal[0,ub[cc[x],lb[cc[x],t]]]],p5->member[lb[cc[x],t],domain[LUB[cc[x]]]],p6->not[equal[0,lub[cc[x],lb[cc[x],t]]]]}]]//Reverse

(%/.{x->x_,t->t_})/.Equal->SetDelayed

Lemma.

Map[not,SubstTest[and,implies[and[p1,p2],p3],implies[p2,p4],implies[and[p3,p4],p5],not[implies[and[p1,p2],p5]],{p1->not[equal[0,t]],p2->not[equal[0,lb[cc[x],t]]],p3->not[equal[0,lub[cc[x],lb[cc[x],t]]]],p4->equal[lub[cc[x],lb[cc[x],t]],intersection[ub[cc[x],lb[cc[x],t]],lb[cc[x],t]]],p5->not[equal[0,intersection[ub[cc[x],lb[cc[x],t]],lb[cc[x],t]]]]}]]//Reverse

(%/.{x->x_,t->t_})/.Equal->SetDelayed

Lemma.

Map[not,SubstTest[and,implies[p2,p4], implies[and[p1,p6],p7], not[implies[and[p1,p2,p3],p7]],{p1->member[t,V],p2->not[equal[0,t]],p3->not[equal[0,lb[cc[x],t]]],p4->equal[intersection[ub[cc[x],lb[cc[x],t]],lb[cc[x],t]],glb[cc[x],t]],p6->not[equal[0,glb[cc[x],t]]],p7->member[t,domain[GLB[cc[x]]]]}]]//Reverse

(%/.{x->x_,t->t_})/.Equal->SetDelayed

Lemma.

SubstTest[member,t,domain[LB[u]],u->cc[x]]//Reverse

member[t_,image[inverse[S],range[VERTSECT[cc[x_]]]]]:=and[member[t,V],not[equal[0,lb[cc[x],t]]]]

Theorem.

Map[equal[V,#]&,SubstTest[class,t,implies[member[t,u],or[empty[t],member[t,v]]],{u->domain[LB[cc[x]]],v->domain[GLB[cc[x]]]}]]

subclass[image[inverse[S],range[VERTSECT[cc[x_]]]],union[domain[GLB[cc[x_]]],set[0]]]:=True

Theorem.  Removing the cc wrapper.

SubstTest[implies,equal[x,cc[t]],subclass[domain[LB[x]],union[domain[GLB[x]],set[0]]],t->x]//Reverse

or[not[member[x_,CC]],subclass[domain[LB[x_]],union[domain[GLB[x_]],set[0]]]]:=True

Theorem.

(member[inverse[t],CC]//AssertTest)/.t->cc[x]

member[inverse[cc[x_]],CC]:=True

Corollary.  (Removing the cc wrapper.)

SubstTest[implies,equal[x,cc[t]],member[inverse[x],CC],t->x]//Reverse

or[member[inverse[x_],CC],not[member[x_,CC]]]:=True

the selfduality theorem for any set

In this section the self-duality theorem is restated without reference to the class CC, and even dropping the hypothesis that x is a relation for brevity.

Theorem.  Conditional completeness is self-dual for any set.

Map[implies[member[x,y],#]&,(or[not[member[t,V]],not[subclass[t,cart[V,V]]],not[subclass[domain[UB[t]],union[domain[LUB[t]],set[0]]]],subclass[domain[LB[t]],union[domain[GLB[t]],set[0]]]]//NotNotTest)/.t->composite[Id,x]]//MapNotNot

or[not[member[x_,y_]],not[subclass[domain[UB[x_]],union[domain[LUB[x_]],set[0]]]],subclass[domain[LB[x_]],union[domain[GLB[x_]],set[0]]]]:=True

Corollary.  Dual result.

Map[implies[member[x,y],#]&,SubstTest[or,not[member[t,V]],not[subclass[domain[UB[t]],union[domain[LUB[t]],set[0]]]],subclass[domain[LB[t]],union[domain[GLB[t]],set[0]]],t->inverse[x]]]//Reverse//MapNotNot

or[not[member[x_,y_]],not[subclass[domain[LB[x_]],union[domain[GLB[x_]],set[0]]]],subclass[domain[UB[x_]],union[domain[LUB[x_]],set[0]]]]:=True

variable-free statement of selfduality

In this section a variable-free restatement of the self-duality theorem is derived.

Lemma.

Map[equal[V,#]&,SubstTest[class,x,or[member[inverse[x],t],not[member[x,t]]],t->CC]]

%/.Equal->SetDelayed

Lemma.

Map[subclass[#,CC]&,ImageComp[IMAGE[SWAP],id[P[cart[V,V]]],CC]]

%/.Equal->SetDelayed

Theorem.  A variable-free statement of the self-duality of the conditional completeness property.

equal[image[INVERSE,CC],CC]//AssertTest

image[INVERSE,CC]:=CC

Corollary.

ImageComp[IMAGE[SWAP],id[P[cart[V,V]]],CC]//Reverse

image[IMAGE[SWAP],CC]:=CC