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

% description:
% 
% Full Predicate Logic (without Identity and Functions).
% The 'restricted comprehension axiom' says: given a set z, there is a.
% set all of whose members are drawn form z and which satisfy some .
% property. If there were a universal set then the Russell set could.
% be formed, using this axiom. So given the appropriate instance.
% of this axiom, there is no universal set.
% (Az)(Ey)(Ax)(Fxy <->.
% --------------------.
%   (Fxz & -Fxx)).
%   --------------.
%   -(Ez)(Ax)Fxz.

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

% premise
(all z exists y all x (F(x,y) <-> (F(x,z) & -F(x,x)))).

% denial of the conclusion
(exists z all x F(x,z)).