\documentclass[12pt]{article}
\usepackage{amsfonts}

\voffset=-3.0cm
\hoffset=-2.6cm
\textwidth=17.5cm
\textheight=24cm

\renewcommand{\not}{\neg}
\newcommand{\nov}[1]{{\overline #1}} % negation by overbar
\renewcommand{\and}{\wedge}
\renewcommand{\or}{\vee}
\newcommand{\impl}{\Rightarrow}
\newcommand{\lequiv}{\Leftrightarrow} %equivalence as logical connective
\newcommand{\all}{\forall}
\newcommand{\exi}{\exists}
\newcommand{\elc}{\models}  % semantic logical consequence
\newcommand{\ylc}{\vdash}  % syntactic logical consequence
%\equiv is already defined for === semantic equivalence
\newcommand{\union}{\cup}
\newcommand{\intersect}{\cap}
%\newcommand{\true}{{\bf T}}
%\newcommand{\false}{{\bf F}}

% these use amsfonts
\newcommand{\true}{{\mathbb{T}}}
\newcommand{\false}{{\mathbb{F}}}

\pagestyle{empty}

\begin{document}

{\bf Proof Example: The Irrationality of $\sqrt{2}$
}

\bigskip

\noindent
During the lecture a student asked for an example of natural style
proof in which one uses the inference rule:

$$
\frac
{\Phi \ylc \Psi, \varphi}
{\Phi, \neg \varphi \ylc \Psi}
\ (\neg\ylc).
$$

Proofs in natural style have only one goal, thus this rule may be used
when the set $\Psi$ is empty, that is, when we are trying to find a contradiction:
$$
\frac
{\Phi \ylc \varphi}
{\Phi, \neg \varphi \ylc \false}
\ (\neg\ylc).
$$

Intuitively, this can be expressed as:
``Since we are trying to find a contradiction, and $\neg \varphi$ is assumed,
then we try to prove $\varphi$''.

The proof below uses this rule.

\smallskip

{\bf Theorem}: $\sqrt{2}$ is not a rational number.

{\bf Proof:} By contradiction: we assume that $\sqrt{2}$ is a rational,
and we try to derive a contradiction.

By the definition of rational numbers, there exist $n$
and $m,$ such that $\sqrt{2} = n/m$ and $n, m$ are
coprime.

(What is ment here by {\em coprime}?
Two natural numbers are coprime iff there does not exist a number
which divides both of them.

What is ment here by {\em divides}?
A natural number $d > 1$ divides a natural number $n$ iff
there exists a natural $k$ such that $n = d * k$.
Note that a divisor is automatically different from 0 and 1.

Intuitively, this definition of rational numbers takes into
account their unique representation $x/y$ in which the fraction is already
simplified by the greatest common divisor -- GCD -- of the nominator and the denominator.
In more exact terms, if one would define the rational numbers as a number
which can be expressed as $x/y$, then one can prove a lemmata stating that
each rational number can be expressed as $x'/y'$, where $x', y'$ are coprime,
because otherwise one can take
$x' = x/{\rm GCD}(x, y)$ and similarly for $y'$.)

Therefore, we now have the assumption:\\
\centerline{{\bf not} (there exists a $d$ which divides $n$ and $m$).}

{\em Now we apply the inference rule mentioned above:}

We prove:\\
\centerline{ there exists a $d$ which divides $n$ and $m$.} 

We take as witness for $d$ the number 2 and we
prove: 2 divides $n$ and $m$.

By definition of $\sqrt{x}$ (that is: the positive number $y$ such that
 $y^2 = x$), we obtain $n^2/m^2 = 2$ and from this $n^2 = 2\ m^2.$

Thus 2 divides $n^2,$ from here 2 divides $n$ (because 2 is prime), therefore
there exists a $k$ such that $n = 2\ k.$

We replace this into the previous equality and obtain $4\ k^2 = 2\ m^2,$
thus $2\ k^2 = m^2,$ hence 2 divides $m^2$ and finally 2 divides $m$.

\smallskip

{\bf Remark 1.}
This theorem was first proved by the ancient mathematician Hippasus around
500 BC in a similar manner. A consequence of this theorem is the existence
of irrational numbers (that is, numbers which can not be expressed as fractions).
At the respective time this was a revolutionary discovery.
Hippasus was a member of the mathematical school of Pythagoras, which was
probably the most advanced ``mathematical society'' of the time,
and which developed many interesting results about numbers and geometry
(in particular the famous theorem about the rectangular triangle).
They believed that all numbers which express lengths of segments
must ``exist'', and they also believed that all numbers can be expressed
as fractions.
However, the lenght of the hypothenusis (in German: {\em Hypothenuse})
of the square triangle with kathetes (in German: {\em Kathete}) of length
1 is equal to $\sqrt{2}$, thus the latter must ``exist'', although it cannot
be expressed as a fraction.

Pythagoras did not agree to this new theorem because it contradicted his
basic convictions about numbers, however he could not find a mistake in
the proof of Hippasus, and this created a conflict with him which finally
escalated in sentencing him to death. (The school of Pythagoras had a strict
code of conduct which included the penalty of death by drowning.)

\noindent
More details are at {\tt http://encyclopedia.thefreedictionary.com/Square+root+of+2}.

\smallskip

{\bf Remark 2.}
In order to keep the proof simple I omitted the details about
the {\em type} of the numbers (positive, different from zero, etc.). 
They can be easily filled in (left as an exercise for the reader).

{\bf Remark 3.}
Another useful exercise is to identify the formal inference steps
(sequent rules) which are used -- most of them are the same or very
similar to the ones discussed in the lecture.

{\bf Remark 4.}
The same proof works for the irrationality of the square root of any prime number.

\end{document}