% problem-set/set.theory/godel/subset.ver1.in % 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 % nop(x,y) : non-ordered pair (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) : > is in rotate_right(x) if > is. % flip_range(x) : > is in flip_range(x) if > 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 set(para_into). set(para_from). set(para_from_left). set(para_from_right). set(Unit_deletion). set(back_demod). set(UR_res). assign(max_kept,5000). list(axioms). % 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). end_of_list. list(sos). % denial of the theorem: SUBSET(as,cs). SUBSET(bs,cs). -SUBSET(join(as,bs),cs). end_of_list. list(demodulators). EQUAL(comp(inter(comp(x),comp(y))),join(x,y)). end_of_list.