[FOM] Yablo, Mirimanoff, and Negative Types

[A.P. Hazen]

   Mirimanoff's Paradox concerns the "set" of all well-founded sets, which
must be both well-founded and non-well-founded.  Yablo has suggested for
our consideration an intriguing variant: what happens if we assume that the
"universe" of sets considered is that of a model of the theory of (positive
and negative) types.  This theory -- Yablo's "Clarification" post refers us
to Hao Wang's original presentation of it -- is an axiomatic system like
the familiar theory of types (as in, e.g., ch. XI of Quine's "Set Theory
and its Logic"; other presntations are in Hatcher's "The (Logical)
Foundations of Mathematics" and Fraenkel and Bar-Hilel's "Foundations of
Set Theory"), formulated in a  many-sorted quantificational language, with
axioms of comprehension for each  type.  The difference is that the "types"
of the "intended model", and so, formally, the sorts of variables, are
indexed by the integers rather than by the natural numbers.  There is thus
no lowest type, so EVERY type is a type of "sets," and there are
comprehension axioms for LITERALLY every type (standard type theory doesn't
have comprehension axioms for the lowest type: individuals aren't generated
THAT way).
   We know that there ARE well-founded sets of each type in a model of this
theory: the null set of each type is well-founded, so is the unit set of
the next lower type's null set, and so on.  (If X is a well-founded set at
some type, every descending membership chain from it must terminate, after
finitely many steps, at the null set of some type or other.)  But now Yablo
deploys a variant of Mirimanoff.  A set of well-founded sets must itself be
well-founded, so the set(1) of all well-founded sets(2) of a given type
ought to be a well-founded set(2) of the next higher type, and so (since
every type contains well-founded sets) we get an infinite descending chain
of "sets-of-all-wf-sets."
   What happened?  We know that the theory of negative types is consistent
(any finite set of its axioms can, by appropriate reinterpretation of the
type-symbols occurring in axioms belonging to the set, be interpreted as
axioms orthodox type theory).  So there are (by Gödel 1930) models of the
theory of negative types.  So Yablo's variant of Mirimanoff can't be turned
into a derivation of a contradiction WITHIN the theory of negative types.
What saves us?  It seems to me that it has to be that the language of
negative type theory is not expressive enough to formulate the condition
"is a well-founded set of type x": otherwise the comprehension axiom would
force the set of well-founded type-x sets to be a set of type x+1, and we'd
be in the soup.  Thus, in the previous paragraph, "set(2)" refers to
objects IN the model of negative type theory, but "set(1)" is
metalinguistic, referring to a set OF objects in the model which is not
itself REPRESENTED by an object in the model.
   If I'm right, Yablo has given us the proof of a theorem in the
metatheory of negative type theory: it's language can't express
well-foundedness.
    I think that's a very nice result!  Thank you, Steve!
---
Allen Hazen
Philosophy Department
University of Melbourne