# Prove constructively that $\log_2 3$ is irrational.

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?

$$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.
• In fact, it's not at all unusual to define $\lnot \phi$ as being "synactic sugar" for $\phi \rightarrow \bot$; and in that case, a proof of this form would be a special case of the standard ${\rightarrow} I$ rule. – Daniel Schepler Dec 21 '18 at 18:45
• So let's see if I understand this. By definition, "$\log_2 3$ is irrational" is by definition shorthand for "$\log_2 3$ is not rational" and we're proving a negative. Furthermore, in constructivism, any theorem of the form "$\lnot A$" can be validly proven by showing that $A\vdash\bot$? So even though the structure of the proof looks like we're proving $\lnot \lnot A\vdash\bot$, that's not what's going on? – Ted Hopp Dec 21 '18 at 20:29
• @TedHopp indeed. A negative is proven by contradiction. How else could one prove a negative. But $\lnot\lnot\phi$ does not show $\phi$. The linked proof here that there are $a,b$ irrational such that $a^b$ is rational shows this by assuming 'tertium non datur' which is not allowed constructively. – Henno Brandsma Dec 21 '18 at 22:41