FOM: Harvey Friedman's distinctions

[Martin Davis]

I am lamentably ignorant of category thory. But I know very well an example
that I think brings some of what is being discussed into focus. I'm thinking
of a theorem due to Norbert Wiener. I'll use "sum" to mean sigma from n =
-infimity to +infinity; i is sqrt(-1). The theorem concerns the ring R of
functions f representable in the form:
                f(t) = sum a_n exp(nit)
where sum |a_n| is finite. 

Theorem. If f is in R and 1/f never vanishes for any real t, then 1/f is in R.

Wiener's original proof is a complicated and lengthy piece of "hard"
analysis. It's been decades since I looked at it, but I have no doubt that
it could be carried out in a suitable conservative extension of PA (and
likely even of something much weaker).

In his classic paper on normed rings (now called Banach algebras), Gelfand
obtained this theorem as a simple corollary of very general considerations.
Gelfand's proof uses the fact that every ideal in R is contained in a
maximal ideal (an example Harvey mentioned) as well as the Hahn-Banach
theorem, and so uses AC. I have little doubt that this use of AC is
"inessential" (I would never say "fake"; Gelfand wasn't trying to fool
anyone, he just wasn't concerned about eliminating references to AC.) I
haven't tried to verify this, but I'd be astonished if AC is needed for the
particular instances in question.


                           Martin Davis
                   Visiting Scholar UC Berkeley
                     Professor Emeritus, NYU
                         martin at eipye.com
                         (Add 1 and get 0)
                       http://www.eipye.com