FOM: Effective Bounds in Core Mathematics

[Harvey Friedman]

I came across the new book

Marc Hindry, Joseph Silverman, Diophantine Geometry, Graduate Texts in
Mathematics, Springer, 2000.

This book specifically highlights four absolutely major results, referred
to as finiteness theorems. It also highlights a uniform logical issue
regarding all four of them.

The logical issue highlighted is that of effectivity. It appears that all
four of these results are Pi-0-3, and effectivity in its broadest sense is
simply the existence of a recursive Skolem function. However, it is
implicit in the way this is discussed there that they are also interested
in just how effective - i.e., bounds.

The logical isssue can also be couched in terms of constructivity.
Obviously all four of these major results are proved nonconstructively, and
no constructive proofs are known. A major challenge would then be to give
constructive proofs. A major challenge, in my view, although likely a much
easier challenge, is to determine if all four of these major results can be
proved in exponential function arithemtic.

But do the core mathematicians regard matters of effectivity as major
challenges? Well, let's see. Here is a verbatim quote of the relevant
material starting on page 456 of this book.

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

"F.4. The Search for Effectivity

Here is a brief list of the main results of Diophantine geometry that we
have proved in this book:

Mordell-Weil Theorem
The group of rational points on an abelian variety is finitely generated.

Roth's Theorem
There are only finitely many rational numbers alpha in K that approximate a
given irrational number beta to within H_K(alpha)^-2+epsilon.

Siegel's Theorem
A curve of genus at least 1 has only finitely many S-integral points.

Faltings' Theorem
A curve of genus at least 2 has only finitely many rational points.

All of these statements are purely qualitative; that is, they merely assert
that certain sets (of generators, numbers, or points) are finite. A major
challenge is to make these theorems effective,*) which means to give an
effective procedure for computing all of the elements in the finite set.
This generally means giving an effective upper bound for the heights of the
elements in the set, since one knows that there are only a finite number of
points of bounded height, and in principle it is then possible to list all
of them and check which ones are actually in the set. None of these
theorems has been proven effectively, although effective versions of
Siegel's theorem are known for many classes of curves (e.g., for all
elliptic curves) via techniques from trnascendence theory and linear forms
in logarithms. We also mention the related question of proving quantitative
results, which means giving an explicit upper bound for the number of
elements in the finite set. Quantitative versions of all of the above
theorems are known.

*) Also bear in mind that Matyasevic's negative solution to Hilbert's tenth
problem says that not all Diophantine problems can be solved effectively.
See Matyasevic [1] and Davis-Matyasevic-Putnam-Robinson [1]."

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

Constructivists should also bear in mind that the truth of these four
theorems is completely accepted by the mathematical community.