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.

  • 1
    $\begingroup$ 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. $\endgroup$ – Daniel Schepler Dec 21 '18 at 18:45
  • $\begingroup$ 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? $\endgroup$ – Ted Hopp Dec 21 '18 at 20:29
  • 1
    $\begingroup$ @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. $\endgroup$ – Henno Brandsma Dec 21 '18 at 22:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.