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?
Best Answer
$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.