[FOM] Yablo, Mirimanoff, and Negative Types

[A.P. Hazen]

Comments on Roger Bishop Jones's comments.
   (i) Jones says he "would have expected" that the type-theoretic language
wouldn't permit formulation of the (relevant sense of) well-foundedness.
Well, yes, now that you mention it, it ISN'T surprising.  To say a set (in
an -- orthodox or negative -- type system) is well-founded is to say
something about what happens arbitrarily many types BELOW it: set-to-member
chains ULTIMATELY terminate.  So it wasn't really to be expected that the
typed language (in which each variable ranges over the objects of a single
type) would be able to express this.  Still, Yablo's argument gives a nice
clean proof.
   (ii) Nonexistence of standard models.  There is an old result (it MAY be
due to Hintikka, "Reductions in the Theory of Types," an "Acta Philosophica
Fennica" monograph (?) from the 1950s) that, just as Second-Order Logic
(with the "standard" -- non-Henkin -- interpretation) can characterize the
natural number series categorically, it can characterize the "standard
model" of Third-Order Logic, or of full Finite Type Theory, up to
isomorphism.  You just say that the model is (a) a model of the language
with a single dyadic predicate (epsilon), that (b) its domain partitions
into SUBSETS forming an omega-sequence,  (c) for every SET of elements from
one cell of the partition, there is exactly one member of the next cell to
which they all bear the epsilon relation, and (d) the epsilon relation
doesn't do anything else.  (I haven't tried to formulate that precisely; I
hope the idea gets across.  The capitalized words represent Second-order
quantifiers in the characterizing language.)  The technique seems broadly
applicable: assuming we know what the standard interpretation of
Second-Order Logic is, we can DEFINE the notion of a standard model of some
other type-theoretic logic.  Natural question, then, is
    * Does the system of negative types have standard models?
The last time I thought about this question, the nearest thing I came to
answering it was to note that, by Cantor's Theorem, the objects of each
Type would have to be more numerous than the objects of the preceding type,
so that the existence of a standard model would imply the existence of a
descending sequence of cardinalities... which is not something that will
make you popular in circles that like the set-theoretic Axiom of Foundation
and the "Iterative Conception of Set," but left the puzzle of whether the
existence of standard models of negative type theory is consistent with
some weird-but-not-too-weird set theory.  Yablo's argument, it seems to me,
establishes a much stronger "no-standard-model" theorem for Negative Type
Theory.
---
Allen ("the longwinded") Hazen
Philosophy Department
University of Melbourne