[FOM] Countable sets with imprediicative definitions

[Daniel Mehkeri]

> Can anyone provide examples of countable sets with impredicative
> definitions and apparently no alternative predicative definitions? Just
> to clarify, my intended notion of countable in relation to a set refers
> to the existence of a surjection from the natural numbers (or from the
> natural numbers excluding zero) to that set.

 Kleene's O was mentioned, but it is constructed from below in a sense. It
is
common especially in constructive mathematics to call that predicative (a
fortiori
Gamma_0 would be too).

But as far as I know nobody considers the power set of the natural numbers
predicative in any sense. Of course, that is uncountable. But Z_2,
second-order
arithmetic, is a formal theory. Assuming it has a model at all, then it has
a
countable model, by the downward Lowenheim-Skolem theorem. This model is
then a countable set with an impredicative definition, and no alternative
predicative
definition is known at this time. You might find this a simple and intuitive
example.

As I recall, Z_2 also happens to be equiconsistent with the System F that
was
mentioned.

Regards,
Daniel
-------------- next part --------------
An HTML attachment was scrubbed...
URL: /pipermail/fom/attachments/20101118/a36b7173/attachment.html