[FOM] Tolerance Principle

[Lew Gordeew]

Thomas Forster wrote on Thu, 9 Feb 2006 16:59:12 +0000 (GMT):
> My guess is that ZF proves Con(NF)

I conjecture that Con(NF) is not provable in ZF.

My guess is that ZF and NF behave like parallel FOM universes. Both can
differently explain "ordinary mathematics", and more. NF might look even
more appealing to some logicians - notably, J. B. Rosser called his NF-based
FOM book "Logic for mathematicians".

>From conventional ZF viewpoint, NF troubles are caused by the axiom of
extenstionality

Ext = (forall x,y,z)(Eq(x,y) -> (x in z <-> y in z))

where

Eq(x,y) = (forall z)(z in x <-> z in y) .

For Con(NF-Ext), and even the strong normalizability of the corresponding
sequent calculus, is less problematic, as both reduce by standard methods to
the consistency of a suitable "small" fragment of ZF.

In the presence of Ext, however, conventional stratified cut elimination
requires stronger assumptions than plain consistency. The new requirements
refer to the domain completion axiom (DCA), or Herbrand-consistency, saying
that all objects are generated by operations. But DCA is hardly weaker than
NF.

To put it more exactly, denote by DCA[L] an instance of DCA saying that all
objects are generated by operations from a finite list L.
For example, in the number theory, DCA[0,S] stands for

(forall x)(x=0 or (exists y)(x=S(y))),

where S is the successor operation. Clearly DCA[0,S] is a trivial instance
of the ordinary induction axiom (schema) IND[0,S].

In NF-Ext, we have a finite list SEP of stratified operations
S1, ..., Sk (k<10), where Sj(parameters)={x : Aj(x,parameters)},
which can replace the ordinary infinite axiom (schema) of stratified
separation. Denote by CLOSURE[SEP] the list (or conjunction) of axioms
expressing that each Sj(parameters) exists, and by DCA[SEP] an axiom
expessing that every x is some Sj(parameters), j=1,...,k.

Moreover, we have  NF-Ext = CLOSURE[SEP]. 
 
Let us slightly modify every Aj such that

(forall x,y)(Eq(x,y) & Aj(x,parameters) -> Aj(y,parameters)).

Denote by SEPEq , CLOSURE[SEPEq] and DCA[SEPEq] the corresponding
specifications. CLOSURE[SEPEq] is weaker than CLOSURE[SEP], but
CLOSURE[SEPEq]+Ext proves CLOSURE[SEP].
Now DCA[SEPEq] proves Ext, and hence

THEOREM. NF is interpretable in CLOSURE[SEPEq]+DCA[SEPEq].

CONJECTURE 1. I conjecture that CLOSURE[SEPEq]+DCA[SEPEq] is consistent.

CONJECTURE 2. Furthermore, I conjecture that the PA-like strengthening
CLOSURE[SEPEq]+IND[SEPEq] is still consistent, where IND[SEPEq] refers to
the corresponding full stratified induction schema.

However, I don't believe that CLOSURE[SEPEq]+IND[SEPEq] can be interpreted
in ZF, or even ZF + LC, where LC stands for Large Cardinals (whatever the
contemporary specification). After all IND[SEPEq] says that the NF universe
is "very small", whereas LC says that the ZF universe is "very large".

Regards,
L. Gordeev

-- 
Lust, ein paar Euro nebenbei zu verdienen? Ohne Kosten, ohne Risiko!
Satte Provisionen für GMX Partner: http://www.gmx.net/de/go/partner