Prove constructively that $\log_2 3$ is irrational.

Question

The usual proof that $\log_2 3$ is irrational is by contradiction. For instance:

Assume the negation: that $\log_2 3 = m/n$ for some integers $m$ and $n$. Then, by the property of logarithms, $2^{m/n} = 3$, which implies that $2^m = 3^n$. However, $2^m$ is even and $3^n$ is odd and an even number cannot be equal to an odd number. Therefore the assumption that $\log_2 3$ is rational is wrong.

My understanding is that this form of proof by contradiction (assume the negation and arrive at a contradiction) is using the law of excluded middle (that proving $\lnot \lnot A$ is the same as proving $A$) and is therefore not a valid constructive proof.

So that leads to my two-part question:

• Is the proof actually okay as a constructive proof (i.e., is my understanding wrong) and if so, why is it okay?
• If it is not valid, what is a constructive proof that $\log_2 3$ is irrational?

Answer 1

$x$ is irrational is defined as "$x$ is not rational", so a proof that shows that from the assumption that $x$ is rational we derive a contradiction is a valid constructive proof for "$x$ is not rational", in fact it's the usual proof for such negative statements in e.g. intuitionistic logic.

Answer 2

Remarking over Henno Brandsma's answer, it is true that irrationality may be defined as the absurdity of rationality. Another convention that is commonly used for irrationality, for instance in Bishop, is being bounded away from every rational number. Note that this is an affirmative property, as one has to provide a positive distance away from the number of interest for every rational number.

In that regard, you have technically done the heaviest part of the proof already by noting that $2^m\neq 3^n$ (in the strong sense!) for all pairs of integers $n$ and $m$ with $n>0$. The rest just utilizes the strong injectivity of logarithms and of real division: $$n\log_2(3)\neq m,$$ and $$\log_2(3)\neq\frac{m}{n}.$$ Composing in this way the proofs showing that logarithms and division map bounded away pairs to bounded away pairs, and that $\lvert 2^m-3^n\rvert>0$ for all relevant pairs, this outlines a perfectly valid algorithm that takes as input rational $p$ and returns, say, a witness natural $k>0$ such that $\lvert\log_2(3)-p\rvert>\frac{1}{k}$.

I find this definition to be overall more in spirit with numerical analysis for instance, as it eschews a lot of possible double negations* later on, and it provides valuable information that is feasibly probeable and reflects what irrationality intuitively is—in particular, this makes the set of irrationals a $G_\delta$, as it was classically, while the rationals are still an $F_\sigma$.

(*Though, this introduces a lot more nuance in the logical relationship between rationality and irrationality. Some may see this as bloat, while others may see it as just the required numerical distinction.)