% problem-set/pelletier/p40.clauses
% created : 07/25/86
% revised : 08/17/89

% description:
%
% Full Predicate Logic (without Identity and Functions).
% If there were an 'anti-Russell set' (a set which contains exactly 
% those sets which are members of themselves), then not every set has a 
% complement.
%  
% (Ey)(Ax)(Fxy <-> Fxx) ->.
%    -(Ax)(Ey)(Az)(Fzy <-> -Fzx).

% representation:
%
% declare_predicate(2,F).
% declare_constant([a]).
% declare_variables([x,y,z]).


% denial of the statement
-(	(exists y all x (F(x,y) <-> F(x,x))) -> 
	-(all x exists y all z (F(z,y) <-> -F(z,x)))
).