%!TEX root = proofs+concepts.tex

\chapter[Two-column proofs]{\texorpdfstring{T\kern-4ptwo\kern1pt-\kern-3ptColumn Proofs}{Two-Column Proofs}}
\label{ch.threecolumn}

\begin{quote}
\it No way of thinking or doing, however ancient, can be trusted without proof. 
What everybody echoes or in silence passes by as true to-day 
\\ may turn out to be falsehood to-morrow, mere smoke of opinion\dots
\par\raggedleft \small\rm\sf
Henry David Thoreau (1817--1862), American author 
\\
\emph{Walden}
\end{quote}

%\begin{quote}
%\it \dots\ it is undesirable to believe a proposition when there is no ground whatsoever for supposing it is true.
%\par\raggedleft \small\rm\sf
%Bertrand Russell (1872--1970), British philosopher 
%\\
%\emph{On the Value of Scepticism}
%\end{quote}

\medskip\noindent
The aim of a \emph{proof} is to show that a deduction is valid, and it does this by putting together a number of simpler deductions that are already known to be valid. 
%This method has two major benefits over evaluating the conclusion for all possible values of the variables that make the hypotheses true.
%	\begin{itemize}
%	\item A proof justifies a deduction in a way that can give us an understanding of \emph{why} the deduction is valid, rather than merely verifying that it can be trusted. 
%	\item A proof is often much shorter, and easier to verify, than a case-by-case consideration of all possible values of the variables.
%	\end{itemize}
%For example, if a deduction has 10 assertion letters, and you have to evaluate the conclusion for all possible values of the variables, then the number of different cases you will need to look at is $2^{10} = 1024$. That would take a tremendous amount of work, and, in practice, no one will want to check all of that work to make sure you have not made a mistake. At the same time, there may be a short proof that takes only a few minutes of work to check.
%
%\begin{rem}
Ultimately, our goal is to teach you to write clear and correct proofs, in English, of claims stated in English. But we will start with the simpler situation of proofs written in the language of {\SL}. This has several advantages:
	\begin{itemize}
	\item it allows assertions to be written more concisely, because entire English phrases are abbreviated to a single letter,
	\item it avoids the difficulties caused by the fact that sentences written in English can be ambiguous,
	and
	\item it displays the logical structure of a proof in a way that makes it easier to decide whether or not each step in a proof is valid. 
	\end{itemize}
After you are familiar with proofs in this simpler setting, you will employ the same principles to write proofs in English. 
%\end{rem}





\section{First example of a two-column proof} \label{sect.ThreecolumnIntro}

Let us begin our exploration of proofs by looking at the following simple deduction. 

\begin{earg} 
 \item \label{UseIfElimEg-eif} $P \eif (Q \eand R)$ 
 \item \label{UseIfElimEg-P} $P$
  \conclusion $R$
 \end{earg}
 
 \noindent 
% (Note that the hypotheses have been numbered for ease of reference.)
% 
 %You could verify that this deduction is valid by evaluating the conclusion for all possible values of the variables that make the hypotheses true. That would not be difficult, but let us take a different approach. Namely, w
 We will prove that it is valid by showing it is a combination of deductions that are already known to be valid.
%For the time being, we will ignore the English interpretation, and refer only to the symbols as we prove that the deduction is valid.  An English version of the proof is given later (on pages~\pageref{useelimsproof} and \pageref{useelimsEnglishproof}).  
Informally, we could try to convince someone that the deduction is valid by making the following explanation:

\begin{quote}
Assume the Hypotheses (1) and~(2) are true. Then applying $\eif$-elimination (with $P$ in the role of~$A$, and $Q \eand R$ in the role of~$B$) establishes that $Q \eand R$ is true. (This is an \emph{intermediate conclusion}. It follows logically from the hypotheses, and is helpful, but it is not the conclusion we want.) Now, applying $\eand$-elimination (with $Q$ in the role of~$A$, and $R$~in the role of~$B$) establishes that $R$ is true. This is the conclusion of the deduction. Thus, we have seen that if the hypotheses of this deduction are true, then the conclusion is also true. So the deduction is valid. 
\end{quote}
For emphasis, let us repeat that this explanation %allows us to avoid considering all the possible values of the variables; instead, we showed 
shows that the deduction is merely a combination of deductions that were already known to be valid.

\begin{rem}
Notice that we are using the fact that a valid deduction applies to all possible values of its variables, so we can plug any assertions we want into its variables. This is what allows us to talk about using (for example) ``$Q \eand R$ in the role of~$B$\rlap.''  
Another way of saying this, is that we are introducing a new symbolization key in which we let $A$ stand for~$P$, and let $B$ stand for $Q \eand R$. 
%%It would make no sense to say that because we know something about whether Bill baked an apple pie, we can conclude something about whether or not the Queen and the Registrar are here.  It is the form of the deduction that we are re-using, not the assertions themselves.
%Or, in the terms of high-school algebra, the known deductions remain valid even when we plug complicated expressions into its variables.
\end{rem}

Formally, a \define{proof} is a sequence of assertions. The first assertions of the sequence are assumptions; these are the hypotheses of the deduction. It is required that every assertion later in the sequence is an immediate consequence of earlier assertions. (You will soon be given specific rules that determine which assertions are allowed to appear at each point in the proof.) The final assertion of the sequence is the conclusion of the deduction.

In this \lcnamecref{ch.threecolumn}, we use the format known as ``\define[proof!two-column]{two-column proofs}'' for writing our proofs.  
%However, we will actually have an additional column for the English-language version of the proof, so we call them ``\define[two-column proof]{two-column proofs}\rlap.'' 
As indicated in the tableau below:
\begin{itemize}
\item Assertions appear in the left column.
\item The reason (or ``justification'') for including each assertion appears in the right column.
(The allowable justifications will be discussed in the later sections % !!!
of this \lcnamecref{ch.threecolumn}.)
%\item The English-language version appears at the right.
\end{itemize}

\twocolpf{
\pfline{}{\langle\text{\it assertion}\rangle}{$\langle\text{\it justification}\rangle$}
}

\vskip-\medskipamount

\factoidbox{Every assertion in a two-column proof needs to have a justification in the second column.}
% The following sections explain the justifications that are allowed. 

\medskip % !!!

For clarity, we draw a dark horizontal line to separate the hypotheses from the rest of the proof. (In addition, we will number each row of the proof, for ease of reference, and we will make the left border of the figure a dark line.) For example, here is a two-column proof that justifies the deduction above.
It starts by listing the hypotheses of the deduction, and ends with the correct conclusion.

\twocolpf{
\pfline{1}{P \eif (Q \eand R)}{hypothesis}%{If the Pope is here, then the Queen \newline and the Registrar are also here.}
\pfline{2}{P}{hypothesis}%{The Pope is here.}
\hypend
\pfline{3}{Q \eand R}{$\eif$-elim (lines 1 and 2)}%{The Queen and the Registrar are both here.}
\pfline{4}{R}{\AndElim{3}}%{The Registrar is here.}
}%\label{useelimsproof}

In this example, the assertions were written in the language of {\SL}, but sometimes we will write our proofs in English. For example, here is a symbolization key that allows us to translate $P$, $Q$, and~$R$ into English.
%From this point on, whenever we give a symbolic deduction, such as the one above, we will also provide a symbolization key and the corresponding English-language version of the deduction.  For example, here is a symbolization key, and English-language version, to accompany the above deduction. 
For convenience, this same symbolization key will be used in many of the examples in this chapter.

\begin{ekey} \label{PQRkey}
\item[P]The Pope is here.
\item[Q]The Queen is here.
\item[R]The Registrar is here.
\end{ekey} 

Now, we can translate the deduction into English:
\begin{earg}
\item If the Pope is here, then the Queen and the Registrar are also here.
\item The Pope is here.
\conclusion The Registrar is here.
\end{earg}
And we can provide a two-column proof in English:
\twocolpf{
\pfline{1}{\splitline{If the Pope is here, then the Queen \qline and the Registrar are also here.}}{hypothesis}
\pfline{2}{\text{The Pope is here.}}{hypothesis}
\hypend
\pfline{3}{\text{The Queen and the Registrar are both here.}}{\IfElim{1}{2}}
\pfline{4}{\text{The Registrar is here.}}{\AndElim{3}}
}

While you are getting accustomed to two-column proofs, it will probably be helpful to see examples in \emph{both} English \emph{and} {\SL}. To save space, and make it easier to compare the two, the text will sometimes combine both proofs into one figure, by adding a third column at the right that states the English-language versions of the assertions:
%\begin{itemize}
%\item Assertions of {\SL} appear in the left column.
%\item The reason for including each assertion appears in the middle column.
%\item The English-language version appears at the right.
%\end{itemize}

\threecolpf{
\pfline{}{\left\langle\begin{matrix} \text{\it assertion in} \\ \text{\it {\SL}} \end{matrix} \right\rangle}
{$\langle\text{\it justification}\rangle$}
{\hfil $\left\langle \begin{matrix} \hbox{\it English-language version} \\[-6pt]  \hbox{\it of the assertion} \end{matrix} \right\rangle$}
}

For example, here is what we get by combining the above two proofs:

