[FOM] Why not NF?

[Lew Gordeew]

CORRECTION

-------------------------
Martin Davis wrote on Sun, 19 Feb 2006 16:57:34 -0800
> NF suffers from at least two grave faults:
> 1. It's inconsistent with AC
> 2. Cantor's theorem 2^x > x fails.

Obviously, ZF is closer to the ordinary mathematical reasoning. It allows
more freedom of expression and has greater expressive power than NF, whose
stratification prevents general diagonalization - this linguistic
restriction eliminates not only Russell's paradox, but also many "harmless"
ZF diagonal constructions.

On the other hand, NF is closer to Frege's desired reduction of mathematics
to logic. This reduction is not "pure" though, due to the axiom of
extensionality (Ext). For Ext has at least two unusual consequences, in NF,
which obviously fail in the ZF world:
1. Ext implies the axiom of infinity (Inf).
2. Ext dramatically increases proof theoretical strength,
   since NF minus Ext is not stronger than PA.
(AC and Cantor theorem consequences are not so bold because they don't refer
to "ordinary" ZF sets.)

It was hinted by other posters that Jensen's weakening NFU can serve as,
say, a missing link between NF and ZF. Moreover, Con(NFU + Inf) is provable
in ZF.

My posting of Tue, 14 Feb 2006, went in the opposite direction. I replaced
Ext by a "logical" extension of NF minus Ext. This extension says that NF
minus Ext has a Herbrand model, thus being Herbrand-consistent (HCon), with
respect to a natural finite list (SEPEq) of stratified separation axioms.
The resulting extended formalism, CLOSURE(SEPEq) + DCA(SEPEq), easily proves
Con(NF). That is, HCon(SEPEq) is not weaker than Con(NF).

Generally speaking, the question arises when a given finite list L of set
theoretical operations is Herbrand-consistent? It must not be a megalomaniac
problem aiming at the whole SEPEq. What can be said about _easy_ conditions
on L which imply HCon(L)? There are lists L for which HCon(L) easily holds
and, conversely, there are L for which HCon(L) easily fails. For example,
consider L1 = {f} consisting of one 0-ary operation (a
constant)

f  = {x : (forall y)not(x in y)}.

By an easy Russell-style argument, HCon(L1) fails. Now let L2 = {f,g} extend
L1 by adding another 0-ary operation

g = {x : (exists y)(x in y)}.

It is readily verified that HCon(L2) holds true - take a 2-element model
{0,1} with (0 in 1) & (1 in 1), in which f = the empty set = 0, and g =
{0,1} = 1.

Regards,
L. Gordeev

-- 
DSL-Aktion wegen großer Nachfrage bis 28.2.2006 verlängert:
GMX DSL-Flatrate 1 Jahr kostenlos* http://www.gmx.net/de/go/dsl