Skip to content

Calculational proofs are usually direct

jd2718 asked in his blog if anyone knew a direct proof of the irrationality of LaTeX Formula  . 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 LaTeX Formula can be something like:

LaTeX Formula

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

LaTeX Formula

Irrational numbers

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

LaTeX Formula

A direct proof for the irrationality of LaTeX Formula

Now that we have clarified the concepts above, we prove that LaTeX Formula is irrational. For all integers m and n, with n non-negative, we have:

LaTeX Formula

Note that, unlike traditional proofs, we don’t assume that m and n are co-prime, nor that LaTeX Formula is a rational. We essentially derive the boolean value of the expression LaTeX Formula

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

12 Comments

  1. Jonathan wrote:

    Slick. Thank you.

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

    No problem :-)

    Monday, February 11, 2008 at 12:25 am | Permalink
  3. 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
  4. Jonathan wrote:

    nope

    Monday, February 11, 2008 at 2:23 am | Permalink
  5. 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
  6. 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
  7. 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
  8. Erik wrote:

    Thanks, I thought I was going mad. :)

    Wednesday, February 13, 2008 at 9:14 pm | Permalink
  9. 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
  10. 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
  11. Jane Forrester wrote:

    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?

    Tuesday, January 13, 2009 at 6:19 pm | Permalink
  12. jff wrote:

    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

    Wednesday, January 14, 2009 at 10:39 am | Permalink

Post a Comment

Your email is never published nor shared. Required fields are marked *
*
*