The consistency of NF in Lean?

Timothy Y. Chow tchow at
Sun Feb 27 08:55:41 EST 2022

On Sun, 27 Feb 2022, JOSEPH SHIPMAN wrote:
> Remind me, what’s the consistency strength that was claimed?

Long ago, Specker showed that NF is equiconsistent with (Russellian 
unramified) typed set theory plus the axiom schema of typical ambiguity.

Assuming Holmes's argument is correct, it constructs a model of TST + 
Ambiguity in ZFA.  (ZFA is used for convenience since the heart of the 
proof is a Fraenkel-Mostowski construction; you can use ZF if you prefer.) 
>From what I've heard, his proof can probably be carried out in something 
weaker, but since the community hasn't yet digested even the ZFA proof, 
working too hard on weakening the metatheory seems premature...


More information about the FOM mailing list