[FOM] purported proof of Con (NF)
holmes at diamond.boisestate.edu
Sat Feb 26 23:37:21 EST 2005
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!
More information about the FOM