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).