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