% problem-set/set.theory/naive/union.ver1.clauses % created : 07/16/86 % revised : 08/10/88 % description: % % Theorem: The union of sets is commutative. % representation: % % declare_predicates(2,[EL,INCL,EQ,EQE]). % declare_functions(2,[difel,join,int]). % declare_function(1,comp). % declare_constants([as,bs,cs,ds,empty]). % declare_variables([x,y,z,xs,ys,zs,xp,yp]). % % In the following axioms, EQ(xs,ys) represents Equality of sets, % EQE(x,y) represents Equality of elements. difel(xs,ys) represents an % element in 'xs' but not in 'ys'. join(xs,ys) is the union of xs and % ys; int(xs,ys) is the intersection of xs and ys; comp(xs) is the % complement of xs; as, bs, and cs are constant sets; empty is the empty % set. % definition of the empty set -EL(x,empty). % axioms of inclusion -INCL(xs,ys) | -EL(x,xs) | EL(x,ys). INCL(xs,ys) | EL(difel(xs,ys),xs). INCL(xs,ys) | -EL(difel(xs,ys),ys). % axioms of complementation EL(x,xs) | EL(x,comp(xs)). -EL(x,xs) | -EL(x,comp(xs)). % axioms of union -EL(x,xs) | EL(x,join(xs,ys)). -EL(x,ys) | EL(x,join(xs,ys)). -EL(x,join(xs,ys)) | EL(x,xs) | EL(x,ys). % axioms of intersection -EL(x,xs) | -EL(x,ys) | EL(x,int(xs,ys)). -EL(x,int(xs,ys)) | EL(x,xs). -EL(x,int(xs,ys)) | EL(x,ys). % set equality axioms -EQ(xs,ys) | INCL(xs,ys). -EQ(xs,ys) | INCL(ys,xs). -INCL(xs,ys) | -INCL(ys,xs) | EQ(xs,ys). % equality axioms EQ(xs,xs). -EQ(xs,ys) | EQ(ys,xs). -EQ(xs,ys) | -EQ(ys,zs) | EQ(xs,zs). EQE(x,x). -EQE(x,y) | EQE(y,x). -EQE(x,y) | -EQE(y,z) | EQE(x,z). % equality substitution axioms -EQE(x,y) | -EL(x,xs) | EL(y,xs). -EQ(xs,ys) | -EL(x,xs) | EL(x,ys). -EQ(xs,xp) | -INCL(xs,ys) | INCL(xp,ys). -EQ(ys,yp) | -INCL(xs,ys) | INCL(xs,yp). -EQ(xs,xp) | EQE(difel(xs,ys),difel(xp,ys)). -EQ(ys,yp) | EQE(difel(xs,ys),difel(xs,yp)). -EQ(xs,xp) | EQ(comp(xs),comp(xp)). -EQ(xs,xp) | EQE(join(xs,ys),join(xp,ys)). -EQ(ys,yp) | EQE(join(xs,ys),join(xs,yp)). -EQ(xs,xp) | EQE(int(xs,ys),int(xp,ys)). -EQ(ys,yp) | EQE(int(xs,ys),int(xs,yp)). % denial of the theorem % equivalent form: -EQ(join(as,bs),join(bs,as)). EQ(join(as,bs),cs). EQ(join(bs,as),ds). -EQ(cs,ds).