[FOM] Fregean set theory and replacement

[William Tait]

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  
going near the paradox'.

> 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