% problem-set/set.theory/godel/union.ver1.clauses
% created : 07/16/86
% revised : 08/12/88

% description :
%
% Theorem: The union of sets is commutative; i.e.,
% 	EQUAL(join(xs,ys),join(ys,xs)).

% representation:
%
% declare_predicate(3,[MAPS]).
% declare_predicates(2,[EQUAL,EL,SUBSET,PROPSUBSET,DISJOINT,CLOSED]).
% declare_predicates(1,[M,OPP,RELATION,SINGVAL,FUNCTION,ONEONE]).
% declare_function(3,[app2]).
% declare_functions(2,[inter,join,op,nop,cross,image,restrict,ly,
%	composition]).
% declare_functions(1,[comp,domain,first,second,converse,rotate_right,
%	flip_range,succ,sigma,powerset,range]).
% declare_constants([0,1,as,bs,cs,ds,estin,f15,ident]).
% declare_variables([x,y,z,u,v,w,xf,xg,xs]).
%
% Interpretations of predicates and functions:
% MAPS(x,y,z) : function x maps element y to element z
% EQUAL(x,y) : usual equality of sets
% EL(x,y) : x is an element of set y
% SUBSET(x,y) : x is a subset of y
% PROPSUBSET(x,y) : x is a proper (nonequal) subset of y
% DISJOINT(x,y) : x and y are disjoint, i.e. their intersection is empty
% CLOSED(x,y) : map y is closed with respect to domain x
% M(x) : x is a little set
% OPP(x) : x is an ordered pair predicate
% RELATION(x) : x is a relation 
% SINGVAL(x) : x is a single-valued set
% FUNCTION(x) : x is a function
% ONEONE(x) : x is a one-to-one function
% app2(x,y,z) : apply function x to arguments y and z
% inter(x,y) : intersection of x and y
% join(x,y) : union of x and y
% op(x,y) : ordered pair <x,y>
% nop(x,y) : non-ordered pair <x,y> (equiv. to nop(y,x))
% cross(x,y) : cross product of sets x and y
% image(x,y) : image of point x under map y
% restrict(x,y) : the intersection of x with the cross product of y and 1
% ly(x,y) : chooses a value out of the image set of y under map x
% composition(x,y) : composes maps x and y
% comp(x) : complement of set x
% domain(x) : domain of function x
% first(x) : the first argument of an ordered pair
% second(x) : the second argument of an ordered pair
% converse(x) : the converse (second, first)
% rotate_right(x) : <u,<v,w>> is in rotate_right(x) if <v,<w,u>> is.
% flip_range(x) : <u,<v,w>> is in flip_range(x) if <u,<w,v>> is.
% succ(x) : successor of x
% sigma(x) : the union of the elements of x
% powerset(x) : the set of all subsets of x
% range(x) : the range of map x
% 0 : empty set
% 1 : universal set
% estin : used to define element relation
% f15 : infinity
% ident : identity relation


% Clauses for Godel's Finite Axiomatization of Set Theory.

% equality axiom:

EQUAL(x,x).

% axiom A-1, little sets are sets (omitted because all objects are sets):

% axiom A-2, elements of sets are little sets:

-EL(x,y) | M(x).

% axiom A-3, principle of extensionality:

M(f1(x,y)) | EQUAL(x,y).
EL(f1(x,y),x) | EL(f1(x,y),y) | EQUAL(x,y).
-EL(f1(x,y),x) | -EL(f1(x,y),y) | EQUAL(x,y).

% axiom a-4, existence of nonordered pair:

-EL(u,nop(x,y)) | EQUAL(u,x) | EQUAL(u,y).
EL(u,nop(x,y)) | -M(u) | -EQUAL(u,x).
EL(u,nop(x,y)) | -M(u) | -EQUAL(u,y).
M(nop(x,y)).

% definition of singleton set:

EQUAL(ss(x),nop(x,x)).

% definition of ordered pair:

EQUAL(op(x,y),nop(ss(x),nop(x,y))).

% definition of ordered pair predicate:

-OPP(x) | M(f2(x)).
-OPP(x) | M(f3(x)).
-OPP(x) | EQUAL(x,op(f2(x),f3(x))).
OPP(x) | -M(y) | -M(z) | -EQUAL(x,op(y,z)).

% axiom of first:

-EL(z,first(x)) | M(f4(z,x)).
-EL(z,first(x)) | M(f5(z,x)).
-EL(z,first(x)) | EQUAL(x,op(f4(z,x),f5(z,x))).
-EL(z,first(x)) | EL(z,f4(z,x)).
EL(z,first(x)) | -M(u) | -M(v) | -EQUAL(x,op(u,v)) | -EL(z,u).

% axiom of second:

-EL(z,second(x)) | M(f6(z,x)).
-EL(z,second(x)) | M(f7(z,x)).
-EL(z,second(x)) | EQUAL(x,op(f6(z,x),f7(z,x))).
-EL(z,second(x)) | EL(z,f7(z,x)).
EL(z,second(x)) | -M(u) | -M(v) | -EQUAL(x,op(u,v)) | -EL(z,v).

