# [FOM] Fregean set theory and replacement

William Tait williamtait at mac.com
Wed Aug 15 18:27:56 EDT 2007

On Aug 14, 2007, at 7:07 PM, John McCarthy wrote:

> Consider set theory with unrestricted comprehension.  I'll call it F,
> because I don't know a standard name.  Is there one?  Regrettably, F
> is inconsistent because of Russell's paradox.
>
> A replacement schema (as well as most axioms) is unneeded, because the
> set asserted to exist by replacement is just a comprehension term,
> namely {y|x in A implies R(x,y)}.
>
> F is a very natural system.  However, any proof using unrestricted
> comprehension is suspect.  However again, a proof in F may be
> repairable, e.g. transformed into a proof in ZFC.  This seems likely
> if the proof doesn't go near a paradox.

It would be interesting to have an analysis of this notion of  'not

> Is there any literature discussing the repair of proofs in F?

Quine's New Foundations suggests one obvious idea for this: In the
primitive notation of set theory, with \in as the only non-logical
constant, being able to coherently assign types to all the free
variables of the proof.

The requirement for proofs in NF itself is of course weaker than this
and so its theorems don't all transform into theorems of ZFC (most
definitely not the C bit).

Bill Tait