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

% description :
%
% Theorem: If A and B are contained in C then the union of A and B is also;
% 	i.e., -SUBSET(xs,ys) | -SUBSET(zs,ys) | SUBSET(join(xs,zs),ys).

% 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 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)))).

% definition of empty set:

-EL(z,0).

% definition of universal set:

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

% 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).


% denial of the theorem:

SUBSET(as,cs).
SUBSET(bs,cs).
-SUBSET(join(as,bs),cs).