5
$\begingroup$

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.

Improve this question
$\endgroup$
5
  • $\begingroup$ I believe one can prove $e$ is constructively irrational using your definition, but probably not $\pi$. Certainly it is not known how to show that any real algebraic number with degree greater than two is constructively irrational. $\endgroup$
    – Stanley Yao Xiao
    Commented Sep 13, 2021 at 0:23
  • 2
    $\begingroup$ @StanleyYaoXiao, I am confused by your last sentence... What about Liouville's inequality, as in JoshuaZ's answer...? Is there a typo that belies your intent? $\endgroup$
    – paul garrett
    Commented Sep 13, 2021 at 1:31
  • $\begingroup$ @paulgarrett I was thinking about how it is not known in general how to show for any $\varepsilon > 0$ that that there are only finitely many reduced rational numbers $p/q$ such that $|\alpha - p/q| < q^{-2 + \varepsilon}$ when $\alpha$ is real-algebraic of degree 3 (i.e., Roth's theorem is ineffective) $\endgroup$
    – Stanley Yao Xiao
    Commented Sep 13, 2021 at 2:58
  • $\begingroup$ @StanleyYaoXiao, ah! Thanks for clarifying. $\endgroup$
    – paul garrett
    Commented Sep 13, 2021 at 3:46
  • $\begingroup$ My answer here also answers many of your questions: mathoverflow.net/questions/345810/… $\endgroup$
    – user44143
    Commented Sep 13, 2021 at 5:50

1 Answer 1

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
8
  • 1
    $\begingroup$ For algebraic numbers $f$ is just a polynomial. For $\zeta(3)$, according to Apery's proof it is superpolynomial but still primitive recursive. Frankly I do not quite understand the "primitive recursive" requirement in the definition. Why not simply "recursive"? $\endgroup$
    – markvs
    Commented Sep 13, 2021 at 1:35
  • $\begingroup$ @MarkSapir How do you do that for Apery's proof? Is there somewhere where someone has made that construction explicit? (I've seen Apery's proof and it isn't obvious to me that you can get such a function out of it, but it isn't a proof I understand very well.) $\endgroup$
    – JoshuaZ
    Commented Sep 13, 2021 at 1:38
  • 2
    $\begingroup$ I just looked at the en.wikipedia.org/wiki/Ap%C3%A9ry%27s_constant#Fast_convergence $\endgroup$
    – markvs
    Commented Sep 13, 2021 at 1:49
  • 1
    $\begingroup$ @MarkSapir Hmm, but doesn't that go in the other direction? That shows that tells us that such an $f(x)$ must grow fast. It doesn't tell us that such an $f(x)$ exists or how to compute it. $\endgroup$
    – JoshuaZ
    Commented Sep 13, 2021 at 1:52
  • 1
    $\begingroup$ @MarkSapir Using primitive recursive avoids unbounded search/Markov's principle. Some constructivists don't like Markov's principle. $\endgroup$
    – Arno
    Commented Sep 13, 2021 at 8:27

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .