jd2718 asked in his blog if anyone knew a direct proof of the irrationality of 
. 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 
can be something like:
Or, alternatively, we can also use a proof of the following shape:
Irrational numbers
An irrational number is a real number that can’t be expressed as a simple fraction. Therefore, the number is irrational because for all integers m and n, with n non-negative, we have that:
A direct proof for the irrationality of
Now that we have clarified the concepts above, we prove that is irrational. For all integers m and n, with n non-negative, we have:
Note that, unlike traditional proofs, we don’t assume that m and n are co-prime, nor that is a rational. We essentially derive the boolean value of the expression 
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).
14 Comments
Slick. Thank you.
No problem
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 $
nope
Hmmm. I’m using a plugin called wp-latexrenderer. I have to investigate whether it works for comments.
Did you keep that sqrt on a little longer than necessary, or am I completely misunderstanding this proof?
Dear Erik,
of course I have. It was a typo, I’m sorry. It is corrected now. Thanks a lot!
Thanks, I thought I was going mad.
Hi.
delicious!truly elegant!
isn’t the first equivalence actually an implication? m/n could be minus sqrt(2)…
tks
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!
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?
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
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
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
Post a Comment