% problem-set/set.theory/godel/compl.ver1.clauses % created : 07/16/86 % revised : 08/12/88 % description : % % Theorem: The complement of the complement of a set is that set; i.e., % EQUAL(comp(comp(xs)),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 B-3, complement: -EL(z,comp(x)) | -EL(z,x). EL(z,comp(x)) | -M(z) | EL(z,x). % definition of empty set: -EL(z,0). % definition of universal set: EL(z,1) | -M(z). % denial of the theorem: EQUAL(comp(as),bs). EQUAL(comp(bs),cs). -EQUAL(as,cs).