\threecolpf{
\pfline{1}{P \eif (Q \eand R)}{hypothesis}{\splitline{If the Pope is here, then the Queen \qline and the Registrar are also here.}}
\pfline{2}{P}{hypothesis}{The Pope is here.}
\hypend
\pfline{3}{Q \eand R}{$\eif$-elim \\(lines 1 and 2)}{The Queen and the Registrar are both here.}
\pfline{4}{R}{\AndElim{3}}{The Registrar is here.}
}\label{useelimsproof}

%\begin{warn}
%You should keep in mind that 
%the symbolic deduction, if it is valid, would be valid for \emph{every} symbolization key and corresponding
%English-language version.  The English is only there to serve as an example and to give you
%another way of thinking about the deduction.  Do not draw any conclusions from the English version unless you are sure that the corresponding conclusions are justified in the purely symbolic version.  It may be, however, that thinking about the English version will give you some insight into what conclusions are justified in the symbolic version.  
%\end{warn}

The next few sections will explain the justifications that are allowed in a two-column proof.


\section{Hypotheses and theorems in two-column proofs} \label{sect.ThreecolumnHyps}

A two-column proof must start by listing all of the hypotheses of the deduction, and
each hypothesis is justified by writing the word \define{hypothesis} in the second column. (This is the only rule that is allowed above the dark horizontal line, and it is not allowed below the dark horizontal line.) We saw this rule in the above examples of two-column proofs. As a synonym for ``hypothesis\rlap,'' one sometimes says ``given'' or ``assumption\rlap.''

Any deduction that is \emph{already known to be valid} can be used as a justification \emph{if} its hypotheses have been verified earlier in the proof. (And the lines where the hypotheses appear are written in parentheses after the name of the theorem.) For example, the theorems ``$\eif$-elim'' and ``$\eor$-elim were used in our first examples of two-column proofs. These and several other very useful theorems were given in \cref{BasicThmEx}. You will be expected to be familiar with all of them.

\begin{eg}
Here is a proof of the deduction
	$$ P \eor Q, \quad Q \eif R, \quad\enot P, \quad \therefore R .$$
We provide an English translation by using the symbolization key on page~\pageref{PQRkey}.
\threecolpf{
\pfline{1}{P \eor Q}{hypothesis}{Either the Pope is here, or the Queen is here.}
\pfline{2}{Q \eif R}{hypothesis}{\splitline{If the Queen is here, then \qline the Registrar is also here.}}
\pfline{3}{\enot P}{hypothesis}{The Pope is not here.}
\hypend
\pfline{4}{Q}{\OrElim{1}{3}}{The Queen is here.}
\pfline{5}{R}{\IfElim{2}{4}}{The Registrar is here.}
}
\end{eg}

\begin{eg} \label{LJValidProof}
Here is a proof of the deduction $\enot L \eif (J \eor L)$, $\enot L$, \ \therefore $J$.
\twocolpf{
\pfline{1}{\enot L \eif (J \eor L)}{hypothesis}
\pfline{2}{\enot L}{hypothesis}
\hypend
\pfline{3}{J \eor L}{\IfElim{1}{2}}
\pfline{4}{J}{\OrElim{3}{2}}
}
\noindent
%This proof is much shorter, and easier to check, than the case-by-case analysis of our original solution.
\end{eg}


\begin{exer}
\label{pr.justify{\SL}proofaWBAJK}
Provide a justification (rule and line numbers) for each line of this proof.
%, as well as a symbolization key and an English-language interpretation.
%\medskip
%%\begin{problist}
%\vbox{%\item
%\begin{multicols}{2}
%\begin{ekey}
%\item[W]
%\item[B]
%\item[A]
%\item[J]
%\item[K]
%\end{ekey}
%\end{multicols}
\twocolpf{
\pfline{1}{W \eif \enot B}{\mbox{\hskip 3.5in}}%{\ }
\pfline{2}{A \eand W}{}%{}
\pfline{3}{\enot B \eif (J \eand K)}{}%{}
\hypend
\pfline{4}{W}{}%{}
\pfline{5}{\enot B} {}%{}
\pfline{6}{J \eand K} {}%{}
\pfline{7}{K}{}%{}
}
%}
%\end{problist}
\end{exer}

