[FOM] Roth's Theorem; Liouville numbers

[Timothy Y. Chow]

I wrote:
>Maybe if all you want is a primitive recursive bound then Mahler's proof 
>can be simplified, but I've not heard of anyone doing that.

I should have checked MathSciNet before posting.  Here is the first half 
of the Mathematical Review of R. L. Goodstein, "The recursive 
irrationality of pi," J. Symb. Logic 19:267-274.

---
A (primitive, general) recursive sequence of rational numbers $s_n$ is 
(p., g.) recursively convergent when there exists a (p., g.) recursive 
function $n (k)$ such that for $n\geq n(k)$, $|s_n-s_{n(k)}|<2^{-k}$. The 
sequence is (p., g.) recursively irrational when there exist also (p., g.) 
recursive functions $i(p,q)$ and $N(p,q)$ such that for $n\geq N(p,q)$, 
$|s_n-p/q+1|>1/i(p,q)$. The sequence is strongly (p., g.) recursively 
convergent in the scale $r$ when there exists a (p., g.) recursive 
function $n(k)$ such that for $n\geq n(k)$, $[r^ks_n]=[r^ks_n]$.

The author constructs a primitive recursive sequence whose limit is the 
zero of the Maclaurin series for $\sin x$ at $\pi$. This sequence is such 
that he is able to prove its primitive recursive irrationality, and to 
obtain a primitive recursive bound on the number of consecutive 
occurrences of a given block of digits in the decimal expansion of $\pi$. 
[...]
---

By the way, I share Steve Simpson's puzzlement at Jacques Carette's post.
As far as effectivity is concerned, the choice of base and the BBP formula 
don't seem relevant.  All we need to do to show that the nth digit of pi 
(in any base) is a recursive (as opposed to a primitive recursive) 
function of n is (1) an algorithm for computing pi to arbitrarily high 
precision and (2) a proof that pi is irrational.  Computing pi to high 
precision will give you the nth digit unless you encounter the repeating 
9's problem, but if you know that pi is irrational, then you know that you 
will eventually resolve the ambiguity by computing far enough.

The BBP formula allows you to compute the nth binary digit of pi without 
computing all the previous digits, but this is a separate issue from 
effectivity.

After saying this, I wonder now whether one could solve Simpson's exercise 
by taking a simple proof that pi is irrational and extracting a primitive 
recursive bound from it.  I took a look at Niven's famous proof that pi is 
irrational:

http://pi314.at/math/misc/irrational_niven.pdf

Unfortunately, since he's concerned with slickness rather than with 
computational issues, the proof is phrased as a proof by contradiction.  
Note that there's an old Putnam problem which required the solver to show 

0  <  integral_0^1 x^4 (1-x)^4 / (1+x^2) dx  =  22/7 - pi.

I suspect one can fiddle with Niven's proof to get a suitable 
generalization of the Putnam problem, which would give a primitive 
recursive handle on the difference between pi and any given rational.  
It would be too weak to get an irrationality measure like Mahler's, but 
would suffice for Simpson's exercise.

Tim