[FOM] Yablo, Mirimanoff, and Negative Types

[Roger Bishop Jones]

On Tuesday 17 September 2002  8:50 pm, Roger Bishop Jones wrote:
> On Tuesday 17 September 2002  2:14 pm, A.P. Hazen wrote:
> >    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.
>
> And hence cannot have the "standard semantics"
> for a higher order logic, i.e. some of the power sets must be
> incomplete.
>
> So though the theory is consistent when formulated as
> a many-sorted first order theory, it is semantically inconsistent
> (i.e. has no models) when formulated as a type theory
> with "standard semantics".

Sorry, this is all wrong!

I have confused two senses of "express well-foundedness"
a type theory.
The first applies to formulating set theory in a type theory
and in this sense well-foundedness is expressible iff
the semantics is standard.
However, the sense relevant to the posting I responded
to concerned well-foundedness across the types,
(and here I would have expected the type system to
preclude expression of well-foundedness irrespective
of the semantics).

Roger Jones