I was reading the wikipedia page for "constructive proof" and I have a question about something one of the authors says in the section "Examples" where two proofs are juxtaposed for the assertion that there exists irrational $x,y$ such that $x^y$ is rational.
I think we all know how the classic non-constructive argument goes, so I wont repeat it. It is also given on the wiki link provided above. They mention that the reason this argument fails to be constructive is because it relies on the statement "Either $q$ is rational or it is irrational".
However, for the constructive proof they exhibit, they assert that $a = \text{log}_{2}(9)$ is irrational because, if it were rational we would get a contradiction.
Can someone explain to me how the form of the argument goes in the constructive case to validate the irrationality of $a$, and why it doesn't fail to be constructive for the same reason as the non-constructive argument? It seems it is also starting with (and relying on) the assumption that $a$ is either rational or irrational, and then shows that [$a$ is rational ] $\rightarrow \bot$, then deduces from this that $a$ is irrational.
Is there a subtle difference between the two arguments? Making subtle use of a valid elimination rule in constructive logic?
"Irrational" means "not rational", and essentially the only way to prove a given number is not rational is to assume it is and then derive a contradiction. This is valid constructively, though it is easy to confuse with the constructively invalid proof by contradiction where you assume a statement is false, derive a contradiction and then conclude that the statement is true.
(The valid version is to assume something is true, derive a contradiction and infer that it must in fact be false. These only seem like the same thing cause we are used to a double negative being a positive in classical reasoning.)
Notice in this constructively valid case, we have not actually made an assumption at the outset that either $a$ is rational or it isn't. We completely leave open the possibility that we cannot produce a $p,q$ such that $a=p/q,$ nor can we derive a contradiction from the supposition that such a $p,q$ exist. We just prove the latter. All we have used is the fact that "not A" means exactly that "A yields a contradiction."
On the other hand, in the first case we do invalidly assume that $q$ is either rational or not, as evidenced by our binary case analysis.