Understanding $\forall p \, q .\, \sqrt{2} \neq p/q$ constructively

Question

"By contradiction" or "of negation" is an old chestnut of constructive dispute.

But taking apartness as primitive instead of equality yields a definition of irrationality without negation, making rationality a derived notion.

So can we give a neat constructive proof of $\forall p q.\sqrt2 \neq p/q$ by induction on $p,q:\mathbb N$ with $q\neq 0$?

To do this properly would require first re-formulating the axioms of arithmetic with apartness instead of equality.

There is no doubt that this is true, although it is perhaps less appreciated than it should be that the standard result from Euclid or before uses induction.

(cf David Fowler, Could the Greeks have used Mathematical Induction? Did they use it?, Physis 31 (1994) 252--265.)

Then if the standard proof is classical, I believe that some easy proof theory make it constructive.

But the reason for asking the question is to see whether some logical or constructive insight can be gained from re-thinking the proof using $\neq$, $\forall$ and $\lor$ instead of $=$, $\exists$ and $\land$.

Maybe (probably?) not, but it's worth a try.

Answer 1

Every positive rational number has a finite continued fraction expansion. This one can prove by induction. On the other hand, $\sqrt{2}$ has an infinite continued fraction expansion.

Added 1. Another way of telling the proof is as follows. If $\sqrt 2=p/q$, then also $\sqrt 2=(2q-p)/(p-q)$. Hence one can induct on the sum $p+q$ to show that $\sqrt 2\neq p/q$. By the way, this was probably the original proof as one can tell it in purely geometric language, starting from the side and diagonal of a square. The point is that the Euclidean algorithm does not terminate for the side and diagonal of a square, hence they are not proportional. All this was well-known to ancient Greek mathematicians.

Added 2. Yet another variant of the proof is based on the identity $$|p^2-2q^2|=|(2q-p)^2-2(p-q)^2|.$$ Using this identity, it follows by induction that $|p^2-2q^2|\geq 1$. In turn, this lower bound implies that $$|\sqrt{2} - p/q|\geq c/q^2\qquad\text{with}\qquad c=2/(3+2\sqrt{2}),$$ and this is sharp for $p/q=3/2$. Indeed, we have that $$|\sqrt{2} - p/q|=\frac{|p^2-2q^2|}{q^2|\sqrt{2} + p/q|}\geq\frac{1}{q^2|\sqrt{2} + p/q|},$$ hence the claim is clear when $p/q\leq 3/2$. For $p/q>3/2$ and $q\geq 2$ we can argue as follows: $$|\sqrt{2} - p/q|>3/2-\sqrt{2}=c/4\geq c/q^2.$$ Finally, for $p/q>3/2$ and $q=1$ we have that $$|\sqrt{2} - p/q|\geq 2-\sqrt{2}>c=c/q^2.$$ For a more general result, see Theorem 2 in this summary.

Answer 2

Let $\nu_2(x)$ be the $2$-adic order of rational number $x$.

[EDIT] Note that this is completely elementary. It doesn't even require unique factorization. Thus for a nonzero integer $k$, $\nu_2(k) = m$ where $k$ is divisible by $2^m$ but not by $2^{m+1}$. Or if you prefer, it is the number of trailing $0$'s when $|k|$ is written in base $2$. For nonzero integers $p$ and $q$, $\nu_2(p/q) = \nu_2(p) - \nu_2(q)$. It is easy to show that this is well-defined, i.e. if $p/q = r/s$, then $ps = rq$ and $$\nu_2(ps) = \nu_2(p) + \nu_2(s) = \nu_2(rq) = \nu_2(r) + \nu_2(q)$$ so $\nu_2(p) - \nu_2(q) = \nu_2(r) - \nu_2(s)$.

Then $\nu_2((p/q)^2) = 2 \nu_2(p/q)$ is an even integer, but $\nu_2(2) = 1$ is odd, therefore $(p/q)^2 \ne 2$.

Answer 3

I asked this question because I was wondering whether considering a positive definition of irrationality could yield any constructive enlightenment, rather than re-packaging the traditional proof of irrationality of $\sqrt 2$.

@Gro-Tsen, @EmilJeřábek and @GHfromMO have convinced me (contrary to my initial thoughts) that continued fractions do this.

There is a classical result that the irrationals are homeomorphic to Baire space. The positive definition, apartness-from-rationals, makes this constructive.

Classically, there is a floor function ${\mathbb R}\to{\mathbb Z}$, given by $$\lfloor x\rfloor\equiv\max\{n\in{\mathbb Z}:n\leq x\}.$$ However, this is not continuous (since $\mathbb R$ is connected) and so not constructive (since $n\leq x$ is not decidable).

The standard constructive solution to this difficulty is the express the Archimedean axiom as $$ \exists n\in{\mathbb Z}.\quad n-1 < x < n+1, $$ so $x$ might miss the "exact" floor by 1.

However, this problem goes away if $x$ is apart-from-rational, which we can write explicitly as $$ \forall q\in{\mathbb Q}.\exists m\in{\mathbb N}^+.\quad (x < q-\frac{1}{m}) \quad\lor\quad (q+\frac{1}{m} < x), $$ in which the decidable disjunction corrects the ambiguity in the constructive Archimedean axiom.

Not only does this give a constructive definition of $\lfloor x\rfloor$, but also of the reciprocal $1/(x-{\lfloor x\rfloor})$, for which $m$ is an upper bound (cf the Archimedean axiom again). It's these points that convince me that continued fractions answer my philosophical question.

Writing $A\subset{\mathbb R}$ for the subspace of apart-from-rational numbers, we then have a homeomorphism $$ A\ \cong\ {\mathbb Z}\times A, $$ and therefore a continuous map $A\to{\mathbb Z}^{\mathbb N}$. In fact the sequence consists of positive integers, apart from the first.

(For categorists, $A$ is a coalgebra for the functor ${\mathbb N}\times({-})$ and Baire space is the final coalgebra.)

Conversely, any continued fraction gives a pair of recurrence relations for the fraction in standard form, which is automatically in lowest terms. Therefore the denominators increase without bound and (I think) it follows that the limit is apart-from-rational.

Moreover, this defines a continuous map from Baire space ${\mathbb Z}\times{\mathbb N}^{\mathbb N}\to A\subset{\mathbb R}$ that is inverse to the one before.