[YoshiRulz]

ZFC is dead, long live NF..?

As an amateur mathematician whose use of sets is mostly as a lingua franca for describing other things, it's not clear to me what implications this has for the wider mathematical field, especially if the usefulness of NF is comparable to the established ZFC and its variants. Is it expected to become as popular as ZFC in machine proofs?

I do find the existence of a universal set more intuitive, so if nothing else this proof has rekindled my own interest in formalisation.

[barfbagginus]

From my naive and amateur view, the relative consistency result makes NF at least as useful as ZFC, since every model of ZFC can be extended into a model of NF. But it seems it won't make NF all that useful unless:

1. We prove NF is inconsistent. Then ZFC is also inconsistent (and the stars start winking out in the night sky ;)

2. We prove ZFC is inconsistent. Then there's still a chance NF is consistent (fingers crossed!)

I'm probably ignoring more practical "quality of life" benefits of NF, like being able to talk about proper classes, and side stepping Russell's paradox with stratified formulas.

[randallholmes]

It is no part of my agenda to promote the use of NF as an independent foundational system. It is a very odd one. But if someone wants to promote this, the consistency result says, it will work, at least in the sense that you are in no more danger of arriving at a contradiction than you are in ZFC.