CHALLENG.TXT                       2002 July 27

The challenge is to show that in general, unions of intersections are
intersections of unions, and conversely.  For finite sets, this is an
immediate consequence of the distributive law.  The challenge is to
show that this holds in general.

The Uclosure of a class x is the class of all unions of subsets of x, 
and the Aclosure of x is the class of all intersections of subsets of x.
In general the class x is contained in both its Uclosure and its Aclosure.
A number of other elementary properties of Aclosure and Uclosure have 
been proved using Otter.  See the groups ACL and UCL in the Otter proof
summaries for details.  Additional properties that have been discovered
with the GOEDEL program have been added as rewrite rules for the program
itself.  The GOEDEL program is a text file that can be opened and read
with any text editor.


These concepts are encountered, for example, in topology: a topology is 
often constructed as the Uclosure of a collection of basic open sets.
A topology is its own Uclosure; the class of closed sets is equal to its
own Aclosure.

These concepts are useful also outside of topology.  The class FULL of 
all full sets fails to be a topology because it is a proper class rather 
than a set.  The class FULL is its own Aclosure and its own Uclosure.  
The same is true for the class OMEGA of all ordinal numbers.  The class 
FINITE of all finite sets is its own Aclosure, but its Uclosure is the 
class of all sets.  

The idempotent functions ACLOSURE and UCLOSURE take a set x to its 
Aclosure and its Uclosure respectively.

The challenge question is to show that Uclosure(Aclosure(x)) is equal
to Aclosure(Uclosure(x)) for any set x.  That is, the question is
whether ACLOSURE commutes with UCLOSURE.