[FOM] Definable sets in ZFC

[Monroe Eskew]

On Wed, Sep 22, 2010 at 9:48 AM, Paul Budnik <paul at mtnmath.com> wrote:
> There are at least two versions of this, both of them interesting.
>
> 1. The least ordinal not provably definable in ZF.
>
> 2. The least ordinal not definable in the language of ZF.

Ali Enayat pointed out these two are the same for any given model of
ZF.  If F(x) is a formula for which there is a unique ordinal \alpha
satisfying F(\alpha), then there is another formula G(x) which holds
of \alpha and only \alpha, and for which ZF proves there is a unique
ordinal satisfying it.

However, one should keep in mind that the notion "F(x) defines \alpha"
is not absolute.  One model may have a unique countable ordinal such
that F(\alpha), in another such an ordinal may not exist, in another
it may not be unique, in another \alpha maybe be uncountable, in
another F may define some \beta different from \alpha.



> Through expanding and generalizing this process I think
> we will eventually be able to understand how to expand the language of
> ZF to define larger countable ordinals than those definable in the
> language of ZF.

 A model of Morse-Kelley set theory can define the least ordinal not
definable in the language of ZF.