FOM: Re: Intuitionism, Godel

[Ulrich Kohlenbach]

In a recent posting H. Friedman wrote:

>Falting's theorem is grossly
>nonconstructive in content and proof right now. It has the form that
>something is true in the integers with finitely many exceptions, without a
>bound on the number of exceptions, and certainly not a bound on the size of
>the exceptions. The same with Roth's theorem on approximations to algebraic
>numbers. 

I would like to point out that in the case of Roth's theorem there are 
effective bounds on the number of exceptions (but not on their size). 
The oldest one is due to Davenport and Roth in their paper 
"Rational approximations to algebraic numbers" (Mathematika, vol. 2,pp. 160-
167, 1955). It is exponential and was improved to a polynomial bound 
independently by Luckhardt (by an unwinding of a proof of Roth's theorem 
due to Esnault/Viehweg and using some earlier ideas of G. Kreisel about 
possible unwindings of finiteness theorems) in "Polynomiale Anzahlschranken" 
(JSL 54, pp. 234-263, 1989) and Bombieri/van der Poorten in "Some 
quantitative results related to Roth's theorem" (J. Australian Math. Soc, 
vol. 45, pp. 233-248, 1988).    

Ulrich Kohlenbach