[FOM] impredicative definitions/paper announcement

[Daniel Mehkeri]

Vaughan Pratt asks:
> Among these and other notions of predicativity, is there one (or more)
> such that the set of quotients of N by an equivalence relation that is
> r.e. but not recursive is impredicative?
>
> (This is relevant to the discussion by virtue of being a countable set.)
>
> Intuitively I would tend to think of this as a predicative set, but I'm
> having difficulty seeing why a proof of (or argument for) its
> predicativity could not be adapted to at least some of the other
> examples suggested, e.g. Dana's.  What is the essential feature(s) of
> those examples that makes them impredicative and this one not?

The way I read Dana Scott's example (which was better than mine), it
was in terms of truth, not provability, so this is not applicable.

Even as far as provability goes, there is still a sense in which the
sets are impredicative. Given a formal system T, the set of sentences
of T, modulo provable equivalence in T, can always be constructed
unproblematically, as you say. But to show the set is not trivial
requires showing that the system is consistent. In this case,
second-order arithmetic has no predicative consistency proof.
Similar considerations apply to the two-element set {T,F} of provable
and refutable sentences; the impredicativity comes in showing it has
two elements.

Regards
Daniel