[FOM] Status of AC

[Harvey Friedman]

On 3/2/06 2:15 PM, "joeshipman at aol.com" <joeshipman at aol.com> wrote:

> How do you show that choice is eliminable from proofs of Pi^1_4
> sentences? 

Let M be a model of ZF + (therexists x)(A(x)), where phi is Pi13. Let M
satisfy A(x). Then A(x) holds in the L(x) of M, and M satisfies ZFC. QED

>And how much of an expansion in proof length is involved in
> the elimination procedure?

The same as for all such things. It is most interesting only if ZF and ZFC
are formalized realistically with abbreviation power. I haven't gone into
this in detail, but certainly at most a very small linear factor plus a
significant constant. It could well be a lot better than this. I can look
into this more closely when I have the time.
> 
> I would hazard a guess that the Sigma^1_4 sentence he
> describes (which is provable in ZFC but not in ZF) cannot actually be
> formalized in second-order-arithmetic in fewer than 10,000 symbols (I'm
> talking about the length of the sentence, not of its proof!).

Far far fewer than that, with abbreviation power. Relative constructibility
is not all that bad given my
http://www.cs.nyu.edu/pipermail/fom/2006-February/009780.html

On 3/2/06 11:36 AM, "Andrej Bauer" <Andrej.Bauer at andrej.com> wrote:

> On Thursday 02 March 2006 08:23, Harvey Friedman wrote:
>> It is provable in ZF that the product of any countably infinite sequence of
>> two point spaces (each with the discrete topology) is compact.
>> 
>> It is not provable in ZF that the product of any countably infinite
>> sequence of three point spaces (each with the discrete topology) is
>> compact.
> 
> Both claims cannot hold, since {0,1}^omega and {0,1,2}^omega are obviously
> homeomorphic, 

True. And they are provably compact in ZF.

>therefore they are either both compact or both non-compact. My
> bet is that ZF does _not_ prove them to be compact.
 
Are you basing you claim on the provability of

"the product of any infinite sequence of two point discrete spaces is
homoeomorphic to {0,1}^omega"

and

"the product of any infinite sequence of three point discrete spaces is
homeomorphic to {0,1,2}^omega"

in ZF?

Harvey Friedman