Calculational proofs are usually direct : Joao Ferreira

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:

$\setms{0.1em}\begin{mpdisplay}{0.1em}{8.5mm}{2mm}{3}$\sqrt{2}$ is irrational\push\-\\$=$ \> \>$\{$ \>\+\+\+justification\-\-$~~~ \}$\pop\\$\mathit{true\/}~~.$\end{mpdisplay}$

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

$\begin{mpdisplay}{0.1em}{8.5mm}{2mm}{3}$\sqrt{2}$ is irrational\push\-\\$\Leftarrow$ \> \>$\{$ \>\+\+\+justification\-\-$~~~ \}$\pop\\$\mathit{true\/}~~.$\end{mpdisplay}$

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:

$\begin{displaymath}\sqrt{2}\ms{2}~~{\neq}~~\ms{2}{\displaystyle\frac{m}{n}}\mbox{\ \ \ .}\end{displaymath}$

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:

$\begin{mpdisplay}{0.1em}{8.5mm}{2mm}{3}$\sqrt{2}\ms{1}~{\neq}~\ms{1}{\displaystyle\frac{m}{n}}$\push\-\\$=$ \> \>$\{$ \>\+\+\+Use arithmetic to eliminate the square root operator.\-\-$~~~ \}$\pop\\$n^{2}{\times}2\ms{1}~{\neq}~\ms{1}m^{2}$\push\-\\$\Leftarrow$ \> \>$\{$ \>\+\+\+Two values are different if applying the same function to them\\ yields different values.\-\-$~~~ \}$\pop\\$\mathit{exp\/}{.}(n^{2}{\times}2)\ms{1}~{\neq}~\ms{1}\mathit{exp\/}{.}m^{2}$\push\-\\$=$ \> \>$\{$ \>\+\+\+Now we choose the function $exp.$\\Let $\mathit{exp\/}{.}k$ be the number that $2$ divides $k.$\\The function $\mathit{exp\/}$ has two important properties:\\~~~$\mathit{exp\/}{.}2\ms{1}{=}\ms{1}1$ and\\~~~$\mathit{exp\/}{.}(k{\times}l)\ms{2}{=}\ms{2}\mathit{exp\/}{.}k\ms{2}{+}\ms{2}\mathit{exp\/}{.}l$ .\\We apply these properties to simplify the left and right sides.\-\-$~~~ \}$\pop\\$1\ms{2}{+}\ms{2}2\ms{1}{\times}\ms{1}\mathit{exp\/}{.}n\ms{3}~{\neq}~\ms{3}2\ms{1}{\times}\ms{1}\mathit{exp\/}{.}m$\push\-\\ $=$ \> \>$\{$ \>\+\+\+The left side is an odd number and the right side is an even\\ number. Odd numbers and even numbers are different.\-\-$~~~ \}$\pop\\$\mathit{true\/}~~.$\end{mpdisplay}$

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

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

10 Comments

Jonathan wrote:

Slick. Thank you.

Monday, February 11, 2008 at 12:18 am | Permalink
jff wrote:

No problem

Monday, February 11, 2008 at 12:25 am | Permalink
Jonathan wrote:

by the way, comments on wordpress support the wordpress subset of LaTeX. But since there’s no preview, if you goof, you have to ask the host to nicely fix things up.

Let’s try:

$latex e^{i\pi}+1=0 $

Monday, February 11, 2008 at 2:21 am | Permalink
Jonathan wrote:

nope

Monday, February 11, 2008 at 2:23 am | Permalink
jff wrote:

Hmmm. I’m using a plugin called wp-latexrenderer. I have to investigate whether it works for comments.

Monday, February 11, 2008 at 9:47 am | Permalink
Erik wrote:

Did you keep that sqrt on a little longer than necessary, or am I completely misunderstanding this proof?

Wednesday, February 13, 2008 at 7:26 pm | Permalink
jff wrote:

Dear Erik,

of course I have. It was a typo, I’m sorry. It is corrected now. Thanks a lot!

Wednesday, February 13, 2008 at 8:37 pm | Permalink
Erik wrote:

Thanks, I thought I was going mad.

Wednesday, February 13, 2008 at 9:14 pm | Permalink
mike wrote:

Hi.

delicious!truly elegant!

isn’t the first equivalence actually an implication? m/n could be minus sqrt(2)…

tks

Monday, September 15, 2008 at 10:05 pm | Permalink
jff wrote:

Mike,

The so-called Leibniz rule (also called ’substitution of equals by equals’) states that, for all a, b, and function f:

a = b => f.a = f.b .

Hence, you can see the first step as a mutual implication where, in one direction, function f is taking the square root, and in the other direction, function f corresponds to squaring.

Thanks for your comment!

Thursday, October 16, 2008 at 9:34 pm | Permalink

João Ferreira