Intuitively, a constructively irrational number is one for which we can effectively separate it from any rational number in terms of the latter's denominator. More formally, a constructively irrational number is a number $x$ such that there is a known primitive recursive function $f : \mathbb{Z}^+ \rightarrow \mathbb{Z}^+$ such that $|x – \frac{p}{q}| > \frac{1}{f(q)}$ for all $p, q \in \mathbb{Z}$ such that $q \neq 0$. This corresponds closely to what is meant by "irrational" in constructive mathematics, where "irrational" is interpreted as stronger than "not rational" (indeed, strictly stronger).
For example, $\sqrt{2}$ is constructively irrational, given that $|\sqrt{2} – \frac{p}{q}| > \frac{1}{3q^2}$.
Which theorems of irrational number theory are known to also hold for constructively irrational numbers? In particular, are all algebraic irrational numbers constructively irrational? Are $\pi$ and $e$ constructively irrational? What about $e^n$ for $n \in \mathbb{Z}$ and $n \neq 0$? Or $\ln{n}$ for $n \in \mathbb{Z}^+$ and $n \geq 2$? And finally, is $\log_p{n}$ constructively irrational for $p$ a prime, $n \in \mathbb{Z}^+$, and $n$ not an integer power of $p$?
Answers to any of these questions would be greatly appreciated.
Best Answer
All algebraic numbers are by this definition constructively irrational. You can adopt Liouville's proof that Liouville numbers are transcendental and turn it in the other direction to get a function of the sort you want given an algebraic number and its corresponding polynomial. Explicit versions of Baker's theorem also can be thought of as a similar statement. Baker's sort of methods also give you your desired result for a lot of logarithms.
What you are interested in is also closely connected to the idea of irrationality measure. In particular, Mahler's theorem on the irrationality measure of $\pi$ may be enough to show that $\pi$ is constructively irrational. For the best bounds currently on that, see this paper by Doron Zeilberger and Wadim Zudilin. I say "may" here because there are epsilons floating around there and I haven't checked to see if they can be made explicit.
A quick aside about a number you didn't ask about but I'm now wondering about: I don't know if Apery's proof that $\zeta(3)$ is irrational can be turned into a proof of constructive irrationality. My guess is that things there are much too delicate.