[FOM] Definable sets in ZFC
paul at mtnmath.com
Wed Sep 22 12:48:43 EDT 2010
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
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.
More information about the FOM