jd2718 asked in his blog if anyone knew a direct proof of the irrationality of $\sqrt{2}$. In this post I present a proof that, even if some don’t consider it direct, is a nice example of the effectiveness of calculational proof. But first, there are two concepts that need to be clarified: direct proof and irrational number.

Direct proofs

The concept of direct proof can vary slightly from person to person. For instance, Wikipedia defines it as:

In mathematics and logic, a direct proof is a way of showing the truth or falsehood of a given statement by a straightforward combination of established facts, usually existing lemmas and theorems, without making any further assumptions.

Alternatively, in Larry W. Cusick’s website we can read:

A direct poof [sic] should be thought of as a flow of implications beginning with “P” and ending with “Q”.

P -> … -> Q

Most proofs are (and should be) direct proofs. Always try direct proof first, unless you have a good reason not to.

I consider the wording ‘without making any further assumptions‘ in the first definition ambiguous and I don’t understand why the second definition only applies to implications. But anyway, with these definitions in mind, a direct proof for the irrationality of $\sqrt{2}$ can be something like:

\[
\beginproof
\pexp{\text{$\sqrt{2}$ is irrational}}
\hint{=}{justification}
\pexp{true~~.}
\endproof
\]

Or, alternatively, we can also use a proof of the following shape:

\[
\beginproof
\pexp{\text{$\sqrt{2}$ is irrational}}
\hint{\Leftarrow}{justification}
\pexp{true~~.}
\endproof
\]

Irrational numbers

An irrational number is a real number that can’t be expressed as a simple fraction. Therefore, the number $\sqrt{2}$ is irrational because for all integers $m$ and $n$, with $n$ non-negative, we have that:

\[
\sqrt{2} \neq \frac{m}{n} ~~.
\]

A direct proof for the irrationality of $\sqrt{2}$

Now that we have clarified the concepts above, we prove that $\sqrt{2}$ is irrational. For all integers $m$ and $n$, with $n$ non-negative, we have:

\[
\beginproof
\pexp{\sqrt{2} \neq \frac{m}{n}}
\hint{=}{Use arithmetic to eliminate the square root operator.}
\pexp{{n^2{\times}2}\neq{m^2}}
\hintf{\Leftarrow}{Two values are different if applying the same function to them}
\hintl{yields different values.}
\pexp{\fapp{exp}{(n^2{\times}2)} \neq \fapp{exp}{m^2}}
\hintf{=}{Now we choose the function $exp$.}
\hintm{Let $\fapp{exp}{k}$ be the number of times that $2$ divides $k$.}
\hintm{The function $exp$ has two important properties:}
\hintm{$~~~\fapp{exp}{2}=1$ and}
\hintm{$~~~\fapp{exp}{k{\times}l} = \fapp{exp}{k} + \fapp{exp}{l}$}
\hintl{We apply these properties to simplify the left and right sides.}
\pexp{1{\,+\,}2{\times}\fapp{exp}{n} ~\neq~ 2{\times}\fapp{exp}{m}}
\hintf{=}{The left side is an odd number and the right side is an even}
\hintl{number. Odd numbers and even numbers are different.}
\pexp{true ~~.}
\endproof
\]

Note that, unlike traditional proofs, we don’t assume that $m$ and $n$ are co-prime, nor that $\sqrt{2}$ is a rational number. We simply derive the boolean value of the expression $\sqrt{2}~{\neq}~{\frac{m}{n}}$.

If you have any suggestions or corrections, please leave a comment. I’d be more than happy to hear from you.

Note: I learnt the contrapositive of this proof from Roland Backhouse (page 38, Program Construction — Calculating Implementations from Specifications).

Related Posts:

• Probabilities in Proofreading
• An improved proof of the handshaking lemma
• Principles and Applications of Algorithmic Problem Solving
• A Calculational Proof of the Handshaking Lemma
• The programmers of tomorrow