√2 is Irrational

First reduce the sign: if a rational $r$ satisfies $r^2 = 2$, then $|r|$ is rational, $|r|^2 = r^2 = 2$, and $r \ne 0$, so $|r|$ is a positive rational solution. Hence it suffices to rule out a positive solution.

Suppose a positive rational $p/q$ with $\left(\frac{p}{q}\right)^2 = 2$ exists. By problem 2 below, we may take $p/q$ in lowest terms, i.e. $\gcd(p, q) = 1$.

Clearing denominators gives $p^2 = 2q^2$, so $p^2$ is even. If $p$ were odd then $p^2$ would be odd (odd × odd = odd), so $p$ must be even: $p = 2k$ for a positive integer $k$.

Substituting gives $4k^2 = 2q^2$, i.e. $q^2 = 2k^2$, so $q^2$ is even too — and the same argument makes $q$ even. But $p$ and $q$ both even means $\gcd(p, q) \ge 2$, contradicting the lowest-terms assumption.

Hence no rational squares to $2$. However close a square gets to $2$ — like $\frac{7}{5}$ or $\frac{17}{12}$ (problem 3) — no fraction lands exactly on $2$: the rational line has a hole where $\sqrt{2}$ should be.

Fix a positive rational $r$. Let $S = \{n \in \mathbb{N} : r = m/n \text{ for some } m \in \mathbb{N}\}$; since $r = a/b$ for positive integers $a, b$, we have $b \in S$ — so $S$ is a nonempty subset of $\mathbb{N}$.

(Here $\mathbb{N} = \{1, 2, 3, \dots\}$.)

By the well-ordering principle, $S$ has a least element $q_0$. Pick $p_0 \in \mathbb{N}$ with $r = p_0/q_0$.

We now show $\gcd(p_0, q_0) = 1$.

If $d = \gcd(p_0, q_0) > 1$, then $r = \frac{p_0/d}{q_0/d}$ with $q_0/d < q_0$, so $q_0/d \in S$ — contradicting the minimality of $q_0$. Hence $d = 1$, and $r = p_0/q_0$ is in lowest terms.

This justifies the "we may take lowest terms" step in problem 1: if some rational squared to $2$, we could look at one with the smallest denominator — and it is exactly that minimal-denominator fraction that falls into the even/even contradiction.

Compute directly: $\left(\frac{7}{5}\right)^2 = \frac{49}{25} = 1.96 < 2$ and $\left(\frac{17}{12}\right)^2 = \frac{289}{144} = 2.0069\ldots > 2$ (verified exactly by integer comparison: $49 < 50 = 2 \times 25$ gives $\frac{49}{25} < 2$, and $289 > 288 = 2 \times 144$ gives $\frac{289}{144} > 2$).

The fractions differ by $\frac{17}{12} - \frac{7}{5} = \frac{85 - 84}{60} = \frac{1}{60} \approx 0.0167 < 0.06$. Their squares differ by $\frac{289}{144} - \frac{49}{25} = \frac{7225 - 7056}{3600} = \frac{169}{3600} < 0.05$ — both squares sit inside an interval of width under $0.05$ straddling $2$.

General step (the numeric instance above is only an illustration): the continued-fraction convergents $p_k/q_k$ of $\sqrt{2}$ ($1/1, 3/2, 7/5, 17/12, \dots$, with $q_k$ increasing and unbounded) satisfy the determinant identity $|p_k q_{k-1} - p_{k-1} q_k| = 1$, hence $\left|\frac{p_k}{q_k} - \frac{p_{k-1}}{q_{k-1}}\right| = \frac{1}{q_k q_{k-1}}$, and since $\sqrt{2}$ lies between consecutive convergents, $\left|\sqrt{2} - \frac{p_k}{q_k}\right| \le \frac{1}{q_k q_{k+1}} \le \frac{1}{q_k^2} \to 0$. So given any $\varepsilon > 0$, choosing $k$ with $\frac{1}{q_k^2} < \varepsilon$ gives $\left|\sqrt{2} - \frac{p_k}{q_k}\right| < \varepsilon$ — rationals get arbitrarily close ($\forall \varepsilon > 0$) to $\sqrt{2}$.

By problem 1, no rational in this interval squares to exactly $2$. Yet rationals squeezing $2$ from both sides, like $\frac{7}{5}$ and $\frac{17}{12}$, are easy to find (in the model the shortest distance shrinks $0.0142 \to 0.00245 \to \cdots$ as $N$ grows), and together with the general estimate above this shows the rationals get as close as one likes to the $\sqrt{2}$ slot, but never touch it.

The number filling this hole is the $\sqrt{2}$ whose existence the least-upper-bound axiom guarantees (the n-th root scene).