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

Related Posts:

17 thoughts on “Calculational proofs are usually direct

  1. 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 $

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

  3. 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?

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

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

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

    • 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

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>