Solution (source code)

= Solution

Use the intended <first-order structure> of real arithmetic, with `Int` selecting the <integers>; $z$ is the parameter in $\phi_z$. A suitable <first-order formula> is
$$
\boxed{\phi_z=\exists r\left(r*r=(1+1)*z\ \land\ \neg\exists p\,\exists q\left(\operatorname{Int}(p)\land\operatorname{Int}(q)\land\neg(q=0)\land q*r=p\right)\right).}
$$
The first condition requires a real <square root> of $2z$. The second excludes every representation as a <rational number> $p/q$ with a nonzero <integer> denominator. This uses only the listed function and constant symbols, the `Int` predicate and <logical equality>; in particular, $2$ is written $1+1$ and there is no extra division symbol. A <square root> exists exactly when $z\ge0$, and either sign of a root is a <rational number> exactly when the other sign is a <rational number>, so the absence of a positivity condition on $r$ does not affect the claim about the principal <square root>. At $z=0$ the formula is false; for $z<0$ there is no real witness. The meanings of $+$ and $*$ as real arithmetic, not just the meaning of `Int`, are part of this interpretation.