# 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}}$.

Note: I learnt the contrapositive of this proof from Roland Backhouse (page 38, Program Construction — Calculating Implementations from Specifications).

# In Defense Of Computer Science

So why study computer science? The job prospects at the end are usually pretty good – because, if nothing else, you can become a pretty good software developer fairly quickly – but they are unknown. My argument is that the study of computer science is enough of an incentive enough to make it worthwhile.

# The programmers of tomorrow

A recent article written by Dr. Robert B.K. Dewar and Dr. Edmond Schonberg (both from AdaCore Inc.) is generating some discussion on the state of Computer Science (CS) education in the United States. In “Computer Science Education: Where Are the Software Engineers of Tomorrow?“, Dewar and Schonberg claim that U.S. universities are training unqualified and easily replaceable programmers.

“It is our view that Computer Science (CS) education is neglecting basic skills, in particular in the areas of programming and formal methods. We consider that the general adoption of Java as a first programming language is in part responsible for this decline. We examine briefly the set of programming skills that should be part of every software professional’s repertoire.”

The comment about Java’s adoption annoyed some Java aficionados, but in a recent interview, Robert Dewar adds that the problem goes far beyond the choice of Java as the first programming language. The real problem is that CS programs are being dumbed down, so that they become more accessible and popular. In result, they “are not rigorous enough and don’t promote in-depth thinking and problem solving”.

“A lot of it is, ‘Let’s make this all more fun.’ You know, ‘Math is not fun, let’s reduce math requirements. Algorithms are not fun, let’s get rid of them. Ewww – graphic libraries, they’re fun. Let’s have people mess with libraries. And [forget] all this business about ‘command line’ – we’ll have people use nice visual interfaces where they can point and click and do fancy graphic stuff and have fun.”

Although the paper is concerned with the American reality, I believe we have the same problem in Europe — at least, and as far as I know, in the UK and in Portugal. However, in my opinion, the problem starts before university. The maths’s programs in secondary schools are also being simplified (or dumbed down, if you prefer) and many important concepts, like logic and proofs, are being ignored.

In result, first-year students usually have a poor background on maths and problem solving. In fact, most of them have never seen a proof and don’t even understand the importance of mathematical reasoning. With poor reasoning abilities, they become intellectually less curious, accepting things as they are presented, and they have tremendous difficulties creating new algorithms, or convincing someone that their own algorithms are correct.

Moreover, once they are in the university, one of two things happens:

1. they are not taught explicitly how to solve problems or how to derive algorithms from their formal specifications (this is the most common case);
2. or they are taught the above skills but their poor background doesn’t allow them to fully appreciate these subjects.