[FOM] Definable sets in ZFC

[Paul Budnik]

  On 09/16/2010 03:21 PM, Max Weiss wrote:
>   5) The "least indefinable ordinal" might be worth thinking about here.
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.

I am not sure what the least ordinal not provably definable in ZF is 
but, with some additional restrictions, one can define something 
similar. The union of the recursive ordinals for which one provably has 
the Gödel number of a recursive notation, is the least ordinal not 
provably definable in this way. A recursive notation provides notations 
for all smaller ordinals so there cannot be smaller undefinable ordinals.

If one had an explicit recursive notation for this ordinal I think one 
would be a long way down the road to constructing a recursive notation 
large enough to prove the consistency of ZF.

Since all recursive ordinals are definable by a recursive notation and 
every recursive process is definable in ZF, every recursive ordinal is 
definable in the language of ZF, but of course there is no general way 
to decide which potential definitions are correct. One way the language 
of ZF might be extended is by generalizing the idea of recursive ordinal 
notation.

The recursive ordinals are definable in terms of recursive processes 
that accept an arbitrary number of integer inputs and halt for every 
possible sequence of inputs. Such a TM is said to be WF (well founded). 
One can extend the idea of a recursive ordinal notation by considering 
TMs WF for infinite sequences of various types. For example we can have 
a TM WF for all sequences of Gödel numbers of notations for recursive 
ordinals. We can iterate this up to any ordinal we can define using this 
process. Writing computer code that does this seems essential to manage 
the complexity. 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.

Paul Budnik
www.mtnmath.com