% axiom B-1, element relation:

-EL(z,estin) | OPP(z).
-EL(z,estin) | EL(first(z),second(z)).
EL(z,estin) | -M(z) | -OPP(z) | -EL(first(z),second(z)).

% axiom B-2, intersection:

-EL(z,inter(x,y)) | EL(z,x).
-EL(z,inter(x,y)) | EL(z,y).
EL(z,inter(x,y)) | -EL(z,x) | -EL(z,y).

% axiom B-3, complement:

-EL(z,comp(x)) | -EL(z,x).
EL(z,comp(x)) | -M(z) | EL(z,x).

% definition of union:

EQUAL(join(x,y),comp(inter(comp(x),comp(y)))).

% axiom B-4, domain:

-EL(z,domain(x)) | OPP(f8(z,x)).
-EL(z,domain(x)) | EL(f8(z,x),x).
-EL(z,domain(x)) | EQUAL(z,first(f8(z,x))).
EL(z,domain(x)) | -M(z) | -OPP(xp) | -EL(xp,x) | -EQUAL(z,first(xp)).

% axiom B-5, cross product:

-EL(z,cross(x,y)) | OPP(z).
-EL(z,cross(x,y)) | EL(first(z),x).
-EL(z,cross(x,y)) | EL(second(z),y).
EL(z,cross(x,y)) | -M(z) | -OPP(z) | -EL(first(z),x) | -EL(second(z),y).

% axiom B-6, converse:

-EL(z,converse(x)) | OPP(z).
-EL(z,converse(x)) | EL(op(second(z),first(z)),x).
EL(z,converse(x)) | -M(z) | -OPP(z) | -EL(op(second(z),first(z)),x).

% axiom B-7, rotate_right:

-EL(z,rotate_right(x)) | M(f9(z,x)).
-EL(z,rotate_right(x)) | M(f10(z,x)).
-EL(z,rotate_right(x)) | M(f11(z,x)).
-EL(z,rotate_right(x)) | EQUAL(z,op(f9(z,x),op(f10(z,x),f11(z,x)))).
-EL(z,rotate_right(x)) | EL(op(f10(z,x),op(f11(z,x),f9(z,x))),x).
EL(z,rotate_right(x)) | -M(z) | -M(u) | -M(v) | -M(w) |
	-EQUAL(z,op(u,op(v,w))) | -EL(op(v,op(w,u)),x).

% axiom B-8, flip_range:

-EL(z,flip_range(x)) | M(f12(z,x)).
-EL(z,flip_range(x)) | M(f13(z,x)).
-EL(z,flip_range(x)) | M(f14(z,x)).
-EL(z,flip_range(x)) | EQUAL(z,op(f12(z,x),op(f13(z,x),f14(z,x)))).
-EL(z,flip_range(x)) | EL(op(f12(z,x),op(f14(z,x),f13(z,x))),x).
EL(z,flip_range(x)) | -M(z) | -M(u) | -M(v) | -M(w) |
	-EQUAL(z,op(u,op(v,w))) | -EL(op(u,op(w,v)),x).

% definition of successor:

EQUAL(succ(x),join(x,ss(x))).

% definition of empty set:

-EL(z,0).

% definition of universal set:

EL(z,1) | -M(z).

% axiom C-1, infinity:

M(f15).
EL(0,f15).
-EL(x,f15) | EL(succ(x),f15).

% axiom C-2, sigma (union of elements):

-EL(z,sigma(x)) | EL(f16(z,x),x).
-EL(z,sigma(x)) | EL(z,f16(z,x)).
EL(z,sigma(x)) | -EL(y,x) | -EL(z,y).
-M(u) | M(sigma(u)).

% definition of subset:

-SUBSET(x,y) | -EL(u,x) | EL(u,y).
SUBSET(x,y) | EL(f17(x,y),x).
SUBSET(x,y) | -EL(f17(x,y),y).

% definition of proper subset:

-PROPSUBSET(x,y) | SUBSET(x,y).
-PROPSUBSET(x,y) | -EQUAL(x,y).
PROPSUBSET(x,y) | -SUBSET(x,y) | EQUAL(x,y).

% axiom C-3, powerset:

-EL(z,powerset(x)) | SUBSET(z,x).
EL(z,powerset(x)) | -M(z) | -SUBSET(z,x).
-M(u) | M(powerset(u)).

% definition of relation:

-RELATION(z) | -EL(x,z) | OPP(x).
RELATION(z) | EL(f18(z),z).
RELATION(z) | -OPP(f18(z)).

% definition of single-valued set:

-SINGVAL(x) | -M(u) | -M(v) | -M(w) | -EL(op(u,v),x) | -EL(op(u,w),x) |
	 EQUAL(v,w).