\begin{exer} \label{2col(AorNotA->B}
Provide a justification (rule and line numbers) for each line of this proof.
\twocolpf{
\pfline{1}{A \eif B}{\mbox{\hskip 3.5in}}%{\ }
\pfline{2}{\enot A \eif B}{}%{}
\hypend
\pfline{3}{A \eor \enot A}{}%{}
\pfline{4}{B}{}%{}
}
\end{exer}

\begin{exers} \label{First2col}
%Using the symbolization key
%\begin{ekey}
%\item [E]Eomer has the Ring
%\item [F]Frodo has the Ring
%\item [G]Golum has the Ring
%\end{ekey}
Write a two-column proof of each of the following deductions:
\begin{multicols}{2}
\begin{problist}
\item  \label{First2col-PQR}
$P\eor Q$, \ $Q\eor R$, \ $\enot Q$, \ \therefore\ $P \eand R$.
\item  \label{First2col-EFG}
$(E\eor F) \eor G$, \ $\enot F \eand \enot G$, \ \therefore\ $E$.
\end{problist}
\end{multicols}
\end{exers}

\goodbreak % !!!

\begin{exers} \label{3ColPQREasy}
Write a two-column proof of each of the following deductions. 
(Write the assertions in English.)
\begin{problist}
\item  \label{3ColPQREasy-PandQ,Q}
\begin{earg}
\item []The Pope and the Queen are here.
\conclusion The Queen is here.
\end{earg}
\item \label{3ColPQREasy-P,RandQ,QandP}
\begin{earg}
\item []The Pope is here.
\item []The Registrar and the Queen are here.
\conclusion The Queen and the Pope are here.
\end{earg}
\item  \label{3ColPQREasy-P->Q,Q->R,P,R}
\begin{earg}
\item []If the Pope is here, then the Queen is here.
\item []If the Queen is here, then the Registrar is here.
\item []The Pope is here.
\conclusion The Registrar is here.
\end{earg}
\item  \label{3ColPQREasy-GraceAndFrank}
Grace is sick.
\\ Frank is sick.
\\ \therefore~Either Grace and Frank are both sick, or Ellen is sick.
\end{problist}
\end{exers}



 \begin{eg}
Many proofs use the Rules of Negation or the fact that any statement is logically equivalent to its contrapositive.
Here is an example.
%\vbox{%\item
%%\begin{multicols}{2}
%\begin{ekey}
%\item[A] I ate an apple.
%\item[B] I ate a banana.
%\item[C] I ate a cherry.
%\item[D] I ate a donut.
%\end{ekey}
%%\end{multicols}
\threecolpf{
\pfline{1}{\enot P \eif (Q \eand R)}{hypothesis}{If the Pope is not here, then the Queen and the Registrar are here.}
%\pfline{2}{(B \eor \enot A) \eif D}{hypothesis}{If either I ate a banana, or I did not eat an apple, then I ate a donut.}
\pfline{2}{\enot Q \eor \enot R}{hypothesis}{Either the Queen is not here, or the Registrar is not here.}
\hypend
\pfline{3}{\enot(Q \eand R) \eif \enot \enot P}{contrapositive of line~1}{If it is not the case that both the Queen and the Registrar are here, then it is not the case that the Pope is not here.}
\pfline{4}{(\enot Q \eor \enot R) \eif P}{Rules of Negation \\ applied to line 3}{If it is the case either that the Queen is not here, or that the Registrar is not here, then the Pope is here.}
\pfline{5}{P}{\IfElim{4}{2}}{The Pope is here.}
%\pfline{7}{B \eor \enot A}{\OrIntro{6}}{}
%\pfline{8}{D}{\IfElim{2}{7}}{}
}%}
\end{eg}


\goodbreak % ???

\begin{exer}
 \label{pr.justify{\SL}proofeasy}
Provide a justification (rule and line numbers) for each line of these proofs.
%, as well as a symbolization key and an English-language interpretation.

\medskip
\begin{problist}

\vbox{
\item \label{pr.justify{\SL}proofeasy-FandG->I} \ \vskip-1.5\baselineskip
%\begin{ekey}
%\item[F]
%\item[G]
%\item[H]
%\item[I]
%\end{ekey}
\twocolpf{
\pfline{1}{H \eif F}{\mbox{\hskip 3.5in}}%{\ }
\pfline{2}{H \eif G}{}%{\ }
\pfline{3}{(F \eand G) \eif I}{}%{\ }
\pfline{4}{\enot I}{}%{\ }
\hypend
\pfline{5}{\enot I \eif \enot (F \eand G)}{}%{\ }
\pfline{6}{\enot (F \eand G)}{}%{\ }
\pfline{7}{\enot F \eor \enot G}{}%{\ }
\pfline{8}{\enot F \eif \enot H}{}%{\ }
\pfline{9}{\enot G \eif \enot H}{}%{\ }
\pfline{10}{\enot H}{}%{\ }
}
}

\vbox{
\item \label{pr.justify{\SL}proofeasy-(WorX)->(YorZ)} \ \vskip-1.5\baselineskip
%\begin{ekey}
%\item[W]
%\item[X]
%\item[Y]
%\item[Z]
%\end{ekey}
\twocolpf{
\pfline{1}{(W \eor X) \eif (Y \eand Z)}{\mbox{\hskip 3.0in}}%{\ }
\pfline{2}{\enot Y}{}%{\ }
\hypend
\pfline{3}{\enot Y \eor \enot Z}{}%{\ }
\pfline{4}{\enot(Y \eand Z) \eif \enot (W \eor X)}{}%{\ }
\pfline{5}{(\enot Y \eor \enot Z) \eif (\enot W \eand \enot X)}{}%{\ }
\pfline{6}{\enot W \eand \enot X}{}%{\ }
\pfline{7}{\enot X}{}%{\ }
}
}

\end{problist}
\end{exer}



\begin{exers}
\label{pr.basicproofargABLMNO}
Give a two-column proof of each of these deductions. 
%Include a symbolization key and an English-language interpretation. %deduction in {\SL}.
\begin{problist}
\item\label{pr.basicproofargABLMNO-AB}
 $A \eif B$, $\enot B$, $\therefore \enot A$
\item \label{pr.basicproofargABLMNO-LMNO}
$(L \eor M) \eif (N \eand O)$, $M$, $\therefore O$
\item \label{pr.basicproofargABLMNO-Pope}
\begin{earg}
\item[] Either the Pope is not here, or the Queen is here.
\item[] The Pope is here.
\conclusion Either the Queen is here, or else the Registrar and the Pope are both here.
\end{earg}
\item \label{pr.basicproofargABLMNO-Sammy}
\begin{earg}
\item[] If Sammy is not tired, then she does not need a nap.
\item [] Sammy needs a nap.
\conclusion Sammy is tired.
\end{earg}
\end{problist}
\end{exers}

\begin{rem}
You should also  remember that $\eand$ and~$\eor$ are commutative, so, for example, 
	$$ \hbox{$F \eif \bigl( (E \eand D \eand C \eand B) \eor (A \eand B) \bigr)
	\quad \equiv \quad
	F \eif \bigl( (A \eand B) \eor (B \eand C \eand D \eand E) \bigr)$.} $$
\end{rem}






\section{Subproofs for \texorpdfstring{$\eif$}{if}-introduction}
\label{IfIntroSect}

Consider this deduction:
\begin{center}
\begin{tabular}{cll}
$P \eif R$&\hspace{1cm}&If the Pope is here, then the Registrar is here.\\
$\hence (P \eand Q) \eif R$&&\begin{minipage}[t]{.6\linewidth}If the Pope and the Queen are both here,\qline  then the Registrar is here.\end{minipage}
\end{tabular}
\end{center}

The deduction is a valid one. Intuitively, we can justify it by noting that if $P \eand Q$ is true, then $P$~is certainly true, so the hypothesis implies $R$~is true. Thus, we have verified that $(P \eand Q) \eif R$. The $\eif$-introduction rule will allow us to turn this intuitive justification into an official proof.

We begin the proof by writing down the hypothesis of the deduction and drawing a dark horizontal line, like this:

\threecolpf{
	\pfline{1}{P \eif R}{hypothesis}{If the Pope is here, then the Registrar is here.}
	\hypend
}

\noindent 
The conclusion of the deduction is an assertion about what happens when $P \eand Q$ is true. That is, we want to see what happens if we assume, for the sake of argument, that the assertion $P \eand Q$ is true. To accomplish this, what we will do is start a \define{subproof}, a proof within the main proof, where we assume that $P \eand Q$ is true. When we start a subproof, we start a new set of double columns, and indent them from the left margin. Then we write in an assumption for the subproof. This can be anything we want. In the case at hand, we want to assume $P \eand Q$. Our proof now looks like this:

\threecolpf{
	\pfline{1}{P \eif R}{hypothesis}{If the Pope is here, then the Registrar is here.}
	\hypend
	\subproof{
		\pfline{2}{P \eand Q}{assumption}{Suppose the Pope and the Queen are both here.}
		\hypend
	}
}

It is important to notice that we are not claiming to have proven $P \eand Q$ (that the Pope and the Queen are here). 
%We do not need to write in any justification for the assumption line of a subproof. 
You can think of the subproof as posing the question: What could we show \emph{if} $P \eand Q$ were true? For one thing, we can derive~$P$. So we do:

\threecolpf{
	\pfline{1}{P \eif R}{hypothesis}{If the Pope is here, then the Registrar is here.}
	\hypend
	\subproof{
		\pfline{2}{P \eand Q}{assumption}{Suppose the Pope and the Queen are both here.}
		\hypend
		\pfline{3}{P}{\AndElim{2}}{The Pope is here.}
	}
}

And now, since the Pope is here, we can derive~$R$, from the hypothesis that $P \eif R$:

\threecolpf{
	\pfline{1}{P \eif R}{hypothesis}{If the Pope is here, then the Registrar is here.}
	\hypend
	\subproof{
		\pfline{2}{P \eand Q}{assumption}{\splitline{Suppose the Pope and the Queen \qline are both here.}}
		\hypend
		\pfline{3}{P}{\AndElim{2}}{The Pope is here.}
		\pfline{4}{R}{\IfElim{1}{3}}{The Registrar is here.}
	}
}

This has shown that \emph{if} we had $P \eand Q$ as a hypothesis, \emph{then} we could prove $R$. In effect, we have proven $(P \eand Q) \eif R$: that if the Pope and the Queen are here, then the Registrar is here. In recognition of this, the if-introduction rule ($\eif$-intro) will allow us to close the subproof and derive $(P \eand Q) \eif R$ in the main proof. Our final proof looks like this:

\threecolpf{
	\pfline{1}{P \eif R}{hypothesis}{\splitline{If the Pope is here, then \qline the Registrar is here.}}
	\hypend
	\subproof{
		\pfline{2}{P \eand Q}{assumption}{\splitline{Suppose the Pope and the Queen \qline are both here.}}
		\hypend
		\pfline{3}{P}{\AndElim{2}}{The Pope is here.}
		\pfline{4}{R}{\IfElim{1}{3}}{The Registrar is here.}
	}
	\pfline{5}{(P \eand Q) \eif R}{\IfIntro{2}{4}}{\splitline{If the Pope and the Queen are both \hbox to 0pt{here,\hss}% avoid overfull !!!
	\qline then the Registrar is here.}}
}

Notice that the justification for applying the $\eif$-intro rule is the entire subproof. Usually that will be more than just three lines.

It may seem as if the ability to assume anything at all in a subproof would lead to chaos: does it allow you to prove any conclusion from any hypotheses? The answer is no, it does not. Consider this proof:

\threecolpf{
	\pfline{1}{P}{hypothesis}{The Pope is here.}
	\hypend
	\subproof{
		\pfline{2}{Q}{assumption}{Suppose that the Queen is here.}
		\hypend
		\pfline{3}{Q}{\Repeat{2}}{As mentioned previously, the Queen is here.}
	}
}

It may seem as if this is a proof that you can derive any conclusion $Q$ (such as the conclusion that the Queen is here) from any hypothesis $P$ (such as the hypothesis that the Pope is here). When the vertical line for the subproof ends, the subproof is \emph{closed}. In order to complete a proof, you must close all of the subproofs. And you cannot close the subproof and use the repeat rule again on line~4 to derive~$Q$ in the main proof. Once you close a subproof, you cannot refer back to individual lines inside it.
\factoidbox{You \textbf{cannot} use a line from a subproof as a hypothesis
\\ for a theorem that is being applied in the main proof. 
\\ Lines in a subproof stay in the subproof.}
\factoidbox{In particular, you \textbf{cannot} use the repeat theorem to 
\\copy a line from a subproof into the main proof.}
%Closing a subproof is called \emph{discharging} the assumptions of that subproof. So we can put the point this way: You cannot complete a proof until you have discharged all of the assumptions besides the original hypotheses of the deduction.

Of course, it is legitimate to do this:

\threecolpf{
	\pfline{1}{P}{hypothesis}{The Pope is here.}
	\hypend
	\subproof{
		\pfline{2}{Q}{assumption}{Suppose that the Queen is here.}
		\hypend
		\pfline{3}{Q}{\Repeat{2}}{As mentioned previously, the Queen is here.}
	}
	\pfline{4}{Q\eif Q}{$\eif$-intro\\ (lines 2 and 3)}{If the Queen is here, then the Queen is here.}
}

This should not seem so strange, though. Since $Q\eif Q$ is a tautology, it follows validly from any hypotheses.

\vbox{% !!!
Put in a general form, the {\mathversion{bold}\define[implies ($\eif$)!-introduction@-introduction]{$\eif$-introduction}} rule looks like this:

\threecolpf{
	\subproof{
		\pfline{m}{\script{A}} {assumption (want \script{B})}{Suppose that Alberta is big.}
		\hypend
		\pfline{}{\vdots}{\hskip0.6in \vdots}{\hfil $\vdots$}
		\pfline{n}{\script{B}}{$\langle\mbox{\it whatever reason}\rangle$}{Then BC is big.}
	}
	\pfline{}{\script{A}\eif\script{B}}{\IfIntro{m}{n}}{If Alberta is big, then BC is big.}
}
}
When we introduce a subproof, it is helpful to make a note of what we want to derive (and add it to the justification). This is so that anyone reading the proof will find it easier to understand why we are doing what we are doing (and also so that we do not forget why we started the subproof if it goes on for five or ten lines). There is no ``want'' rule. It is a note to ourselves and to the reader; it is not formally part of the proof.

Although it is legal to open a subproof with any assumption you please, there is some strategy involved in picking a useful assumption. Starting a subproof with an arbitrary, wacky assumption would just waste lines of the proof. In order to derive an if-then statement by using $\eif$-intro, for instance, you must assume the hypothesis of the statement in a subproof.


Now that we have both the introduction rule and the elimination rule for ``implies\rlap,'' we can prove that the following deduction is valid:
\par\smallskip
{ \renewcommand{\arraystretch}{1.2}
\begin{tabular}{ccll} \label{proofHS}
\hbox{\hskip2\parindent} & $P \eif Q$&\hspace{1cm}& If the Pope is here, then so is the Queen.\\
&$Q \eif R$&& If the Queen is here, then so is the Registrar.\\
&\hence $P \eif R$&& 
Therefore, if the Pope is here, then so is the Registrar.
\end{tabular}
}
\smallskip

We begin the proof by writing the two hypotheses as assumptions. Since the main logical operator in the conclusion is~$\eif$, we can expect to use the $\eif$-introduction rule. For that, we need a subproof---so we write in the hypothesis of the if-then statement as the assumption of a subproof:

\threecolpf{
	\pfline{1}{P \eif Q}{hypothesis}{If the Pope is here, then so is the Queen.}
	\pfline{2}{Q \eif R}{hypothesis}{If the Queen is here, then so is the Registrar.}
	\hypend
	\subproof{
		\pfline{3}{P}{assumption\\ (want $R$)}{Suppose that the Pope is here.}
		\hypend
	}
}

We made $P$ available by assuming it in a subproof, allowing us to apply $\eif$-elim to line~1. This gives us $Q$, which allows us to apply $\eif$-elim to line~2. Having derived $R$, we close the subproof. By assuming $P$ we were able to prove $R$, so $\eif$-elim completes the proof. Here it is written out:

\threecolpf{
\label{HSproof}
	\pfline{1}{P \eif Q}{hypothesis}{If the Pope is here, then so is the Queen.}
	\pfline{2}{Q \eif R}{hypothesis}{If the Queen is here, then so is the Registrar.}
	\hypend
	\subproof{
		\pfline{3}{P}{assumption ({want $R$)}}{Suppose that the Pope is here.}
		\hypend
		\pfline{4}{Q}{\IfElim{1}{3}}{The Queen is here.}
		\pfline{5}{R}{\IfElim{2}{4}}{The Registrar is here.}
	}
	\pfline{6}{P \eif R}{\IfIntro{3}{5}}{If the Pope is here, then so is the Registrar.}
}


\begin{exer}
\label{IfIntroPLEx}
Provide a justification (rule and line numbers) for each line of these proofs.
%, as well as a symbolization key and an English-language interpretation.

\medskip
\begin{problist}

\vbox{
\item \label{IfIntroPLEx-ABC} \ \vskip-1.5\baselineskip
\twocolpf{
\pfline{1}{A \eif B}{}%{\ }
\pfline{2}{\enot A \eif C}{}%{}
\hypend
\pfline{3}{A \eor \enot A}{}%{}
	\subproof{
	\pfline{4}{A}{\mbox{\hskip 3.5in}}%{}
	\hypend
	\pfline{5}{B}{}%{}
	\pfline{6}{B \eor C}{}%{}
	}
\pfline{7}{A \eif (B \eor C)}{}%{}
	\subproof{
	\pfline{8}{\enot A}{\mbox{\hskip 3.5in}}%{}
	\hypend
	\pfline{9}{C}{}%{}
	\pfline{10}{B \eor C}{}%{}
	}
\pfline{11}{\enot A \eif (B \eor C)}{}%{}
\pfline{12}{B \eor C}{}%{}
}
}

\vfil

\vbox{
\item \label{IfIntroPLEx-LO} \ \vskip-1.5\baselineskip
%\begin{ekey} 
%\item[L]
%\item[O]
%\end{ekey}
\twocolpf{
\pfline{1}{L \eiff \enot O}{}%{\ }
\pfline{2}{L \eor \enot O}{}%{}
\hypend
\subproof{
	\pfline{3}{L}{\mbox{\hskip 3.5in}}%{\ }
	\hypend
	\pfline{4}{L}{}%{}
}
\pfline{5}{L \eif L}{}%{}
\pfline{6}{\enot O \eif L}{}%{}
\pfline{7}{L}{}%{}
}
}

\vfil

\vbox{
\item \label{IfIntroPLEx-FGHI} \ \vskip-1.5\baselineskip
%\begin{ekey} 
%\item[F]
%\item[G]
%\item[H]
%\item[I]
%\end{ekey}
\twocolpf{
\pfline{1}{F \eif \bigl( (G \eand H) \eor I \bigr)}{}%{\ }
\pfline{2}{\enot I}{}%{}
\hypend
\subproof{
	\pfline{3}{\enot G}{\mbox{\hskip 2.5in}}%{\ }
	\hypend
	\pfline{4}{\enot G \eor \enot H}{}%{}
	\pfline{5}{(\enot G \eor \enot H) \eand \enot I}{}%{}
	\pfline{6}{\enot \bigl((G \eand H) \eor I \bigr)}{}%{}
	\pfline{7}{\enot \bigl((G \eand H) \eor I \bigr) \eif \enot F}{}%{}
	\pfline{8}{\enot F}{}%{}
}
\pfline{9}{\enot G \eif \enot F}{}%{}
\pfline{10}{\enot \enot F \eif \enot \enot G}{}%{}
\pfline{11}{F \eif G}{}%{}
}
}

\vfil

\vbox{
\item \label{IfIntroPLEx-ABC2} \ \vskip-\baselineskip
%\begin{ekey}
%\item[A]
%\item[B]
%\item[C]
%\end{ekey}
\twocolpf{
\pfline{1}{\enot C \eif B \eor C}{}%{\ }
\hypend
\pfline{2}{C \eor \enot C}{}%{\ }
\subproof{
	\pfline{3}{C}{\mbox{\hskip 3.5in}}%{\ }
	\hypend
	\pfline{4}{B \eor C}{}%{\ }
}
\pfline{5}{C \eif (B \eor C)}{}%{\ }
\pfline{6}{B \eor C}{}%{\ }
\subproof{
	\pfline{7}{A \eand \enot B}{\mbox{\hskip 3.5in}}%{\ }
	\hypend
	\pfline{8}{\enot B}{}%{\ }
	\pfline{9}{C}{}%{\ }
}
\pfline{10}{(A \eand \enot B) \eif C}{}%{\ }
}
}

\vfil

\vbox{
\item \label{IfIntroPLEx-ZCN} \ \vskip-\baselineskip
%\begin{ekey}
%\item[Z]
%\item[C]
%\item[N]
%\end{ekey}
\twocolpf{
\pfline{1}{Z \eif (C \eand \enot N)}{}% {}
\pfline{2}{\enot Z \eif (N \eand \enot C)}{}%{}
\hypend
\pfline{3}{Z \eor \enot Z}{}%{}
\subproof{
	\pfline{4}{Z}{\mbox{\hskip 3.5in}}%{\ }
	\hypend
	\pfline{5}{C \eand \enot N}{}%{\ }
	\pfline{6}{C}{}%{\ }
	\pfline{7}{N \eor C}{}%{\ }
}
\pfline{8}{Z \eif (N \eor C)}{}%{}
\subproof{
	\pfline{9}{\enot Z}{\mbox{\hskip 3.5in}}%{\ }
	\hypend
	\pfline{10}{N \eand \enot C}{}%{\ }
	\pfline{11}{N}{}%{\ }
	\pfline{12}{N \eor C}{}%{\ }
}
\pfline{13}{\enot Z \eif (N \eor C)}{}%{}
\pfline{14}{N \eor C}{}%{}
}
}

\vfil

\vbox{
\item \label{IfIntroPLEx-ACE} \ \vskip-1.5\baselineskip
%\begin{ekey} 
%\item[A]
%\item[C]
%\item[E]
%\end{ekey}
\twocolpf{
\pfline{1}{A \eif E}{}%{\ }
\pfline{2}{C \eif E}{}%{}
\hypend
\subproof{
	\pfline{3}{A \eor C}{\mbox{\hskip 3.5in}}%{\ }
	\hypend
	\pfline{4}{E}{}%{}
}
\pfline{5}{(A \eor C) \eif E}{}%{}
}
}

\vfil

\end{problist}
\end{exer}


 

\begin{exers} \label{PQRIfIntro}
Write a two-column proof of each of the following deductions:
\begin{problist}

\item  \label{PQRIfIntro-P->S}
$P \eif (Q \eor R)$, $Q \eif S$, $R \eif S$, \quad \therefore\ $P \eif S$

%Using our symbolization key about the Pope, the Queen, and the Registrar, w
\item  \label{PQRIfIntro-Q->R}
$Q \eif (Q \eif P)$, \quad \therefore\ $Q \eif P$
%\begin{earg}
%\item []If the Queen is here, then if the Queen is here so is the Pope.
%\conclusion If the Queen is here, then so is the Pope.
%\end{earg}

\item \label{PQRIfIntro-M}
$M\eor(N\eif M)$, \quad \therefore\ $\enot M \eif \enot N$

\item   \label{PQRIfIntro-R->(QorP)}
$R \eif \Bigl(R \eif \bigl(R \eif (R \eif Q) \bigr) \Bigr)$, \quad \therefore $R \eif (Q \eor P)$
%\begin{earg}
%\item []If the Registrar is here, then if the Registrar is here, then if the Registrar is here, then if the Registrar is here, then so is the Queen.
%\conclusion  If the Registrar is here, then either the Queen or the Pope is here.
%\end{earg}
%\end{problist}
%\end{exers}

\item \label{PQRIfIntro-ABCDE}
%Include a symbolization key and an English-language interpretation. 
$A \eor B$, $A \eif C$, $B \eif D$, $C \eif E$, $D \eif E$, \quad $\therefore E$ 
%\hint{Use proof by cases from the previous chapter.}

%
%%\begin{exers}
%%Give a two-column proof for each of these deductions.  Include a symbolization key and an English-language interpretation.
%%\begin{problist}
%%\item $A\eiff B$, $B\eiff C$, \therefore\ $A\eiff C$
%%\item $A \eiff B$, $\therefore A \eif B$
%%\item $A \eiff B$, $\therefore B \eif A$
%%\end{problist}
%%\end{exers}

%\begin{exers}
%Using our symbolization key about the Pope, the Queen, and the Registrar, write a two-column proof for the following deduction:
%\begin{problist}
\item   \label{PQRIfIntro-P<>R}
\begin{earg}
\item [] The Pope is here if and only if the Queen is here.
\item [] The Queen is here if and only if the Registrar is here.
\conclusion The Pope is here if and only if the Registrar is here.
\end{earg}
%\item
%\begin{earg}
%\item []The Registrar is here if and only if the Queen is here.
%\item [\therefore]The Queen is here if and only if the Registrar is here.
%\end{earg}
%\item
%\begin{earg}
%\item []The Queen is here if and only if the Pope is here.
%\item [\therefore]The Queen is here if and only if either the Pope or the Queen is here.
%\end{earg}
\item   \label{PQRIfIntro-JimIsSick}
\begin{earg}
\item[] If Jim is sick, he should stay in bed.
\item [] If Jim is not sick, he should go outside to play.
\conclusion Jim should either stay in bed or go outside to play.
\end{earg}
\item   \label{PQRIfIntro-KingSing}
\begin{earg}
\item[] If the King will sing, then the Queen will sing.
\item[] If the King and the Queen will both sing, then the Prince and the Princess will also sing.
\item[] If the King and the Queen and the Prince and the Princess will all sing, then the party will be fun.
\conclusion If the King will sing, then the party will be fun.
\end{earg}
\item   \label{PQRIfIntro-PopeThenSpy}
\begin{earg}
\item[] If the Pope is here, then either the Queen is here or the Registrar is here.
\item[] If the Queen is here, then the Spy is here.
\item[] If the Registrar is here, then the Spy is here.
\conclusion If the Pope is here, then the Spy is here.
\end{earg}
\end{problist}
\end{exers}





\section{Proof by contradiction} \label{PfByContraSect}

\smallskip

\begin{quote}
\it
How often have I said to you that when you have eliminated the impossible,
whatever remains, \emph{however improbable,} must be the truth?
\\
\raggedleft\small\rm\sf
Sherlock Holmes, fictional British detective
\\
in \emph{The Sign of the Four}
\end{quote}

\noindent
The usual way to prove that an assertion is false is to show that it cannot be true. We do this by considering what would happen if it were indeed true. That is, we assume, for the sake of argument, that the assertion is true. If, by using logic, we can show that this assumption leads to a contradiction, then we can conclude that the hypothesis was wrong: the assertion we are interested in must be false. This is known as \define[proof!by contradiction]{proof by contradiction}. 

Proofs by contradiction are used quite commonly in everyday life. Here is a contrived example:

\begin{eg}
Suppose someone has stolen a bracelet from Ms.~Haslot's parlour. Could the butler have done it? Inspector Thinkright might say: ``Let us suppose that Jeeves, the butler, took the bracelet. We know he was in the kitchen until 8pm, so the theft must have taken place at a later time. However, Jeeves is highly allergic to Fifi, and that dog was in the parlour from 7:30pm until the theft was discovered at midnight, so Jeeves must have sneezed continuously while he was in the parlour. But the security guard absolutely refutes this: he states unequivocally that there were precisely 2 coughs, and no sneezes at all, coming from the parlour last evening. Thus, Jeeves could \emph{not} have taken the bracelet; we eliminate him as a suspect\rlap.''
\end{eg}

They also arise in mathematics:

\begin{eg}
Here is an argument  in English that shows there is no greatest (i.e., largest) natural number:
\begin{assertlist}
\item[] Suppose there is some greatest natural number. Call it $n$.
\item[] Then $n + 1$ is also a natural number.
And, obviously, $n+1 > n$.
\item[] So there is a natural number (namely, $n + 1$) that is greater than $n$.
\item[] This contradicts the fact that  $n$ is the greatest natural number.
\item[] So our hypothesis leads to consequences that are impossible.
\conclusion Our hypothesis cannot be true: there is no greatest natural number.
\end{assertlist}
\end{eg}
%This deduction form is traditionally called a \emph{reductio}. Its full Latin name is \emph{reductio ad absurdum}, which means ``reduction to absurdity\rlap.'' In a reductio, we assume something for the sake of argument---for example, that there is a greatest natural number. Then we show that the assumption leads to two contradictory assertions---for example, that $A$ is the greatest natural number and that it is not. In this way, we show that the original assumption must have been false.

The ``Proof by Contradiction'' rule allows us to turn an explanation of this type into an official proof. If we assume that a particular assertion is true and show that this leads to something impossible (namely, a contradiction), then we have proven that our assumption is wrong; the assumption must be false, so its negation must be true:
%This is the negation introduction ({\enot}I) rule:

\begin{ekey}
\item[\script{A}]Alberta is big.
\item[\script{B}]BC is big.
\end{ekey}
\threecolpf{
\subproof{
	\pfline{m}{\script{A}}{assumption \\ ({for contradiction})}{Suppose that Alberta is big.}
	\hypend
	\pfline{}{\vdots}{\hskip 0.5in\vdots}{\hfil$\vdots$}
	\pfline{n}{\script{B}\eand \enot\script{B}}{$\langle\mbox{\it whatever reason}\rangle$}{Then BC is big and BC is not big.}
}
\pfline{}{\enot\script{A}}{\NotIntro{m}{n}}{Alberta must not be big.}
}

For this rule to apply, the last line of the subproof must be an explicit contradiction of the form $\script{B} \eand \enot \script{B}$: some assertion and its negation. We write ``(will lead to a contradiction)'' or ``(for contradiction)'' as a note to ourselves and the reader. It is an explanation of why we started the subproof, and is not formally part of the proof. 

\begin{otherterm}
Proof by Contradiction allows us to put $\enot$ onto an assertion, so some logicians call it 
{\mathversion{bold}\define[not ($\enot$)!-introduction@-introduction]{$\enot$-introduction}}, but we use the terminology of mathematicians, who always refer to it as ``Proof by Contradiction\rlap.'' (And the {\mathversion{bold}\define[not ($\enot$)!-elimination@-elimination]{$\enot$-elimination}} rule is the fact that $\enot\enot A$ is logically equivalent to~$A$, which is one of the rules of negation in \fullcref{BasicEquivs}{negation}.)
\end{otherterm}

\begin{exers}
\label{pr.justify{\SL}proofb}
Provide a justification (rule and line numbers) for each line of these proofs.
%, as well as a symbolization key and an English-language interpretation.
%\smallskip
\begin{problist}

\item \label{pr.justify{\SL}proofb-ABC} \hskip-1.5em
%\begin{ekey}
%\item[A]
%\item[B]
%\item[C]
%\end{ekey}
\setbox0\vbox{%
\twocolpf{
\pfline{1}{\enot C \eif B \eor C}{}%{\ }
\hypend
\subproof{
	\pfline{2}{A \eand \enot B}{}%{\ }
	\hypend
	\subproof{
		\pfline{3}{\enot C}{\mbox{\hskip 3.5in}}%{\ }
		\hypend
		\pfline{4}{B \eor C}{}%{\ }
		\pfline{5}{B}{}%{\ }
		\pfline{6}{\enot B}{}%{\ }
		\pfline{7}{B \eand \enot B}{}%{\ }
	}
	\pfline{8}{\enot \enot C}{}%{\ }
	\pfline{9}{C}{}%{\ }
}
\pfline{10}{(A \eand \enot B) \eif C}{}%{\ }
}
}\raise2\baselineskip\hbox{\lower\ht0\copy0\hskip-25pt}


\vfil

\item \label{pr.justify{\SL}proofb-AB} \hskip-1.5em
%\begin{ekey}
%\item[A]
%\item[B]
%\end{ekey}
\setbox0\vbox{%
\twocolpf{
\pfline{1}{(A \eor B) \eif \enot B}{\mbox{\hskip 1.5in}}%{\ }
\hypend
\subproof{
	\pfline{2}{B}{\mbox{\hskip 3.5in}}%{\ }
	\hypend
	\pfline{3}{A \eor B}{}%{\ }
	\pfline{4}{\enot B}{}%{\ }
	\pfline{5}{B \eand \enot B}{}%{\ }
}
\pfline{6}{\enot B}{}%{\ }
}
}\raise2\baselineskip\hbox{\lower\ht0\copy0\hskip-25pt}


\vfil

\item \label{pr.justify{\SL}proofb-PQR} \hskip-1.5em
%\begin{ekey}
%\item[P]
%\item[Q]
%\item[R]
%\end{ekey}
\setbox0\vbox{%
\twocolpf{
\pfline{1}{P \eif Q}{\mbox{\hskip 1.5in}}%{\ }
\pfline{2}{Q \eif R}{}%{\ }
\pfline{3}{R \eif \enot P}{}%{\ }
\hypend
\subproof{
	\pfline{4}{P}{\mbox{\hskip 3.5in}}%{\ }
	\hypend
	\pfline{5}{Q}{}%{\ }
	\pfline{6}{R}{}%{\ }
	\pfline{7}{\enot P}{}%{\ }
	\pfline{8}{P \eand \enot P}{}%{\ }
}
\pfline{9}{\enot P}{}%{\ }
}
}\raise2\baselineskip\hbox{\lower\ht0\copy0\hskip-25pt}

\vfil

\item \label{pr.justify{\SL}proofb-PQR2} \hskip-1.5em
%\begin{ekey}
%\item[P]
%\item[Q]
%\item[R]
%\end{ekey}
\setbox0\vbox{%
\twocolpf{
\pfline{1}{(P \eor \enot Q) \eif \enot R}{\mbox{\hskip 1.5in}}%{\ }
\pfline{2}{Q \eif P}{}%{\ }
\hypend
\subproof{
	\pfline{3}{R}{\mbox{\hskip 1.5in}}%{\ }
	\hypend
	\subproof{
		\pfline{4}{Q}{\mbox{\hskip 3.0in}}%{\ }
		\hypend
		\pfline{5}{P}{}%{\ }
		\pfline{6}{P \eor \enot Q}{}%{\ }
		\pfline{7}{\enot R}{}%{\ }
		\pfline{8}{R \eand \enot R}{}%{\ }
	}
	\pfline{9}{\enot Q}{}%{\ }
	\pfline{10}{P \eor \enot Q}{}%{\ }
	\pfline{11}{\enot R}{}%{\ }
	\pfline{12}{R \eand \enot R}{}%{\ }
}
\pfline{13}{\enot R}{}%{\ }
}
}\raise2\baselineskip\hbox{\lower\ht0\copy0\hskip-25pt}

\vfil

\item \label{pr.justify{\SL}proofb-ZCN} \hskip-1.5em
%\begin{ekey}
%\item[Z]
%\item[C]
%\item[N]
%\end{ekey}
\setbox0\vbox{%
\twocolpf{
\pfline{1}{Z \eif (C \eand \enot N)}{\mbox{\hskip 1in}} %{}
\pfline{2}{\enot Z \eif (N \eand \enot C)}{}%{}
\hypend
\subproof{
	\pfline{3}{\enot(N \eor  C)}{\mbox{\hskip 1in}}%{\ }
	\hypend
	\subproof{
		\pfline{4}{N}{\mbox{\hskip 2.5in}}%{\ }
		\hypend
		\pfline{5}{N \eor C}{}%{}
		\pfline{6}{(N \eor C) \eand \enot(N \eor C)}{}%{}
	}
	\pfline{7}{\enot N}{}%{}
	\subproof{
		\pfline{8}{C}{\mbox{\hskip 2.5in}}%{\ }
		\hypend
		\pfline{9}{N \eor C}{}%{}
		\pfline{10}{(N \eor C) \eand \enot(N \eor C)}{}%{}
	}
	\pfline{11}{\enot C}{}%{}
	\subproof{
		\pfline{12}{Z}{\mbox{\hskip 3.25in}}%{\ }
		\hypend
		\pfline{13}{C \eand \enot N}{}%{}
		\pfline{14}{C}{}%{}
		\pfline{15}{C \eand \enot C}{}%{}
	}
	\pfline{16}{\enot Z}{}%{}
	\pfline{17}{N \eand \enot C}{}%{}
	\pfline{18}{N}{}%{}
	\pfline{19}{N \eand \enot N}{}%{}
}
\pfline{20}{\enot \enot (N \eor C)}{}%{}
\pfline{21}{N \eor C}{}%{}
}
}\raise2\baselineskip\hbox{\lower\ht0\copy0\hskip-25pt}

\end{problist}
\end{exers}

%\begin{exers} \label{AllMathnsExer}
%Use the following symbolization key to write a two-column proof for each of the following deductions.
%\begin{ekey}
%\item [A] Archimedes was a mathematician.
%\item [B] Boole was a mathematician.
%\item [C] Cayley was a mathematician.
%\item [D] Descartes was a mathematician.
%\end{ekey}
%\begin{problist}
%\item
%Archimedes was a mathematician if and only if Boole was a mathematician.  Therefore, 
%Archimedes was not a mathematician if and only if Boole was not a mathematician.
%\item
%Either Archimedes or Boole was a mathematician, and either Cayley or Descartes was a mathematician.
%If Boole was a mathematician, then so was Descartes.
%Descartes was not a mathematician.
%Therefore, both Archimedes and Cayley were mathematicians.
%\end{problist}
%\end{exers}

\begin{exers}
\label{pr.basicproofargQJM}
Give a two-column proof of each of these deductions.
% Include a symbolization key and an English-language interpretation. %deduction in {\SL}.
\begin{problist}
\item \label{pr.basicproofargQJM-Q}
$Q\eif(Q\eand\enot Q)$, \quad \therefore\ $\enot Q$
\item \label{pr.basicproofargQJM-J}
$J\eif\enot J$, \quad  \therefore\ $\enot J$
\item  \label{pr.basicproofargQJM-notUandV}
$U \eif X$, $V \eif \enot X$, \quad  \therefore\ $\enot (U \eand V)$
\item  \label{pr.basicproofargQJM-notM}
$(M \eor N) \eif \enot T$, $\enot T \eif \enot M$, \quad \therefore\ $\enot M$
\item  \label{pr.basicproofargQJM-AliceNotHere}
\begin{earg}
\item[] If Alice is here, then Bob is here.
\item [] If Bob is here, then Carol is here.
\item[] If Carol is here, then Bob is not here.
\conclusion Alice is not here.
\end{earg}

\end{problist}
\end{exers}






\section{Proof strategies} \label{ProofStrategiesSect}
\nobreak
Finding a proof is very much the same as solving a puzzle that tells you a starting position and a goal, and gives specific rules about exactly what steps you are allowed to take to complete the task. At each step (of a proof or a puzzle) there are several options for what to do, and you need to choose the right one. There is no simple recipe that will always tell you what to do; being successful requires the same skills that you need to solve a maze.

\begin{exer} \label{MazeEx}
Find a path through each maze from the top left corner to the bottom right corner.

\medskip

%\begin{problist}
\hbox to \textwidth{\includegraphics[scale=0.45]{PDF/maze1.pdf}
\hfil  \includegraphics[scale=0.45]{PDF/maze2.pdf}}
\bigskip
\hbox to \textwidth{\includegraphics[scale=0.45]{PDF/maze3.pdf}
\hfil \includegraphics[scale=0.45]{PDF/maze-backward.pdf}}
\end{exer}


There is no substitute for practice, but here are some suggestions and strategies to keep in mind when doing proofs.



%\item \emph{Consider both the English and {\QL} statements of your hypotheses and desired conclusion.} Either may give you ideas about how to proceed.

% could use \subsection*, but that would put these in the table of contents
\newcommand{\ProofStrategy}[1]{\par\medbreak{\bf #1}}

\ProofStrategy{Work forwards from what you have.}
Look at the hypotheses (and any other assertions that you have derived so far). Think about the elimination rules for the main operators in these assertions. These will tell you what your options are.
For example:
	\begin{itemize}
	\item If you have $P \eand Q$, you can immediately obtain both~$P$ and~$Q$. 
	\item If you have both $P$ and $P \eif Q$, you can use $\eif$-elimination to obtain~$Q$.
	\item If you have $P \eor Q$, you should consider using a proof by cases. 
	\end{itemize}

\begin{exer} \label{strategy:A->BandC}
  Give a two-column proof of the deduction 
$$ \text{$A \eif (B \eand C)$, $A$, \ $\therefore C$} $$
 \end{exer}

\ProofStrategy{Work backwards from what you want.}
The ultimate goal is to derive the conclusion. Look at the conclusion and ask what the introduction rule is for its main logical operator. This gives you an idea of where you want to be \emph{just before} the last line of the proof. Then you can treat this line as if it were your goal; we call it a \define{subgoal} because it represents partial progress toward the true goal. Ask what you could do to derive the subgoal. 
For example:
\begin{itemize}
\item If your conclusion is $\script{A}\eand\script{B}$, then you need to figure out a way to prove~$\script{A}$ and a way to prove $\script{B}$.
\item If your conclusion is a conditional $\script{A}\eif\script{B}$, plan to use the $\eif$-intro rule. This requires starting a subproof %(a separate paragraph) 
in which you assume~\script{A}. In the subproof, you want to derive~\script{B}.
\item The last % is it still the last !!!
 of the four mazes in \cref{MazeEx} is easy if you work backwards from the finish, instead of forward from the start.
\end{itemize}

\begin{exer}
\label{pr.basicproofargPQRS-P->Q}
 Give a two-column proof of the deduction 
$$ \text{$(P \eor Q) \eif (R \eand S)$, $(R \eor S) \eif (P \eand Q)$, $\therefore P \eif Q$} $$
 \end{exer}


\ProofStrategy{Try breaking the proof down into cases.}
%This is a technique that comes from the fact that if $P \eif Q$ and $\enot P \eif Q$ are both true, then $Q$~must be true. (See Exercise~\fullref{pr.justify{\SL}proofb}{PfByCases}.) 
If it looks like you need an additional hypothesis ($A$) to prove what you want, try considering two cases: since $A \eor \enot A$ is a tautology (``Law of Excluded Middle''), it suffices to prove that~$A$ and~$\enot A$ each yield the desired conclusion.

\begin{exer}
 \label{pr.basicproofargPQRS-S}
 Give a two-column proof of the deduction 
$$ \text{$P \eif Q$, $\enot P \eif R$, $(Q \eor R) \eif S$, $\therefore S$} $$
 \end{exer}


\ProofStrategy{Look for useful subgoals.}
Working backwards is one way to identify a worthwhile subgoal, but there are others. For example, if you have $\script{A} \eif \script{B}$, you should think about whether you can obtain~$\script{A}$ somehow, so that you can apply $\eif$-elimination.

\begin{exer}
\label{pr.basicproofargPQRS-R->P}
Give a two-column proof of the deduction 
$$ \text{$(R \eor S) \eif (P \eor Q)$, $\enot Q$, \  $\therefore R \eif P$} $$
\end{exer}

\ProofStrategy{Change what you are looking at.}
Replacement rules can often make your life easier; if a proof seems impossible, try out some different substitutions.
For example:
	\begin{itemize}
	\item the Rules of Negation should become second nature; they can often transform an assertion into a more useful form.
	\item Remember that every implication is logically equivalent to its contrapositive. The contrapositive may be easier to prove as a conclusion, and it might be more useful as a hypothesis.
%	\item It is often difficult to prove a disjunction $\script{A}\eor\script{B}$ by using the basic rules; it is often easier to show $\enot\script{A}\eif\script{B}$, which is a logically equivalent assertion. [If want to put this back in, should add an exercise to show that 
%	(A or B)  <=> ( (not A) => B ) 
%is a tautology.  Then students could refer to this known theorem in their 2-column proofs.}
	\end{itemize}

\begin{exer} \label{strategy:P+notPQ+QorR}
  Give a two-column proof of the deduction 
$$ \text{$P$, $\enot (P \eand Q)$, $Q \eor R$, \ $\therefore R$
} $$
 \end{exer}

%Showing $\enot \exists x\script{A}$ can also be hard, and it is often easier to show  $\forall x\enot \script{A}$ and use the QN rule.


\ProofStrategy{Do not forget proof by contradiction.}
If you cannot find a way to show something directly, try assuming its negation, and then look for a contradiction. For example, instead of proving $\script{A} \eor \script{B}$ directly, you can \emph{assume} both $\enot \script{A}$ and $\enot \script{B}$, which is likely to make the work easier.

%Remember that most proofs can be done either indirectly or directly. One way might be easier---or perhaps one sparks your imagination more than the other---but either one is formally legitimate. 

\begin{exer}
 \label{pr.basicproofargPQRS-notP}
  Give a two-column proof of the deduction 
$$ \text{$P \eif Q$, $Q \eif \enot P$, \ $\therefore \enot P$
} $$
 \end{exer}


\ProofStrategy{Repeat as necessary.} 
After you have made some progress, by either deriving some new assertions or deciding on a new goal that would represent substantial progress, see what the above strategies suggest in your new situation.

%Once you have decided how you might be able to get to the conclusion, ask what you might be able to do with the hypotheses. Then consider the target assertions again and ask how you might reach them.


\ProofStrategy{Persist.}
Try different things. If one approach fails, try something else. When solving a difficult maze, you should expect to have to backtrack several times, and the same is true when doing proofs.


\begin{exers}
\label{pr.basicproofargPQRS}
Give a two-column proof of each of these deductions.
%, using the symbolization key
%	\begin{ekey}
%	\item[P] The Pope is here.
%	\item[Q] The Queen is here.
%	\item[R] The Registrar is here.
%	\item[S] The Spy is here.
%	\end{ekey}
%to give an English-language interpretation. %deduction in {\SL}.
\begin{problist}
\item \label{pr.basicproofargPQRS-(PandNotQ)->(RorS)}
 $(P \eand \enot Q) \eif (Q \eor R)$, \ $\therefore (P \eand \enot Q) \eif (R \eor S)$
\item  \label{pr.basicproofargPQRS-P->S}
$P \eif (Q \eor R)$, $Q \eif \enot P$, $R \eif S$, \ $\therefore P \eif S$
\end{problist}
\end{exers}




\section{What is a proof?} \label{WhatIsPfSect}

\begin{quote}
\it I don't know --- a proof is a proof. What kind of a proof? It's a proof. A proof is a proof, and when you have a good proof, it's because it's proven.
\par\raggedleft\small\rm\sf
Jean Chr\'etien (b.\,1934), Prime Minister of Canada
%\smallskip
%\rightline{When asked what kind of proof he needed for the}
%\rightline{existence of weapons of mass destruction in Iraq.}
\end{quote}

\medskip

\noindent
The goal of a mathematical proof is to provide a completely convincing explanation that a deduction is valid. It needs to be so carefully written that it would hold up in court forever, even against your worst enemy, in any country of the world, and without any further explanation required. Fortunately, the rules of logic are accepted worldwide, so, if applied properly, they create an irrefutable case.

In the previous sections of this chapter, we wrote our proofs in two-column format. We will now start the transition to writing proofs in English prose; our ideas will be expressed in sentences and paragraphs, using correct grammar, combining words with appropriate mathematical notation.  A proof written in prose needs to convey the same information as would be found in a two-column proof, so essentially the same rules and strategies will still apply, but writing in ordinary English provides more freedom, and often leads to shorter proofs that are more reader-friendly. 
%Indeed, the proofs we write will essentially be a rephrasing of  the contents of the last two columns of a twocolumn proof, but, when it is helpful, mathematical notation from the first column may also be included.

%The techniques are the same, but we will express the ideas using words, sentences, and paragraphs, rather than in the rigid structure of the two-column format. 

\begin{rem}
The big advantage of two-column proofs is that the rules are very clear, so there are no ambiguities that require good judgment to resolve. This makes them easier for beginners who may have difficulty deciding what they are allowed to do. The disadvantage is that being required to record every detail of every step makes the proofs very verbose, so they cannot reasonably be used in the complicated situations that arise in the study of advanced mathematics.
\end{rem}

Just as when using the two-column format, our proofs will be a sequence of assertions that lead from the hypotheses to the desired conclusion. Each assertion must have a logical justification based on assertions that were stated earlier in the proof.  Any subproof (for $\eif$-introduction or Proof by Contradiction) will form a paragraph of its own within the proof. 

Before the proof begins, we always provide a statement of the theorem that will be proved.
\begin{itemize}
\item The statement is preceded by the label ``Theorem'' (or a suitable substitute).  
%This will be given a title.  The title will include a key word such as ``Theorem\rlap,'' ``Proposition\rlap,'' ``Lemma\rlap,'' or ``Corollary\rlap.''  
\item The statement of the result begins with a list all of the hypotheses. To make it clear that they are assumptions, not conclusions, this list of assertions is introduced by an appropriate word or phrase such as ``Assume\dots\rlap,'' or ``Suppose that \dots\rlap,'' or ``If \dots\rlap,''  or  ``Let \dots\rlap.''
\item The statement of the result ends with a statement of the desired conclusion, introduced by an appropriate word or phrase such as ``Then \dots\rlap,'' or ``Therefore, \dots\rlap.''
\end{itemize}
Following the statement of the result, we begin our proof in a new paragraph.
	\begin{itemize}
	\item The proof is labelled with the single word: ``Proof\rlap.'' 
	\item We then proceed to give a well-organized series of assertions that logically lead from our hypotheses to the desired conclusion. 
% The last assertion in this series will be the assertion of the desired conclusion itself.  The proof is then wrapped up in a separate, concluding paragraph, that will state ``Therefore\rlap,'' and repeat (or paraphrase) the statement of the result.  
	\item A small square is drawn at the right margin at the end of the proof to signify that the proof is complete.
	\end{itemize}


For example, here is how the \lcnamecref{ch.threecolumn}'s first deduction could be treated:

\begin{thm*}
Assume:
	\begin{enumerate} \renewcommand{\theenumi}{\alph{enumi}}
	\item \label{useelimsEnglishproof-PQR}
 if the Pope is here, then the Queen and the Registrar are both here, 
	and
	\item \label{useelimsEnglishproof-P}
 the Pope is here.
	\end{enumerate}
Then the Registrar is here.
\end{thm*}

\begin{proof}  \label{useelimsEnglishproof}
From Assumption~\pref{useelimsEnglishproof-P}, we know that the Pope is here. Therefore, Assumption~\pref{useelimsEnglishproof-PQR} tells us that the Queen and the Registrar are both here. In particular, the Registrar is here.
\end{proof}

Here is another example:

\begin{eg} \label{EnglishEg(P->QorR)} \ 

\begin{earg}
\item \label{EnglishPfP->QorRHyp}
 If the Pope is here, and the Queen is not here, then the Registrar is here.
\conclusion If the Pope is here, then either the Queen or the Registrar is also here.
\end{earg}
\end{eg}

\begin{proof}[Proof by contradiction] 
Suppose the conclusion is false. (This will lead to a contradiction.) This means that the Pope is here, but neither the Queen nor the Registrar is here. In particular, the Pope is here and the Queen is not here, so Hypothesis~\pref{EnglishPfP->QorRHyp} tells us that the Registrar is here. However, since neither the Queen nor the Registrar is here, we also know that the Registrar is not here. Therefore, the Registrar is both here and not here. This is a contradiction.
\end{proof}

\begin{proof}[Alternate proof]
Suppose the Pope is here. (We wish to show that either the Queen or the Registrar is also here.)  From the Law of Excluded Middle, we know that the Queen is either here or not here, and we consider these two possibilities as separate cases.

\setcounter{case}{0}

\begin{case}
Assume the Queen is here.
\end{case}
Then it is true that either the Queen or the Registrar is here, as desired.

\begin{case}
Assume the Queen is not here.
\end{case}
Then the Pope is here, and the Queen is not here. From Hypothesis~\pref{EnglishPfP->QorRHyp}, we conclude that the Registrar is here. Therefore, either the Queen or the Registrar is here, as desired.
\end{proof}

\begin{rem}
Note that some of the rules of the two-column format are relaxed for proofs written in prose:
\begin{enumerate}
\item We will no longer list all of the hypotheses at the start of our proof. Instead, we refer to the list that is in the statement of the theorem. 
\item We will no longer make a practice of numbering all of the assertions in our proofs. However, if there is a particular assertion that will be used repeatedly, we may label it with a number for easy reference. 
\item We will usually not cite the basic rules of {\SL} by name every time they are used. However, we should be able to justify any assertion with a rule, if called upon to do so.  
\end{enumerate}
\end{rem}

\begin{exer} \label{TranslateEnglishEg}
Translate both proofs of \cref{EnglishEg(P->QorR)} into two-column format (using our usual symbolization key).
\end{exer}

%Here is a sample outline of this format:

%\begin{thm} 
%{\bf Suppose that} $\langle$list all hypotheses$\rangle$.  {\bf Then} $\langle$state the desired conclusion$\rangle$.
%\end{thm}

%\begin{proof}
%$\langle$\emph{A series of assertions, with justifications, leading from the hypotheses to the desired conclusion.  The last of these assertions is the desired conclusion itself.}$\rangle$.
%\end{proof}

\goodbreak % !!!
\begin{exers} \label{1stPfInEnglish}
Write a proof of each of these theorems in English prose.
\begin{problist}

\item   \label{1stPfInEnglish-Pope->Registrar}
\begin{earg}
\item   \label{1stPfInEnglish-Pope->Registrar-PopeQueen}
If the Pope is here, then the Queen is here.
\item   \label{1stPfInEnglish-Pope->Registrar-QueenRegistrar}
If the Queen is here, then the Registrar is here.
\conclusion If the Pope is here, then the Registrar is here.
\end{earg}

\item  \label{1stPfInEnglish-Spy} 
\begin{thm*}
Assume:
	\begin{enumerate}
		\makeatletter \renewcommand{\p@enumii}{} \makeatother
	\item \label{1stPfInEnglish-Spy-P->R} 
	If the Pope is here, then the Registrar is here.
	\item  \label{1stPfInEnglish-Spy-Q->S} 
	If the Queen is here, then the Spy is here.
	\item  \label{1stPfInEnglish-Spy-P&Q} 
	The Pope and the Queen are both here.
	\end{enumerate}
Then the Registrar and the Spy are both here.
\end{thm*}

\item    \label{1stPfInEnglish-ABC}
\begin{thm*}
Assume:
	\begin{enumerate} 
			\makeatletter \renewcommand{\p@enumii}{} \makeatother
	\item  \label{1stPfInEnglish-ABC-AB}
	If Adam is here, then Betty is here.
	\item  \label{1stPfInEnglish-ABC-BC}
	If Betty is not here, then Charlie is here.
	\item  \label{1stPfInEnglish-ABC-AC}
	Either Adam is here, or Charlie is not here.
	\end{enumerate}
Then Betty is here.
\end{thm*}

\item  \label{1stPfInEnglish-Jack&Jill}
\begin{thm*}
Assume:
	\begin{enumerate} 
	\makeatletter \renewcommand{\p@enumii}{} \makeatother%% need \ref to return (a), (b), (c), instead of 2a, 2b, 2c for these hyps
	\item \label{JackJillPf-wrong}
	 If Jack and Jill went up the hill, then something will go wrong.
	\item \label{JackJillPf-JackJill}
	 If Jack went up the hill, then Jill went up the hill.
	\item  \label{JackJillPf-nothing}
	Nothing will go wrong.
	\end{enumerate}
Then Jack did not go up the hill.
\end{thm*}

%\begin{proof}
%The contrapositive of \pref{JackJillPf-wrong} tells us that if nothing will go wrong, then Jack and Jill did not both go up the hill. Hence, we conclude from \pref{JackJillPf-nothing} that Jack and Jill did not both go up the hill.

%Now suppose Jack went up the hill. Then, from \pref{JackJillPf-JackJill}, we know that Jill also went up the hill. So Jack and Jill both went up the hill. This contradicts the conclusion of the preceding paragraph. Hence, our assumption must be false: contrary to what we assumed, it must be the case that Jack did not go up the hill.
%\end{proof}
\end{problist}
\end{exers}







\section{Counterexamples} \label{CounterSect}

Not all deductions are valid. To show that a particular deduction is \emph{not} valid, you need to show that it is possible for its conclusion to be false at the same time that all of its hypotheses are true. 
To do this, you should find an assignment to the variables that makes all of the hypotheses true, but makes the conclusion false. 

\begin{eg}
Show that the deduction
	$$ A \eor B, \quad A \eif B, \quad \therefore\ A $$
is not valid.
%For example, consider the following deduction:\\
%\vbox{
%\begin{earg}
% \item[] $A \eor B$,
% \item[] $A \eif B$,
% \conclusion $A$.
% \end{earg}
% }
\end{eg}

\begin{scratchwork}
To make the conclusion false, we let $A$ be false. Then, to make the first hypothesis true, we must let $B$ be true. Fortunately, this also makes the second hypothesis true.
\end{scratchwork}

\begin{solution}
Let $A$ be false, and let $B$ be true. Then
	$$ A \eor B \qeq \false \eor \true \qeq \true $$
and
	$$ A \eif B \qeq \false \eif \true \qeq \true, $$
so both hypotheses of the deduction are true. However, the conclusion of the deduction (namely,~$A$) is false.

Since we have a situation in which both hypotheses of the deduction are true, but the conclusion of the deduction is false, the deduction is not valid. 
\end{solution}


\begin{defn}
Any situation in which all of the hypotheses of a deduction are true, but the conclusion is false, is called a \define{counterexample} to the deduction.
\end{defn}
\factoidbox{ To show that a deduction is \emph{not} valid, find a counterexample. }

\begin{exer} \label{FindCounteregsEx}
Show that each of these deductions is invalid, by finding a counterexample.
\begin{tasks}(2)
\task\fixtask \label{FindCounteregsEx-IfAThenB}%
$A \eor B$, \therefore$A \eif B$
\task\fixtask \label{FindCounteregsEx-PandQ}%
$P \eor Q$, \ \therefore$P \eand Q$
\task\fixtask \label{FindCounteregsEx-C}%
$A \eif (B \eand C)$, \ $\enot A \eif (B \eor C)$, \ \therefore $C$
\task\fixtask \label{FindCounteregsEx-Qand(PorR)}%
$P \eif Q$, $\enot P \eif R$,  \therefore $Q \eand (P \eor R)$
\end{tasks}
\end{exer}




\begin{summary}

\item A ``two-column proof'' is a tool that we use to learn techniques for writing proofs.
\begin{itemize}
\item The left-hand column contains a sequence of assertions.
\item The right-hand column contains a justification for each assertion.
\item Each row of the proof is numbered (in the left margin) for easy reference.
%\item The right-hand column contains an English-language version of the deduction, based on an accompanying symbolization key.
\item A dark horizontal line is drawn to indicate the end of the hypotheses.
\item A dark horizontal line is drawn along the left edge of the proof, and of each subproof.
\end{itemize}
\item In addition to the basic theorems of {\SL}, we have two rules that use subproofs:
\begin{itemize}
\item $\eif$-introduction
\item proof by contradiction
\end{itemize}
\item Proofs often use the Law of Excluded Middle, the Rules of Negation, and contrapositives.
\item Assertions that are in a subproof cannot be used as justification for lines that are not in that same subproof. 
%In particular, the repeat rule cannot be used to copy a line from a subproof into the main proof.
\item Writing proofs takes practice, but there are some strategies that can help.
\item Proofs can also be written in English prose, using sentences and paragraphs.
\item To show that a deduction is \emph{not} valid, find a counterexample.
\end{summary}

