I have little knowledge of formal logic or set theory. Nevertheless it occurred to me to wonder whether one can give an explicit construction of a real number, such that it does not follow from the usual ZF axioms of set theory whether or not it is rational.
My question is partly motivated by the supposed "proof" of the existence of irrational $a,b$ such that $a^b$ is rational. It says: if $x=\sqrt2 ^{\sqrt2}$ is irrational, then $x^{\sqrt2}$ is rational. My first reaction is not the standard intuitionist objection, but that it is very hard to prove that ZF can show whether $x$ is rational. (The now known theorem, that $x$ is irrational, is beside the point.) This leads me to ask the same question about $e+\pi$, and so on.
The standard way to do this is to define $x$ to be $0$ if the axiom of choice holds, and $\sqrt2$ if the axiom of choice fails.
In set theoretic language this is more complicated, as it involves the exact way that we define the real numbers, and how we interpret the language of fields into set theory. But you can take these as black boxes, and end up with the definition above. You can replace $\sqrt2$ for any other irrational number that you'd like to have.
You can also use the above trick to get some sort of odd scenarios. For example, if you replace "the axiom of choice holds" with "ZF is consistent" (which is itself a number theoretic statement), then you get a real number that is provably rational if and only if ZF is inconsistent to begin with.
It is important to point, however, that these examples rely on the law of excluded middle, and they are not constructively valid. If you are interested in a constructive system, then you'd have to specify more accurately what system you're interested in.
(But I imagine that one can use some intuitionistically valid incompleteness argument to reproduce the above $x$. After all, we only want something which is provably a real, but not provably a rational number.)