3
$\begingroup$

(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?

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

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.

$\endgroup$

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.