SINGVAL(x) | M(f19(x)).
SINGVAL(x) | M(f20(x)).
SINGVAL(x) | M(f21(x)).
SINGVAL(x) | EL(op(f19(x),f20(x)),x).
SINGVAL(x) | EL(op(f19(x),f21(x)),x).
SINGVAL(x) | -EQUAL(f20(x),f21(x)).

% definition of function:

-FUNCTION(xf) | RELATION(xf).
-FUNCTION(xf) | SINGVAL(xf).
FUNCTION(xf) | -RELATION(xf) | -SINGVAL(xf).

% axiom C-4, image and substitution:

-EL(z,image(x,xf)) | OPP(f22(z,x,xf)).
-EL(z,image(x,xf)) | EL(f22(z,x,xf),xf).
-EL(z,image(x,xf)) | EL(first(f22(z,x,xf)),x).
-EL(z,image(x,xf)) | EQUAL(second(f22(z,x,xf)),z).
EL(z,image(x,xf)) | -M(z) | -OPP(y) | -EL(y,xf) | -EL(first(y),x) |
	-EQUAL(second(y),z).
-M(x) | -FUNCTION(xf) | M(image(x,xf)).

% definition of disjoint:

-DISJOINT(x,y) | -EL(u,x) | -EL(u,y).
DISJOINT(x,y) | EL(f23(x,y),x).
DISJOINT(x,y) | EL(f23(x,y),y).

% axiom D, regularity:

EQUAL(x,0) | EL(f24(x),x).
EQUAL(x,0) | DISJOINT(f24(x),x).

% axiom E, choice:

FUNCTION(f25).
-M(x) | EQUAL(x,0) | EL(f26(x),x).
-M(x) | EQUAL(x,0) | EL(op(x,f26(x)),f25).

% definition of range:

-EL(z,range(x)) | OPP(f27(z,x)).
-EL(z,range(x)) | EL(f27(z,x),x).
-EL(z,range(x)) | EQUAL(z,second(f27(z,x))).
EL(z,range(x)) | -M(z) | -OPP(xp) | -EL(xp,x) | -EQUAL(z,second(xp)).

% definition of identity relation:

-EL(z,ident) | OPP(z).
-EL(z,ident) | EQUAL(first(z),second(z)).
EL(z,ident) | -M(z) | -OPP(z) | -EQUAL(first(z),second(z)).

% definition of restrict:

EQUAL(restrict(x,y),inter(x,cross(y,1))).

% definition of one-to-one function:

-ONEONE(xf) | FUNCTION(xf).
-ONEONE(xf) | FUNCTION(converse(xf)).
ONEONE(xf) | -FUNCTION(xf) | -FUNCTION(converse(xf)).

% definition of ly:

-EL(z,ly(xf,y)) | OPP(f28(z,xf,y)).
-EL(z,ly(xf,y)) | EL(f28(z,xf,y),xf).
-EL(z,ly(xf,y)) | EQUAL(first(f28(z,xf,y)),y).
-EL(z,ly(xf,y)) | EL(z,second(f28(z,xf,y))).
EL(z,ly(xf,y)) | -OPP(w) | -EL(w,xf) | -EQUAL(first(w),y) | -EL(z,second(w)).

% definition of app2:

EQUAL(app2(xf,x,y),apply(xf,op(x,y))).

% definition of maps:

-MAPS(xf,x,y) | FUNCTION(xf).
-MAPS(xf,x,y) | EQUAL(domain(xf),x).
-MAPS(xf,x,y) | SUBSET(range(xf),y).
MAPS(xf,x,y) | -FUNCTION(xf) | -EQUAL(domain(xf),x) | -SUBSET(range(xf),y).

% definition of closed:

-CLOSED(xs,xf) | M(xs).
-CLOSED(xs,xf) | M(xf).
-CLOSED(xs,xf) | MAPS(xf,cross(xs,xs),xs).
CLOSED(xs,xf) | -M(xs) | -M(xf) | -MAPS(xf,cross(xs,xs),xs).

% definition of composition:

-EL(z,composition(xf,xg)) | M(f29(z,xf,xg)).
-EL(z,composition(xf,xg)) | M(f30(z,xf,xg)).
-EL(z,composition(xf,xg)) | M(f31(z,xf,xg)).
-EL(z,composition(xf,xg)) | EQUAL(z,op(f29(z,xf,xg),f30(z,xf,xg))).
-EL(z,composition(xf,xg)) | EL(op(f29(z,xf,xg),f31(z,xf,xg)),xf).
-EL(z,composition(xf,xg)) | EL(op(f31(z,xf,xg),f30(z,xf,xg)),xg).
EL(z,composition(xf,xg)) | -M(z) | -M(x) | -M(y) | -M(w) |
	-EQUAL(z,op(x,y)) | -EL(op(x,w),xf) | -EL(op(w,y),xg).


% denial of the theorem:

EQUAL(join(as,bs),cs).
EQUAL(join(bs,as),ds).
-EQUAL(cs,ds).