FOM: consistency of NF from a measurable

[Randall Holmes]

Harvey Friedman's latest post about the power shift axiom implies that
the consistency of NF follows from the existence of a measurable
cardinal in NBGC, if Theorem 2 is really a theorem.

Harvey claims (Theorem 2) that NBGC + measurable interprets NGB +
power shift.

In NGB, we can define a natural model of the theory of types based at
any set x (a disjoint union of the iterated power sets of x will do
it).  The theory of this model depends only on the cardinality of x.
For any finite set of sentences in the language of TT, we can define a
class map V -> omega capturing the truth values of those sentences in
the natural model of TT with base x.  By the power shift axiom, it
follows that there are sets x and y with 2^|x| = |y| such that the
theory of the models of TT based at x and y are the same with respect
to that finite set of sentences.  It follows that the theories of the
models of TT based at x and the power set of x are the same (because
the theory depends only on cardinality), from which it follows that
the model based at x is ambiguous with respect to that finite set of
sentences.  From this it follows by compactness that the full scheme
of ambiguity is consistent with the theory of types, from which it
follows that NF is consistent.

I would like to see the proof of Theorem 2 -- or is it a conjecture?

Or am I misreading something?

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes