problem-set/pelletier/p41.desc created : 07/25/86 revised : 08/17/89 Natural Language Description: Full Predicate Logic (without Identity and Functions) Problem #41. 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 Versions: p41.in - declarative representation. created by : From Pelletier paper, 1986. verified for ITP : untested, 07/25/86 translated for OTTER by : caw. verified for OTTER : 08/17/89.