[FOM] consistency of NF?

[Lew Gordeew]

Hi,

First off, Crabbé argued in the natural deduction calculus. Strong
normalization (cut elimination) theorem in the corresponding sequent
calculus formalism of NF minus Ext was presented in my 1988 talk in
Oberwolfach, see also L. Gordeev, Strong normalization and realizability,
Bull. of Symb. Log. 1 (1995), 109-110. This theorem is stronger than Crabbé
result. Actually, I proved that sequent-calculus strong normalizability of
NF minus Ext is provable within Zermelo set theory extended by the existence
of the power-set hierarchy along aleph-omega.

Second, in my 1988 appendix, I also pointed out that an extended proposition
asserting strong normalizability of the corresponding intuitionistic
sequent-calculus abstract-term formalism of NF minus Ext extended by
standard omega-rules already implies the consistency of full NF. I also
conjectured that this proposition is true, but not provable in any known
extension of ZF and/or NF. (Hint: in the presence of omega-rules, standard
cut elimination arguments can't be formalized in standard set theoretical
formalisms.)

Regards,
LG
 
> Dear FOM'ers,
> 
> I am looking for refutations of a purported proof of the consistency
> of NF, which is found at the head of the Current Research section of
> my web page
> 
> http://math.boisestate.edu/~holmes/holmes/nfconsistency.ps
> 
> This is a quite brief argument, but it does require one to read a (very
> nice) paper of Marcel Crabb\'e:
> 
> Marcel Crabb\'e, ``The
> Hauptsatz for comprehension, a semantic proof'', {\em Mathematical
> Logic Quarterly\/}, 40 (1994), 481-489.
> 
> in which he proves cut-elimination for NF with no extensionality axiom.
> It appears to me at the moment that with a slight additional twist this
> can be turned into an NF consistency proof.
> 
> While I believe this at the moment, I certainly don't quite meta-believe
> it, so I await refutation with interest.
> 
> --Randall Holmes
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
> 

-- 
DSL Komplett von GMX +++ Supergünstig und stressfrei einsteigen!
AKTION "Kein Einrichtungspreis" nutzen: http://www.gmx.net/de/go/dsl