FOM: a comment on a post by Mathias

[holmes@catseye.idbsu.edu]

Mathias said:

5. The point of psychological divergence of the two schools seems to be 
Mostowski's isomorphism theorem, (MIT for short),  
that every extensional well-founded relation 
is isomorphic to a transitive set, with its corollary that every well-ordering 
is isomorphic to a von Neumann ordinal. 

MIT is essential to modern set theory, but rejected with passion by 
Mac Lane and his school.   

6. MIT is not provable in Mac Lane' system Mac (nor in Zermelo's), 
its proof requiring instances of the axiom scheme of collection 
which are not available in those systems; but, 
ironically, there is a natural interpretation of Mac + MIT in Mac, so that 
the two systems are equiconsistent. Similar comments apply to 
the systems Zermelo + MIT and Zermelo. 

[See my paper "The Strength of Mac Lane Set Theory", to appear in the 
Annals of Pure and Applied Logic, for the proofs of these and other 
remarks.] 
 
My comments:

first, the paper Mathias mentions is wonderful; all of us should read it.

second, the status of MIT in NFU (which doesn't fit altogether comfortably
into either of the categories of theories Mathias proposes earlier in 
that post:  NF and NFU have untyped variables with a different restriction
on comprehension than the separation axiom of Zermelo -- the original 
motivation of the NF comprehension axiom was of course type-theoretical):

the Mostowski isomorphism theorem is provably false in NFU -- in fact,
it is provable that there are well-orderings longer than the order
type of any von Neumann ordinal (which disproves MIT by disproving an
important special case).  Like many phenomena in NFU, the result cited
above becomes much less mysterious when one looks at what is going on
in models.  Technical reasoning about von Neumann ordinals in NFU is
interesting because it is one of the more accessible things one can do
in NFU which has no analogue in type theory.  (Most remarks here apply
to NF, but we have no (known) models of NF).

Nonetheless, NFU (+ a suitable infinity axiom) allows one to interpret
Mac + MIT (or any Zermelo-style theory if stronger infinity axioms are
used). One interprets Zermelo-style set theory in Quine-style
set theory by investigating the theory of isomorphism types of
well-founded extensional relations, which is also the technique
Mathias uses (of course working in Mac) for relative consistency
arguments in the paper he cites above.

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.boisestate.edu
not glimpse the wonders therein. | http://math.boisestate.edu/~holmes