# Calculational proofs are usually direct

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

## 17 thoughts on “Calculational proofs are usually direct”

1. Slick. Thank you.

2. No problem

3. 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^{ipi}+1=0$

4. nope

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

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

7. Dear Erik,

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

8. Hi.

delicious!truly elegant!

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

tks

9. 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!

10. I am just a layperson who’s interested in logic. Your proof looks very intuitive and direct, and I have to admit it’s more elegant.

However, I have a small question from my ignorance on your notation.

In-between the statements, there are lines that explain the transformation. All of them start with an equal sign except the second one, which is left-arrow. What does that mean and why is this the only one?

11. Jane,

Each step in the proof format I use has the form:

A
R { hint }
B .

This means that A is related with B by relation R, and the reason is shown in the hint. If I instantiate R with equality, I get:

A
= { hint }
B ,

which means that A=B.

Similarly, if I use the arrow, as in

A
< = {hint}
B ,

then it means that B implies A.

***

In this particular example, I am using the contrapositive of the so-called Leibniz rule:

f(a) =/= f(b) => a =/= b .

In words, if the value of f(a) is different from f(b), then a must be different from b.

I hope this helps,
Joao

12. And why are two values different if applying the same function to them yields different values?
Because if they were same, function would return same values

13. Dear XSLX,

that’s the contrapositive of Leibniz’s rule. Leibniz rule states that, for all a, b, and function f:
a=b => f.a = f.b

The contrapositive is obtained by negating both sides and changing the direction of the implication:

a=/=b <= f.a =/= f.b

Thanks for your comment,
Joao

14. Argh, I don’t completely understand.
Why must exp(n) and exp(m) be integers?
Why cant exp(m)=exp(n)+0.5?

Thanks. =)

• Hi Simon,

By definition, exp(m) is the number of times that 2 divides m; this means that exp(m) is always a natural number. For example, exp(4)=2, exp(5)=0, exp(6)=1, exp(8)=3.

Hence, you can never find m and n, such that exp(m)=exp(n)+0.5, because the left-hand side is a natural number and the right-hand side is not.

I hope this helps,
Joao

15. I’m a little late to the game here, but I think it’s very interested that both of us had early forays into the calculational style, inspired by Roland Backhouse’s calculation in Program Construction.

My effort at the same thing was recorded in JAW2, which can be read here: http://mathmeth.com/jaw/main/jaw0xx/jaw2.pdf .

Cheers!