[FOM] purported proof of Con (NF)

[Randall Holmes]

Dear NF-istes (cc FOM list),

This argument appears to have a serious defect.  It hinges on 
an idee fixe I have about cut elimination:  there's a consequence
that I persist in thinking should follow from cut elimination for
type theory (and which perhaps even does follow) but seems to be
beyond my ability to prove so far.

I do think I'm right that a Forster term model of the restricted
comprehension axiom described in the note would be a model of NF,
and perhaps that is an interesting fact, but I have no idea how
to construct such a model!  This does serve to illustrate my contention
that Forster's notion of term model is a very strong notion.

I do encourage people to look at Marcel's paper on cut elimination!

--Randall Holmes