Hahn-Banach and the axiom of choice?

The general statement of the Hahn-Banach theorem is undecidable in ZF.
AC implies it, but the converse is not true; however, HB does imply
strange things such as non-Lebesgue measurable sets.

First, they're telling me in freenode ##math that for the
finite-dimensional case, HB is provable in ZF, and that this is
apparently obvious from the proof of it. Nobody had a reference, so
I'm not sure this is true. Can anyone confirm here whether or not ZF
proves this for the finite-dimensional case - and for any choice of
seminorm, no matter how strange? It seems somewhat likely to me that
it would be true for all Lp norms on finite-dimensional spaces, but
what about other weird norms, like Kees seminorms or whatever?

Second, even if this is true for all norms and with finite-dimensional
vector spaces, I'm not sure if we're going to run into trouble with
this for the countably infinite-dimensional case, which is a direction
Keenan's been leading us into for some time. Does anyone know if HB is
still true for the "ω-limit" case? Or, alternatively, will we run into
weird things like undefinable TOP tunings which mathematically "exist"
but which you can't play or define?

-Mike

--- In tuning-math@yahoogroups.com, Mike Battaglia <battaglia01@...> wrote:

> First, they're telling me in freenode ##math that for the
> finite-dimensional case, HB is provable in ZF, and that this is
> apparently obvious from the proof of it. Nobody had a reference, so
> I'm not sure this is true.

Sure, you only need to make a finite number of choices. Finite choice is true in ZF, though even countable choice isn't. I was thinking of mentioning this when discussing uniqueness and Zorn's Lemma, which is far more powerful than needed, but then figured what the hell.

> Second, even if this is true for all norms and with finite-dimensional
> vector spaces, I'm not sure if we're going to run into trouble with
> this for the countably infinite-dimensional case, which is a direction
> Keenan's been leading us into for some time.

You will, as then you'd need countable choice.

--- In tuning-math@yahoogroups.com, "genewardsmith" <genewardsmith@...> wrote:
> > Second, even if this is true for all norms and with finite-dimensional
> > vector spaces, I'm not sure if we're going to run into trouble with
> > this for the countably infinite-dimensional case, which is a direction
> > Keenan's been leading us into for some time.
>
> You will, as then you'd need countable choice.

Perhaps no one cares, but my personal belief is that countable choice is true (even though the axiom of choice is false). So I can't see myself having philosophical problems with any of the math that's actually useful for tuning. (In particular, the claims Mike enjoys making that end in "...assuming the axiom of choice" don't actually require it.)

Keenan

On Tue, Jul 31, 2012 at 3:55 PM, Keenan Pepper <keenanpepper@gmail.com> wrote:
>
> Perhaps no one cares, but my personal belief is that countable choice is true (even though the axiom of choice is false).
> So I can't see myself having philosophical problems with any of the math that's actually useful for tuning. (In particular, the claims Mike enjoys making that end in "...assuming the axiom of choice" don't actually require it.)

This wasn't meant to be philosophical, but to figure out what it means
that the existence of ω-limit Lp tunings that perfectly restrict down
to subgroup Lp tunings is, in general, undecidable in ZF.

-Mike