[FOM] Yablo, Mirimanoff, and Negative Types
Roger Bishop Jones
rbj at rbjones.com
Tue Sep 17 17:25:46 EDT 2002
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
More information about the FOM
mailing list