(I don't have a formal background in logic, but I am trying to learn.)

The classical proof works like this:

It is either the case that $\sqrt{2}^\sqrt{2} \in \mathbb{Q}$ or $\sqrt{2}^\sqrt{2} \notin \mathbb{Q}$ If it is the former case, we are done. Otherwise, consider $\left(\sqrt{2}^\sqrt{2}\right)^\sqrt{2} = 2 \in \mathbb{Q}$

The crucial component of this proof is the law of the excluded middle, in particular $\sqrt{2}^\sqrt{2} \in \mathbb{Q}$ or $\sqrt{2}^\sqrt{2} \notin \mathbb{Q}$.

I read (from Software Foundations) that in intutionistic systems like Coq, we could possible derive this by adding the axiom manually.

Definition excluded_middle := forall P : Prop,
  P \/ ~ P.

Is there a known proof that does not require this axiom? Is it the case that many important theorems in real analysis cannot be proven in intuitionistic logic?

  • $\begingroup$ You got the order of operations wrong on the repeated exponential; I fixed it. $\endgroup$
    – user14972
    May 15, 2017 at 3:18

1 Answer 1


The typical proof that $\log_2(3)$ is irrational should go through intuitionistically: if $\log_2(3)=\frac pq$, then $2^{p/q}=3$, so $2^p=3^q$, which is a contradiction since the LHS is even and the RHS is odd. Likewise, most of the classical proofs that $\sqrt{2}$ is irrational should be intuitionistically valid. But then we have $(\sqrt{2})^{2\log_2{3}}=3$, which proves that there are numbers $x$ and $y$, neither rational, with $x^y$ rational.


You must log in to answer this question.

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