[FOM] 608: Integer and Real Functions 2

Harvey Friedman hmflogic at gmail.com
Tue Sep 1 06:40:18 EDT 2015


There were a lot of replies to 605
http://www.cs.nyu.edu/pipermail/fom/2015-August/018931.html

http://www.cs.nyu.edu/pipermail/fom/2015-August/018933.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018935.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018940.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018941.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018946.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018947.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018947.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018949.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018949.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018960.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018960.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018961.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018972.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018970.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018950.html
http://www.cs.nyu.edu/pipermail/fom/2015-August/018966.html

http://www.cs.nyu.edu/pipermail/fom/2015-August/018950.html pointed out to
me something I find very striking, even if Tim Chow was doubting that I
would:

https://en.wikipedia.org/wiki/Bohr–Mollerup_theorem  The Bohr Mollerup
theorem characterizing the Gamma function.

I found http://ms.mcmaster.ca/~speisseg/blog/?p=2688

where it is claimed that the Gamma function on (0,infinity), just what we
were talking about, is o-minimal when added to the field of real numbers -
backed up by http://plms.oxfordjournals.org/content/81/3/513 Also there,
you can add the Gamma function plus a lot of other functions, including the
exponential function, and retain o-minimality.

​So we ought to be able to use o-minimality effectively as a tool for
picking out good functions. E.g., we should be able to prove

THEOREM(?) Let f:[0,inifnity) into [0,infinity) satisfy f(0) = 1, f(x+1) =
xf(x), and (R,+,dot,f,exp) be o-minimal. Then f is the Gamma function.

The proof should go something like this. f is going to have to be
eventually log concave upward or eventually log concave downward, by the
o-minimality. I think the eventual concave downward must be nonsense, and
so it is eventually log concave upward. So it is eventually the Gamma
function. But by the functional equation, it is the Gamma function.

GENERAL PRINCIPLE(?). For a lot of functional equations, there can be at
most one solution which is o-minimal together with exponentiation, or maybe
even sometimes without exponentiation.

Now let's look at the functional equation f(n+1) = e^f(n), f(0) = 1. The
idea is that a good solution should be really nice, going sharply up all
the time, nice and smoothly. Like e^x but only faster. Now e^x has
derivatives of all orders at 0 that are 1. This is bounded away from 0. It
seems sensible to require that of f. But then you get into trouble I think,
with derivatives of all orders everywhere on [0,infinity) positive, and
growing fast. The former, if I remember right, implies real analyticity,
and the latter makes real analytically impossible. So there seems to be no
solution to that equation of the kind we would be naturally looking for.

What is the best correct theorem of this kind ruling out any decent
solution to that equation? Maybe we can also show outright that there
cannot be such an f where (R,+,dot,f,exp) is o-minimal?

And what about compositional square roots?

THEOREM(???) There is no compositional square root of e^x that is o-minimal
when combined with exponentiation, as we have been discussing above.

******************

Coming back to the natural numbers for the moment, recall my Count
Arithmetic, which is a formal system which is in some ways preferable to
our old friend PA = Peano Arithmetic. Addition and multiplication are
derived notions coming out of the count operator # on formulas with free
variables. See 176: Count Arithmetic 6/10/03 8:54AM
http://www.cs.nyu.edu/pipermail/fom/2003-June/006743.html

and followups

http://www.cs.nyu.edu/pipermail/fom/2003-June/006746.html
http://www.cs.nyu.edu/pipermail/fom/2003-June/006752.html
http://www.cs.nyu.edu/pipermail/fom/2003-June/006748.html

We can extend Count Arithmetic to incorporate exponentiation by adding a
power set operation on finite sets, and presumably get a good
axiomatization of EFA. Also, factorial can be thrown into the mix.
Incidentally, what if all of this Count Arithmetic is revisited from the
intuitionistic/constructive standpoint?

Now let me mention a computational project.

Start with the base 2 exponential function defined on {0,...,30}. We are
looking for a "good" compositional square root of this function. Do some
experimental math here to see what is nice. Experimentally play with your
experimental compositional square root at the numbers in {0,...,30}. Start
developing some numerical criteria for how it should behave. Maybe find
some interesting conditions, and see if they can be satisfied armed with
your favorite big computer.

************************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 607th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
​607: Hindman's Theorem  ​

​Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150901/6345712b/attachment-0001.html>


More information about the FOM mailing list