\documentclass[10pt,twoside]{article}
\usepackage{amssymb}
\def\pline#1{\noindent #1}
\def\ste{\enspace\enspace\enspace\enspace}
\newcount{\rulco}
\newcount{\drulco}
%\def\co#1{#1}
\def\ruloin#1{\medbreak\noindent{\bf  RULE
\the\rulco.#1}\ }
\def\rulo#1{\global\advance\rulco by 1
\medbreak\noindent{\bf  RULE
\the\rulco.#1}\ }
\def\rulonn#1{\medbreak\noindent{\bf  RULE #1$\,$.}\ }
\def\rulon#1{\medbreak\noindent{\bf  RULE
\the\rulco.#1}\ }
\renewcommand{\iff}{\longleftrightarrow}
\def\drulo{\global\advance\drulco by 1
\medbreak\noindent {\bf DERIVED RULE
\the\drulco.}\ }
\def\justo{
\medbreak\noindent {\bf JUSTIFICATION$\,$:}\ \ }
\newcount{\quesco}
\def\quesno{\the\quesco \global\advance\quesco by 1}
\def\largebold{\large\bf}
\def\hugeee{\Huge}
\def\largerbold{\Large\bf}
\newcommand{\sepa}{\medbreak
\begin{center}$\,$\hbox to5cm{\hrulefill}$\,$\end{center}
\medbreak}
\def\nin{\noindent}
\def\mnin{\medbreak\noindent}
\def\bnin{\bigbreak\noindent}
\newcounter{boxcount}
\setcounter{boxcount}{0}
\newcommand{\boxon}[1]{\refstepcounter{boxcount}
\medbreak
\begin{center}
{\bf BOX NO. \theboxcount$\,$:\ \ #1.}
\end{center}
\medbreak}
\newcommand{\Ft}[1]{\footnote{\mynine\baselineskip 8pt #1}}
\def\vup{\vspace{-1mm}}
\def\imply{\longrightarrow}
\def\lto{\longrightarrow}
\def\zz{\mathbb{Z}}
\def\qq{\mathbb{Q}}
\def\cc{\mathbb{C}}
\def\rr{\mathbb{R}}
\def\nn{\mathbb{N}}
\def\itobf{\subsubsection}
\def\unde#1{\underbar{#1}}
\def\tto{\mbox{$\kern4pt\rightarrow\kern-14.3pt\mapsto\kern5pt$}}
\def\vepsi{V^{\beps,\eps,\delta}}
\def\vepsim{V^{\beps(m),\eps(m),\delta(m)}}
\def\kepsi{K^{\beps,\eps}}
\def\pepsi{P^{\beps,\eps}}
\def\phixeps{\Phi_x^{\beps}}
\newcommand{\bprn}{\begin{proof}}
\newcommand{\eprn}{\end{proof}}
\newenvironment{proof}{\noindent {\em Proof}.\ }{\medskip}
\def\So{{\rm So}}
\def\Ta{{\rm Ta}}
\def\Gr{{\rm Gr}}
\def\Do{{\rm Dom}}
\def\Im{{\rm Im}}
\def\acabx{AC([a,b],X)}
\def\cabx{C^0([a,b],X)}
\def\acomabx{AC_{\Omega}([a,b],X)}
\def\comabx{C_{\Omega}^0([a,b],X)}
\newcommand{\myput}{\input}
\newcommand{\authorsar}{\cite{antocell,bressancolombo,cellina,cellinaornelas,colomboetal,fry,ornelas}}
\newcommand{\dato}{\vskip 3cm
{\bf THIS IS A DRAFT.\\
\vskip 0.2cm
DO NOT QUOTE WITHOUT PERMISSION.\\
\vskip 0.2cm
Date of this draft: \today.}}
\renewcommand{\theequation}{\arabic{section}.\arabic{subsection}.\arabic{equation}}
\newcommand{\idx}{\index}
\renewcommand{\contentsname}{\hfil {\small{\bf Contents}}}
%\topmargin -1.5cm
\newcommand{\hjsdraft}{\hfill{\rm Math 300 - 04}}
\newcommand{\mpdraft}{{\rm Instructor's Notes, No. 1, 
September 5, 2001} \hfill }
\begin{document}
\markboth{\hjsdraft}{\mpdraft}\parskip 0pt
\def\lefquo{``} %``for home use
\newcommand{\tgt}{{T}^{2,\ge}}
\newcommand{\bi}{\begin{itemize}}
\newcommand{\comment}[1]{}
\newcommand{\ei}{\end{itemize}}
\def\beps{\bar\varepsilon}
\def\co{{\rm co}}
\def\cco{\overline{{\rm co}}}
\def\belo{\,\epsilon\,}
\def\lowsub#1{\lower 2pt\hbox{${_{#1}}$}}
\def\adj{{\rm Adj\,}}
\def\traj{{\rm Traj\,}}
\def\ctraj{{\rm CTraj\,}}
\def\arc{{\rm Arc\,}}
\def\carc{{\rm CArc\,}}
\def\bloi{{\cal BL}(\Omega,I)}
\def\blon{{\cal BL}(\rr^n,\rr)}
\def\bor{{\rm Bor}}
\def\leb{{\rm Leb}}
\def\blons{{\cal BL}(\rr^n,\rr;S)}
\def\mbloiy{{\cal M}_e(\bloi,Y)}
\def\blxr{{\cal BL}(X,\rr)}
\def\bbxr{{\cal B}(X\times\rr)}
\def\mblxr{{\cal M}(\blxr,Y)}
\def\cvf{TVVF}
\def\cvfadomi{TVVF_{AD}(\Om,I)}
\def\ndc{{\bf W}}
\def\togr{{\buildrel \rm igr \over \to}}
\newcommand{\halmos}{\rule{1ex}{1.4ex}}
\newcommand{\edo}{\end{document}}
%\newcommand{\indexentry}[2]{\smalltype #1,$\,$#2}
%\newcommand{\indexentry}[2]{#1,$\,$#2}
\newcommand{\eprnoen}{\hspace*{\fill}$\halmos$\medskip}
\newtheorem{ittheorem}{Theorem}
\newtheorem{itdef}{Definition} 
\newtheorem{itlem}{Lemma} 
\newtheorem{itprop}{Proposition}
\newtheorem{itcor}{Corollary}
\newtheorem{itrem}{Remark}
\newcounter{itfac}
\newcounter{itexam}
\newtheorem{myfact}[itfac]{Fact}
\newtheorem{myexample}[itexam]{Example}
\newtheorem{mytheorem}[ittheorem]{Theorem}
\newtheorem{mydefinition}[itdef]{Definition}
\newtheorem{mylemma}[itlem]{Lemma}
\newtheorem{myproposition}[itprop]{Proposition}
\newtheorem{mycorollary}[itcor]{Corollary}
\newtheorem{myremark}[itrem]{Remark}
\newcommand{\subssection}[1]{\subsection{#1}
   \setcounter{equation}{0}}
\newenvironment{theorem}{\begin{mytheorem}$\!\!\!{\bf .}$}{\end{mytheorem}}
\newenvironment{definition}{\begin{mydefinition}$\!\!\!{\bf .}$\rm}{\end{mydefinition}} %no-italics
\newenvironment{lemma}{\begin{mylemma}$\!\!\!{\bf .}$}{\end{mylemma}}
\newenvironment{corollary}{\begin{mycorollary}$\!\!\!{\bf .}$}{\end{mycorollary}}
\newenvironment{proposition}{\begin{myproposition}$\!\!\!{\bf .}$}{\end{myproposition}}
\newenvironment{remark}{\begin{myremark}$\!\!\!{\bf .}$\rm}{\end{myremark}} %no-italics
\newenvironment{fact}{\begin{myfact}$\!\!\!{\bf .}$}{\end{myfact}}
\newenvironment{example}{\begin{myexample}$\!\!\!{\bf .}$\rm}{\end{myexample}} %no-italics
\def\proofend{\hfill$\diamondsuit\,$}
\newcommand{\beq}{\begin{equation}}
\newcommand{\eeq}{\end{equation}}
\newcommand{\beqn}{\begin{eqnarray}}
\newcommand{\eeqn}{\end{eqnarray}}
\newcommand{\beqno}{\begin{eqnarray*}}
\newcommand{\eeqno}{\end{eqnarray*}}
\newcommand{\bequot}{\begin{quotation}}
\newcommand{\equot}{\end{quotation}}
\newcommand{\rf}[1]{[\ref{#1}]} %bibliographical references
\newcommand{\text}[1]{\hbox{\rm \ #1\ \/}}
\newcommand{\beql}[1]{\begin{equation}\label{#1}}
\newcommand{\bt}{\begin{theorem}}
\newcommand{\bl}{\begin{lemma}}
\newcommand{\br}{\begin{remark}}
\newcommand{\bc}{\begin{corollary}}
\newcommand{\bp}{\begin{proposition}}
\newcommand{\bd}{\begin{definition}}
\newcommand{\bfact}{\begin{fact}}
\newcommand{\bex}{\begin{example}}
\newcommand{\ber}[1]{\begin{exercise}\label{#1}}
\newcommand{\bem}[1]{\begin{example}\label{#1}}  %Yes, 2 different ones...
\newcommand{\ec}{\end{corollary}}
\newcommand{\el}{\end{lemma}}
\newcommand{\er}{\end{remark}}
\newcommand{\et}{\end{theorem}}
\newcommand{\ed}{\end{definition}}
\newcommand{\ednoen}{\end{definition}}
\newcommand{\eprop}{\end{proposition}}
\newcommand{\epr}{\end{proof}}
\newcommand{\bpr}{\begin{proof}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  These are just for statements, no "qed" box is put in.
%%  (Also for when I have to finish something after a displayed equation
%%        or itemized.)
\newcommand{\ecs}{\end{corollary}}
\newcommand{\eers}{\end{exercise}}
\newcommand{\eexs}{\end{example}}
\newcommand{\eems}{\end{example}}
\newcommand{\els}{\end{lemma}}
\newcommand{\eles}{\end{lemmaex}}
\newcommand{\ers}{\end{remark}}
\newcommand{\ets}{\end{theorem}}
\newcommand{\eds}{\end{definition}}
\newcommand{\eps}{\end{proposition}}
\newcommand{\efact}{\end{fact}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\mybox}{\hfill \mbox{$\Box$}} %put at right margin (white square)
\newcommand{\qed}{\mybox} %put qed at right margin


\def\bptl{\pmb{\partial}}
\def\bptld{\pmb{\partial}^{{\cal D}}}
\def\nball{\bmath^n}  
\def\idnpball{{\rm id}_{\partial\bmath_n}}
\def\idrn{{\rm id}_{\rr^n}}
\def\id{{\rm id}}
\def\nno{\nn\cup\{0\}}
\def\dom{{\rm Dom}}
\def\msr{{\rm meas}}
\def\mitem{\medbreak\item}
\def\uitem{\vspace{-3mm}\item}
\def\oitem{\vspace{-1.2mm}\item}
\def\bigparo{\parindent=23pt}
\def\miitem{\medbreak\itemitem}
\def\medno{\medbreak\noindent}
\def\smalltype{\baselineskip=8pt}
\def\normaltype{\baselineskip=11pt}
\def\dekkertype{\baselineskip=0.54true cm}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%% Set up for Black Board Bold (\Bbb) font
% N.B. \Bbb works only in math mode
%\def\aabx{{\cal A}([a,b],X)}
\def\convav#1{{\onarr{{\rm av}#1}}}
\def\convtr{{\onarr{{\rm T}}}}
\def\Om{\Omega}
\def\mtraj{{\rm MTraj\,}}
\def\indi{\raise 1.5pt\hbox{$\chi$}}
\def\lowsub#1{\lower 2pt\hbox{${_{#1}}$}}
\def\pfo#1{{\cal P}_{#1}^{\rightarrow}}
\def\pba#1{{\cal P}_{#1}^{\leftarrow}}  
\def\aabx{{\cal A}(a,b,X)}
\def\icone{IC\kern0.1pt$^1$}
\def\iconeit{IC\kern0.5pt$^1$}
\def\mdno{\medbreak\noindent}
\def\inn{\int_{0}^{\tau}}
\def\bel{\beta}
\def\al{\alpha}
\def\eps{\varepsilon}
\def\bes{\bar\varepsilon}
\def\bdel{\bar\delta}\def\ffi{\varphi}
\def\al{\alpha}
%\font\twelvemsy=msym10 scaled\magstep1
%\font\tenmsy=msym10
%\font\sevenmsy=msym7
%\font\tinyfont=cmr6 
%\newfam\msyfam
%\textfont\msyfam=\twelvemsy
%\scriptfont\msyfam=\tenmsy
%\scriptscriptfont\msyfam=\sevenmsy
%\def\Bbb{\fam\msyfam}
%\def\nn{\Bbb{N}}
\def\nninf{\bar{\Bbb{N}}}
%\def\pmb#1{\setbox0=\hbox{$#1$}%
%  \kern-.025em\copy0\kern-\wd0
%  \kern.05em\copy0\kern-\wd0
%  \kern-.025em\raise.0433em\box0 }
\def\pmb#1{\setbox0=\hbox{$#1$}%
  \kern-.025em\copy0\kern-\wd0
  \kern.05em\copy0\kern-\wd0
  \kern-.025em\raise.0144em\box0 
  \kern-.025em\raise.0288em\box0 
  \kern-.025em\raise.0433em\box0 }
\def\pmbsus{\pmb}
\def\equaldef{\,{\buildrel \rm def \over =}\,}
\def\steero{$\sim$\kern -0.1cm$\sim$\kern -0.1cm$\sim$\kern-0.2cm$>$\kern-0.28cm$>$\kern-0.28cm$>$\kern-0.28cm$>$\kern-0.28cm$>$\kern-0.28cm$>$\kern-0.28cm$>$\kern0.1cm}
\def\PPhi{\pmb{\Phi}}
\def\steer#1#2{$#1$\steero$#2$}
\def\steert#1#2#3{\hbox{$#1$\hbox{\lower0.4ex\hbox{\steero}}\kern-0.59cm\raise0.53ex\hbox{$#2$}}\kern0.35cm$#3$}
%BLACKBOARD BOLD
\def\vbar{\mathchoice{\vrule height6.3ptdepth-.5ptwidth.8pt\kern-.8pt}
   {\vrule height6.3ptdepth-.5ptwidth.8pt\kern-.8pt}
   {\vrule height4.1ptdepth-.35ptwidth.6pt\kern-.6pt}
   {\vrule height3.1ptdepth-.25ptwidth.5pt\kern-.5pt}}
\def\fudge{\mathchoice{}{}{\mkern.5mu}{\mkern.8mu}}
\def\bbc#1#2{{\rm \mkern#2mu\vbar\mkern-#2mu#1}}
\def\bbb#1{{\rm I\mkern-3.5mu #1}}
\def\bba#1#2{{\rm #1\mkern-#2mu\fudge #1}}
\def\bb#1{{\count4=`#1 \advance\count4by-64 \ifcase\count4\or\bba A{11.5}\or
   \bbb B\or\bbc C{5}\or\bbb D\or\bbb E\or\bbb F \or\bbc G{5}\or\bbb H\or
   \bbb I\or\bbc J{3}\or\bbb K\or\bbb L \or\bbb M\or\bbb N\or\bbc O{5} \or
   \bbb P\or\bbc Q{5}\or\bbb R\or\bbc S{4.2}\or\bba T{10.5}\or\bbc U{5}\or
   \bba V{12}\or\bba W{16.5}\or\bba X{11}\or\bba Y{11.7}\or\bba Z{7.5}\fi}}
\def\eps{\varepsilon}
\def\pmath{{\rm I}\kern-.2em{\rm P}}
\def\emath{{\rm I}\kern-.2em{\rm E}}
\def\bmath{{\rm I}\kern-.2em{\rm B}}
\def\rarr{\rightarrow}
\font\mymagfivebf=cmbx10 scaled\magstep 5
\font\mymagfiverm=cmr10 scaled\magstep 5
\font\mymagfourbf=cmbx10 scaled\magstep 4
\font\mymagfourrm=cmr10 scaled\magstep 4
\font\mymagthreebf=cmbx10 scaled\magstep 3
\font\mymagthreerm=cmr10 scaled\magstep 3
\font\mymagtwobf=cmbx10 scaled\magstep 2
\font\mymagtworm=cmr10 scaled\magstep 2
\font\mymagonebf=cmbx10 scaled\magstep 1
\font\mymagonerm=cmr10 scaled\magstep 1
\font\mymagzerobf=cmbx10 scaled\magstep 0
\font\mymagzerorm=cmr10 scaled\magstep 0
\font\mymagfivesl=cmsl10 scaled\magstep 5
\font\mymagfiveit=cmti10 scaled\magstep 5
\font\mymagfoursl=cmsl10 scaled\magstep 4
\font\mymagfourit=cmti10 scaled\magstep 4
\font\mymagthreesl=cmsl10 scaled\magstep 3
\font\mymagthreeit=cmti10 scaled\magstep 3
\font\mymagtwosl=cmsl10 scaled\magstep 2
\font\mymagtwoit=cmti10 scaled\magstep 2
\font\mymagonesl=cmsl10 scaled\magstep 1
\font\mymagoneit=cmti10 scaled\magstep 1
\font\mymagzerosl=cmsl10 scaled\magstep 0
\font\mymagzeroit=cmti10 scaled\magstep 0
\font\mynine=cmr9
\font\myninebf=cmbx9
\font\mysmall=cmr7
\font\mysmallit=cmti7
\font\myverysmall=cmr5
\def\figcap#1#2{\medbreak
\centerline{ Figure {#1}:\ #2}
\vbox to 0.3true in{\vfill}}
\def\mybigbreak{\vskip 0.3true in}
\def\mynotsobigbreak{\vskip 0.2true in}
%THE FOLLOWING MACROS WERE USED FOR THE 1987 CDC PAPER
\def\lip{{\rm Lip}}
\def\lipomy{{\rm Lip}(\Omega,Y)}
\def\rarr{\rightarrow}
\def\rint{\enspace\rightarrow\!\!\!\!\!\!\int}
\def\lint{\enspace\leftarrow\!\!\!\!\!\int}
\def\pvarieta{{\cal  P}({\bf P},\eta)}
\def\pvdata{{\bf P}=(m,{\bf t},{\bf r},{\bf E})}
\def\sre{S_{\rho}(\eta)}
\def\vari{E=\{\eta_{\varepsilon}:\varepsilon\in C\}}
\def\varii{E_{i}=\{\eta_{i,\varepsilon_{i}}:\varepsilon_{i}\in C_{i}\}}
\def\tou{trajectory of uniqueness}
\def\uzsig{{\cal U}_{0}(\Sigma)}
\def\uosig{{\cal U}_{1}(\Sigma)}
\def\uksig{{\cal U}_{k}(\Sigma)}
\def\sigisz{$\Sigma$ is a $C^{0}$ system}
\def\sigiso{$\Sigma$ is a $C^{1}$ system}
\def\sigisk{$\Sigma$ is a $C^{k}$ system}
\def\czad{$C^{0}$-admissible}
\def\coad{$C^{1}$-admissible}
\def\ckad{$C^{k}$-admissible}
\def\mysys{\Sigma=(M,U,f)}
\def\vk{(V,\kappa)}
\def\vkk{(V,\kappa,K)}
\def\chm{{\cal CH}(M)}
\def\km{{\cal K}(M)}
\def\kz{{\cal K}_{0}}
\def\kk{\kappa(K)}
\def\kv{\kappa(V)}
\def\rr{{\rm I}\kern-.2em{\rm R}}
\def\rrinf{\overline{\rr}}
\def\nn{{\rm I}\kern-.2em{\rm N}}
\def\nninf{\overline{\nn}}
\def\rrsmall{{\mysmall I}\kern-.2em{\mysmall R}}
\def\R{{\rm I}\kern-.2em{\rm R}}
\def\emath{{\rm I}\kern-.2em{\rm E}}
\def\pmath{{\rm I}\kern-.2em{\rm P}}
\def\lmath{{\rm I}\kern-.2em{\rm L}}
\def\ro{{\rr}}
\def\rn{{\rr}^{n}}
\def\rnn{{\rr}^{n\times n}}
\def\rnlow{{\rr}_{n}}
\def\vkinchm{(V,\kappa)\in {\cal CH}(M)}
\def\vkkinkm{(V,\kappa,K)\in {\cal K}(M)}
\def\vvkkinkm{{\cal V}=(V,\kappa,K)\in {\cal K}(M)}
\def\vvkkinkz{{\cal V}=(V,\kappa,K)\in {\cal K}_{0}}
\def\vinkm{{\cal V}\in {\cal K}(M)}
\def\vinkz{{\cal V}\in {\cal K}_{0}}
\def\xinkv{x\in\kappa(V)}
\def\xinkk{x\in\kappa(K)}
\def\fk{f^{\kappa}}
\def\fke{f_{\eta}^{\kappa}}
\def\fkeo{f_{\eta_{1}}^{\kappa}}
\def\fket{f_{\eta_{2}}^{\kappa}}
\def\fkei{f_{\eta_{i}}^{\kappa}}
\def\szve{\sigma_{{\cal V},\eta}^{0}}
\def\sove{\sigma_{{\cal V},\eta}^{1}}
\def\skve{\sigma_{{\cal V},\eta}^{k}}
\def\rzveoet{\rho_{{\cal V},\eta_{1},\eta_{2}}^{0}}
\def\roveoet{\rho_{{\cal V},\eta_{1},\eta_{2}}^{1}}
\def\rtildeoveoet{\tilde \rho_{{\cal V},\eta_{1},\eta_{2}}^{1}}
\def\rkveoet{\rho_{{\cal V},\eta_{1},\eta_{2}}^{k}}
\def\delzveoet{\delta_{\cal V}^{0}(\eta_{1},\eta_{2})}
\def\deloveoet{\delta_{\cal V}^{1}(\eta_{1},\eta_{2})}
\def\delkveoet{\delta_{\cal V}^{k}(\eta_{1},\eta_{2})}
\def\delkvee{\delta_{\cal V}^{k}(\eta,\eta)}
\def\delkv{\delta_{\cal V}^{k}}
\def\delkvj{\delta_{{\cal V}_{j}}^{k}}
\def\dome{{\rm Dom}(\eta)}
\def\domei{{\rm Dom}(\eta_{i})}
\def\domej{{\rm Dom}(\eta_{j})}
\def\domeo{{\rm Dom}(\eta_{1})}
\def\domet{{\rm Dom}(\eta_{2})}
\def\arrint{\rightarrow\kern -7.5pt\int}
\def\expint#1#2#3{e^{\arrint_{#1}^{#2}#3}}
\def\compo{\hbox{$\,${\myverysmall o}$\,$}}
\def\plplus{(+\kern-0.02in\compo\kern -0.02in\oplus)}
\def\Om{\Omega}
\def\om{\omega}
\def\restr{\lceil}
\def\ffi{\varphi}
\def\ep{\varepsilon}
\def\dki{{\partial\,\,\,\over\partial\kappa^i}}
\def\dkia{\partial_i^\kappa}
\def\dkonea{\partial_1^\kappa}
\def\dkna{\partial_n^\kappa}
\def\pdto{\,\rightarrow\kern -12pt ^{pd}\,}
\def\tvto{\,\rightarrow\kern -12pt ^{tv}\,}
\def\opdto{\,\longrightarrow\kern -18pt ^{opd}\,}
\def\pdtvto{\,\hbox to 1.1true cm{\rightarrowfill}\kern -20pt ^{pdtv}\,\,\,}
\def\tpdtvto{\,\hbox to 1.1true cm{\rightarrowfill}\kern -23pt ^{tpdtv}\,\,\,}
\def\adjo#1{{\rm Adj}(#1)}
\def\adjonul#1{{\rm Adj}^{\nu,L}(#1)}
\def\cch{\overline{co}}


%\voffset=-0.28true in
%\hsize=16true cm
%\vsize=9.45true in
%\parindent 0.25true in
\raggedbottom
%\def\onarr#1{\,\hbox to 0.4in{\rightarrowfill}\kern-0.25 in
%\raise 5pt\hbox{$#1$}\kern 0.2 in}
\def\onarr#1{\,\hbox to 0.37in{\rightarrowfill}\kern-0.37in
\raise 7pt\hbox to 0.37in{\hfill$#1$\hfill}\kern 0.04 in}
\def\nextarr#1{\,\,\,\,\,\,|\kern-3.8pt\lower 9.3pt
\hbox{$\downarrow$}\lower 3pt\hbox{$#1$}\,\,}
\def\pmbeta{{\pmb{\eta}\kern 0.02in}}
\def\pmbetas{{\pmbsus{\eta}\kern 0.02in}}

\setcounter{page}{1}
\pagenumbering{arabic}
\pagestyle{myheadings}
\thispagestyle{empty}
\setcounter{page}{37}


\begin{center}
{\mymagthreebf MATHEMATICS 300\ ---\  FALL 2001}

\bigbreak

{\mymagtwoit Introduction to Mathematical Reasoning}\\

 {\mymagtwoit (640 - 300, Section 04)}

\bigbreak

{\mymagtwoit  H. J. Sussmann}

\bigbreak

\vspace{0.7cm}

{\Large{\bf  INSTRUCTOR'S NOTES, PART 2}}\\
{\large{\em (October 8, 2001)}}

\end{center}

\bigbreak\noindent {\Large\em This is the final version (except for typos,
of which there probably are quite a few still left). 
{\bf This supersedes the previous preliminary version that you 
got on October 3.}}

\bigbreak



\begin{minipage}{12cm}
\baselineskip=9pt
{\tiny\tableofcontents}
\end{minipage}

\thispagestyle{empty}
\def\plin#1#2#3{\noindent\hbox to 0.4cm{\hfill#1.$\,$}
#2\ \ \hrulefill\ \hbox to 0.9cm{\hfill\ Page}\hbox to 0.6cm{\hfill #3}}

\medbreak

\setcounter{section}{9}

\section{Additional information on the course}

\subsection{The midterms (a reminder)}

{\bf Midterm dates:}   {\bf Monday October 15} and {\bf Wednesday November 28}.

\subsection{The final exam}

The {\bf final exam} will be on  {\bf Monday December 17, 8 to 11 pm}.

\vbox{
\subsection{Readings for the period from Sept. 5 to Oct. 10}


\begin{itemize}
\item{} the book's note ``To the Student,''
\item{} the book's  Chapter 1 ({\bf all of it!}),
\item{} the instructor's notes, Part 1,
\item{} the book's  Chapter 2 ({\bf all of it!}),
\item{} the instructor's notes, Part 2.
\end{itemize}
}

\subsection{Homework assignments for the first half of October}

\subsubsection{Assignment \ no. 4, \ due \ on \ Wednesday,
\mbox{October} 3.}

\begin{itemize}  
\item[A.] Redo Problem E of Assignment No. 1. Make sure that you use
the precise definition of ``sum of a series.'' (You can find this definition
in any Calculus textbook.) 

\item[B.] Problems 10 and 11 in page 41 of the book. 
\end{itemize}

\subsubsection{Assignment no. 5, due on Wednesday, October 10}

\medbreak
\begin{itemize}
\item[A.]  Section 7 of the book, Problems 1, 4, 7(c)(d), 8, 9.
\item[B.]  Section 8 of the book, Problems \ \ 1(b)(c)(d)(e)(g), 
\ \ \ 2(b)(c)(d)(e)(f)(g),\\
3(d)(e)(f)(g), 4, 6, 8, 9.
\item[C.] Here are five sentences about rabbits, unicorns, elephants, 
Peter, Dumbo, and the  binary relation ``taller than.''
\begin{itemize}
\item[(1)] Unicorns are taller than elephants. (That is, ``every unicorn is
taller than every elephant,'' or, if you prefer, ``for every $x$ and every 
$y$, if $x$ is a unicorn and $y$ is an elephant, then $x$ is taller than 
$y$.'') 
\item[(2)] Rabbits are taller than unicorns.
\item[(3)] If something is taller than something else which is in turn
taller than a third thing, then the first one is taller than the third
one.  (That is ``for every $x$, every $y$ and every $z$, if $x$ is taller
than $y$ and $y$ is taller than $z$, then $x$ is taller than $z$.'')
\item[(4)] Peter is a rabbit.
\item[(5)] Dumbo is an elephant. 
\end{itemize}
\item[] Using sentences (1), (2), (3), (4), (5), {\em and
{\bf no other fact} about rabbits, unicorns, elephants, Peter, 
Dumbo, and the
binary relation ``taller than,''}  prove that Peter is taller than Dumbo. 
\end{itemize}

\section{Proofs: an introduction}

\noindent A {\bf proof} of a statement $S$ 
is a {\em convincing argument} that establishes {\bf beyond the shadow
of a doubt} that $S$ is true.

You should think of proving statements as a {\bf game} that you are playing
against an opponent who does not believe that the statement you are proving
is true.  You make statements, your opponent may find them convincing or
not, and it is up to you to clear up all your opponent's doubts by 
arguing your case persuasively every time your opponent isn't convinced. 
(Maybe you should think that I, the instructor, am the ``opponent.''
{\bf You} have to convince {\bf me}. If you convince me, then your proof
has worked. Otherwise it has not.)

\subsection{What is a convincing argument?}

The trouble with the above remarks is that it is not very clear what
will count as a ``convincing argument.''  Suppose your opponent says,
after you have given what looks to you like a very convincing proof:
``I am not convinced; I don't see why what you just said proves
anything.''  How would you deal with something like that?

Moreover, any argument you give will have to {\it start} somewhere.  (You
cannot prove anything starting from nothing.)  What can you do if your
opponent refuses to accept your starting point?  

\bigbreak\noindent EXAMPLE: suppose you want to prove that, 

\medbreak
\bi
\item{} {\sl The product of two odd integers is odd.}

\medbreak\noindent Equivalently---and more concisely---you want to show that 

\medbreak
\item{} {\sl If $x$ and $y$ are odd integers 
then $xy$ is odd.}
\ei

\medbreak

\noindent Or---even more concisely---you want to prove that 

\begin{equation}\label{topro}
\forall x\in\zz,\forall y\in\zz,(((x\,\,{\rm is\,\,odd})
\wedge(y\,\,{\rm is\,\,odd}))\lto(xy\,\,{\rm is\,\,odd}))\,.
\end{equation}

\noindent To prove this, you can proceed as follows: 

\noindent To prove (\ref{topro}), 
we pick arbitrary $x\in\zz$ and $y\in\zz$, and try to prove that 
\begin{equation}\label{topro-2}
((x\,\,{\rm is\,\,odd})
\wedge(y\,\,{\rm is\,\,odd}))\lto(xy\,\,{\rm is\,\,odd})\,.
\end{equation}

\noindent To prove (\ref{topro-2}), 
we assume that
\begin{equation}\label{topro-3}
(x\,\,{\rm is\,\,odd})\wedge(y\,\,{\rm is\,\,odd})
\end{equation}
and try to prove that 
\begin{equation}\label{topro-4}
xy\,\,{\rm is\,\,odd}\,.
\end{equation}

So let us assume (\ref{topro-3}). Then 
\begin{equation}\label{topro-5}
x\,\,{\rm is\,\,odd}
\end{equation}
and
\begin{equation}\label{topro-6}
y\,\,{\rm is\,\,odd}\,.
\end{equation}
Since $x$ is odd, the definition of ``odd'' tells us that 
\begin{equation}\label{topro-7}
\exists z\in\zz,(x=2z+1)\,.
\end{equation}
Since $y$ is odd, the definition of ``odd'' tells us that 
\begin{equation}\label{topro-8}
\exists w\in\zz,(y=2w+1)\,.
\end{equation}

In view of (\ref{topro-7}), we can pick an integer---call it $a$---such
that 
\begin{equation}\label{topro-9}
x=2a+1\,.
\end{equation}

In view of (\ref{topro-8}), we can pick an integer---call it $b$---such
that 
\begin{equation}\label{topro-10}
y=2b+1\,.
\end{equation}
Then 
$$
xy=(2a+1)(2b+1)=4ab+2a+2b+1=2(2ab+a+b)+1\,.
$$
Therefore, if we let
$$
c=2ab+a+b\,,
$$
we have 
\begin{equation}\label{topro-11}
xy=2c+1\,.
\end{equation}
Moreover,
\begin{equation}\label{topro-12} 
c\in\zz\,,
\end{equation}
because $c=2ab+a+b$, $a\in\zz$, and $b\in\zz$.

In view of (\ref{topro-11})and (\ref{topro-12}), 
\begin{equation}\label{topro-13}
\exists u\in\zz,(xy=2u+1)\,.
\end{equation}
It then follows from the definition of ``odd'' that 
$$
xy\,\,{\rm is\,\,odd}\,.
$$
{\bf END OF PROOF}

\bigbreak\noindent {\bf Is this a truly convincing argument?}

\medbreak\noindent The answer is ``yes'' if all the steps are convincing. 
But {\bf if one step is not convincing, then the whole argument fails.}
(This is why you should {\bf not} expect to get partial credit for a wrong
proof if most steps are O.K. but just a few of them are wrong.  A proof is
like a chain. And {\bf a chain is no stronger than its weakest link.}  If a
16-Ton weight is hanging right above your head, held by a chain, and the
chain breaks because of one weak link, and the weight falls on your head
and kills you, do you think the chain manufacturer should be entitled to
``partial credit'' because ``most links were O.K.; only one broke''?  If
the driver of Lady Diana's car didn't drink every night, but only drank on
the particular night of the accident, should he be entitled to partial
credit because ``after all, most of the time he didn't drink''?)

\bigbreak\noindent So, {\bf are {\mymagtwobf ALL} the steps in the above 
proof truly convincing?}

\medbreak\noindent In the proof, we have given justifications for each
step. For example, at one point we went from ``$x$ is odd'' to
``$\exists z\in\zz,(x=2z+1)$,''  and we said that this was done 
because of the definition of ``odd.'' Now, why is this step permissible?

Suppose I tell you that 

\medbreak\begin{center}\begin{minipage}{10cm}
I don't see how the definition of ``odd'' allows you to do this.
\end{minipage}\end{center}\medbreak

How would you persuade me?   Well, let us give it a try. 
You might say: 

\medbreak\begin{center}\begin{minipage}{10cm}
because the definition of ``odd'' says the following:
an integer $x$ is {\sl odd} provided that 
$\exists z\in\zz,(x=2z+1)$.
\end{minipage}\end{center}\medbreak

\noindent But I could then say

\medbreak\begin{center}\begin{minipage}{10cm}
Fine. We know that ``$x$ is odd,'' and also that 
``$x$ is odd provided that $\exists z\in\zz,(x=2z+1)$.''
How does it follow from these two statements that 
``$\exists z\in\zz,(x=2z+1)$''?
\end{minipage}\end{center}\medbreak

\noindent You would then have to answer something like

\medbreak\begin{center}\begin{minipage}{10cm}
because there is a rule that says that 
if you have a statement $A$, and you also have the statement
``$A$ provided that $B$,'' then you can conclude that $B$.
\end{minipage}\end{center}\medbreak

\noindent (REMARK: The words ``provided that,'' when used in a definition,
mean ``if and only if.'' The ``rule'' you are invoking really says that 
``if you have a statement $A$, and you also have the statement
`$A$ if and only if $B$,' then you can conclude that $B$.'')

Now I could say

\medbreak\begin{center}\begin{minipage}{10cm}
How do I know that this new rule of yours is valid?
\end{minipage}\end{center}\medbreak

What would you answer?

If you are very impatient, you could say 

\medbreak\begin{center}\begin{minipage}{10cm}
{\Large BECAUSE I SAY SO, AND STOP ASKING STUPID QUESTIONS!!!!!!}
\end{minipage}\end{center}\medbreak

But this would be sort of rude, so you might try to reason with me,
and say something like:

\medbreak\begin{center}\begin{minipage}{10cm}
if you have a statement $A$, and you also have the statement
``$A$ if and only if $B$,'' then you can conclude that $B$, for the following 
reason: ``$A$ if and only if $B$'' really means ``if $A$ then $B$ and if $B$
then $A$.'' So if you have ``$A$ if and only if $B$'' then 
you have ``if $A$ then $B$,'' and them, since  you have $A$, you can go
to $B$. {\Large SEE?}
\end{minipage}\end{center}\medbreak

Let us suppose I say 

\medbreak\begin{center}\begin{minipage}{10cm}
No, I don't see!!!  You are telling me that 
``If you have `if $A$ then $B$,' and  you have $A$, then you can go
to $B$.'' {\Large WHY?}
\end{minipage}\end{center}\medbreak

You might try to answer 

\medbreak\begin{center}\begin{minipage}{10cm}
Becase there is a rule called ``Modus Ponens'' that says precisely
that.
\end{minipage}\end{center}\medbreak

Can you guess what my answer would be? Yes, you guessed right!!!
My answer is 

\medbreak\begin{center}\begin{minipage}{10cm}
Oh, another rule!!! You seem to make up a new rule every time
I ask you a question!!! Why is this ``Modus Ponens'' rule of yours 
valid?
\end{minipage}\end{center}\medbreak

A posible answer of yours could be 

\medbreak\begin{center}\begin{minipage}{10cm}
{\Large BECAUSE ANYBODY WHO IS NOT A COMPLETE IDIOT MUST REALIZE
THAT IT IS TOTALLY OBVIOUS THAT IF {\bf A} IS TRUE AND
${\bf A}\lto{\bf B}$ IS TRUE THEN $B$ MUST BE TRUE.!!!!}
\end{minipage}\end{center}\medbreak


Naturally, I would answer 

\medbreak\begin{center}\begin{minipage}{10cm}
{\Large WHY?}
\end{minipage}\end{center}\medbreak

\noindent and then you would give up in despair.

The point I am trying to make should be clear by now: no matter 
how you justify a step in a proof, your justification will be based
on some rule or rules. And then I can always refuse to accept these
rules and ask you to justify them. But your justification of the rules
would have to be based on other rules. And I could 
claim, once again, that I am not convinced of the validity of these rules.  

\medbreak

\begin{center}
\begin{minipage}{10cm}
{\Large IF I WANTED TO,  I COULD GO ON LIKE THIS FOREVER. NO MATTER WHAT
JUSTIFICATION YOU GIVE FOR A STEP OF YOUR PROOF, I COULD ALWAYS ASK:
``WHY IS THAT VALID?'' THEN YOU WOULD GIVE ME A REASON, BUT I COULD 
ASK ``WHY?'' AGAIN. AND SO ON AND ON AND ON.}
\end{minipage}
\end{center}

\medbreak\noindent
In other words, if your opponent is truly stubborn and uncooperative, then
there is {\it nothing} you can do. Maybe you will come up with some reason,
but this reason will be based on some other facts that look obviously true
to you.  But your opponent can still refuse to accept these other facts,
and this process can go on for ever.

\subsection{Why do we need formal proofs?}


To take care of the ``problem of the opponent that doesn't play fair
and refuses to be convinced,'' 
mathematicians have come up with the concept of a {\bf formal proof}.
We give very precise rules defining what a ``formal proof'' is, 
and if you prove something correctly, and strictly following the rules, 
then you are {\it guaranteed} that your proof will be accepted as valid. 

If you do {\it not} obey the rules, then you are on uncertain ground: you
might be able to convince an instructor or grader, but you cannot be sure,
because any time you take a step one of us might ask ``how do you 
justify that step?''

You should think of giving formal proofs as similar to playing a game
such as chess: you are given very strict, precise rules, and you are only
allowed to make moves following the rules. As long as you obey the rules,
your opponent does not have the right to reject your moves. (If your
opponent unilaterally decides that a move of yours is not acceptable,
because ``you are not allowed to move a bishop if in the previous move you
moved a knight,'' then you would say that your opponent is not playing
fair, because this ``rule'' was not in the list of rules that had been
agreed upon before the game started.) 

{\bf In Mathematics we play fair.} We tell you what the rules are, and if
you prove something correctly following the rules, then you can be sure
that it will be accepted.  You may think that having to follow the rules is
a restriction to your freedom. But this is not so.  You should think of it
as {\bf your own protection against unfair play.}  If you correctly justify
every step according to the rules, then we promise you that we will not
change the rules in the middle of the game, kick the board, or come up with
other surprises.

\begin{remark}
\ I said that you should think of giving formal
proofs of theorems as a game similar to chess, in which you are given a
small number of very strict rules telling you which moves are permitted,
and each move has to be justifiable by explaining exactly which rule you
are using and how you are using it.  However, exactly as in the case of
chess, if all you know is the rules, and you always apply the rules
carefully and scrupulously, you may still lose all the time.  If you want
to {\bf win} (that is, in the case of a proof, if you want to get to the
desired conclusion) then you have to {\bf think}. You have to plan a
strategy, make a move now because it will be useful five or six steps
later, etc.

The one big difference between chess and theorem-proving is that {\bf chess
is a zero-sum game}, but {\bf theorem-proving is a cooperative game.} 
What this means is that in chess your opponent wants you to lose,
whereas in theorem-proving you and your opponent are working together,
trying to find out whether something is true, and to understand why.

That's why in chess you don't explain openly why you make a move.  You do
{\sl not} say to your opponent things like: ``I am making this move now so
that then in the next move I can do this other thing, so that three moves
later I can do that, and then I will checkmate you.'' {\sl You don't want your
opponent to be able to figure out your strategy.}

In theorem-proving you definitely {\bf do} want your opponent to understand
your strategy.  Your opponent is going to be ruthless in criticizing you if
you don't obey the rules, but as long as you obey them you will get full
coopertaion. In fact, usually you don't have to go through the whole
business of explaining every detail of every application of every rule.
{\sl As long as you persuade your opponent that something can be done using
the rules, there is no need to go through all the steps and actually do
it.}  And, since your opponent wants to be persuaded, the more you do to 
explain why you are doing something, the better. That's why {\sl in 
theorem-proving it's always nice to explain your strategy, so that your
opponent can understand where you are headed.}    

Because theorem-proving is a cooperative game, when writing proofs it is
always nice to use the first person plural ---the so-called ``editorial
we''--- as we did in our first example of a proof (``we pick,''\ \ ``we are
assuming,''\ \ ``we have shown'').  This is a good way to convey the idea
that the writer and the reader are {\sl working together}, that {\bf the writer
is leading the reader gently along a path of discovery.} \proofend
\end{remark}


\subsection{Proofs keep us honest}

One of the main purposes of giving proofs is {\bf to keep 
ourselves honest}.  Let me explain. Suppose you think a certain
statement ``feels true'' to you. You are just ``convinced''
is is true. You think it must be true. That is very nice, 
except that people who are very convinced of something,
people who have a strong feeling that something must be true, 
are likely to make mistakes. We have seen at least two examples 
of that in this course:

\begin{itemize}
\item[1.] Almost all the students ``proved'' in their homework that
{\em a positive integer which is not prime is composite}.  Yet, this
statement is {\bf false}, and the reason is very simple: the number
$1$ is a positive integer which is not prime, and yet $1$ is not
composite either.  {\large\bf How come nobody noticed (with one exception)? 
And how come almost everybody wrote a ``proof'' and was perfectly happy 
with it? How come nobody had doubts?}
\item[2.] Almost all the students ``proved'' in their homework that
{\em even if one were to change the order of the months of the year, 
it would still be necessarily true that every year must have a Friday
the 13th}.  Yet, this
statement is {\bf false}. I showed you in class how one can reorder
the months so as to produce years that do not have a Friday
the 13th. Once again, you should ask yourself
{\large\bf how come nobody noticed (with a few exceptions)? 
And how come almost everybody wrote a ``proof'' and was perfectly happy 
with it? How come nobody had doubts?}
\end{itemize}

\medbreak\noindent These are just two examples. And, believe me, 
there are going to be quite a few more. In fact, there is a at least
one which is already there in homework you have handed in 
but has not been returned to you yet. 

{\large\bf Why does this happen?} I do not know for sure, but
here is my guess: this is happening to a very large extent because
students are not careful and write just lots of words without making sure
that they do indeed prove anything. For example, in the problem 
of the Friday the 13th, students wrote things like:
{\large\em 
The order of the months does not matter \mbox{because} when you add 
numbers the order in which you add them does not matter.}

Now, to me these words are unitelligible. It is indeed true that
``when you add numbers the order in which you add them does not
matter.'' But, what does this have to do with there being a Friday the
13th?  The student did not tell, and I do not see it.

What can you do about this problem? {\Large\bf Think carefully!!!}

\medbreak

\section{On giraffes, cows, sheep, rabbits, unicorns, elephants, and honesty}

Here is an example of {\bf how carelessness when you write proofs
can lead you to make big big mistakes, and how paying attention to 
the rules can  keep you honest and prevent you from fooling yourself.}

Let us look at the problem on giraffes, cows, sheep, Olivia and
Dolly. (Cf. Part 1 of the notes.)  You were asked 
to prove that ``Olivia is taller than Dolly.'' The correct answer
is {\em it cannot be done; the conclusion that Olivia is taller than Dolly
does {\bf not follow} from the five hypotheses
listed in the problem. If you really want to deduce
from these hypotheses that Olivia is taller than Dolly you need one extra 
fact, which is true but is not one of the statements (1), (2), (3), (4), (5).
Without this fact, it cannot be proved that  Olivia is taller than Dolly.}

I will tell you very soon why this is true, and what the ``extra fact''
is. But before we get there, let us try to prove that Olivia is taller than 
Dolly. I will show you that, if you are really careful, then
you will discover that your ``proof'' does not work, and you really 
cannot prove  that Olivia is taller than Dolly. And, by working 
backwards, you will discover why this is so.

It turns out that {\em nobody} realized that the answer is that
``it cannot be proved that Olivia is taller than Dolly.'' Why did this happen?
Again, I do not know, but my guess is that it happen because
people are just trying to write something, without being careful
about whether what they write is properly justifiable.

Let us set out to prove that Olivia is taller than Dolly, 
and see what happens.

For example, one student wrote: let $x$ bea cow.  Since giraffes are
taller than cows, Olivia is a giraffe, and $x$ is a cow, it follows
that Olivia is taller than $x$. Since cows are taller than sheep, $x$
is a cow, and Dolly is a sheep, it follows that $x$ is taller than
Dolly. So by (3) Olivia is taller than Dolly. 

What is wrong with the above argument?  What is wrong is that the student
introduces a cow and calls the cow $x$, but by the rules
that we have discussed in class quite extensively,
{\bf you are not allowed to introduce an object of a certain 
kind and give it a name unless you have established that such an object
exists.} In this case,  if we want to introduce a cow and call her $x$, 
we need to know that cows exist, that is, that ``$\exists x,x$ is a cow''.


Of course it is true that ``$\exists x,x$ is a cow''.  But this statement
is not in the list of five assertions that you were allowed to use. 
And the question said very clearly that you are allowed to use these five 
statements and nothing else! So the fact that 
``$\exists x,x$ is a cow'' cannot be used, even though it is true.
And if you cannot use that fact there is no way on Earth that 
you can prove that Olivia is taller than Dolly. 


To make this point clearer to you, I then gave you the same 
question, just changing ``giraffes'' to ``rabbits,''
``cows'' to ``unicorns,'' and ``sheep'' to ``elephants.''
{\bf This has exactly the same logical structure as the 
giraffes-cows-sheep problem.}  If you could prove
that Olivia is taller than Dolly, then exactly the same
argument would also prove that Peter is taller than Dumbo!

But  Peter is {\bf not} taller than Dumbo!  (If you proved
that Peter is taller than Dumbo then please ask yourself
``am I really able to prove anything, even things that are obviously
false?'')  Now it should be clearer that the ``proof'' does not work,
because the intermediate step (``let $x$ be a unicorn'') 
is not true, since there are no unicorns!!!

%\input hao2-extrastuff.tex

\section{Proofs}

\subsection{{\bf The structure of a proof}}
\medbreak\noindent Suppose we specify a collection ${\bf H}$ of sentences
called {\bf hypotheses}.  Suppose in addition that we have a collection
${\bf A}$ of sentences declared to be {\bf axioms}, and a collection ${\bf
D}$ of sentences declared to be {\bf definitions}.  Then a {\bf proof under
hypotheses {\bf H}}---under the axioms ${\bf A}$ and the definitions ${\bf
D}$--- is a sequence of {\bf justified steps}, each of which is a sentence
(called the ``assertion'' of---or in---that particular step)
together with a valid justification.

A {\bf proof of a sentence $\mathcal{A}$ under hypotheses {\bf H}}---under
the axioms ${\bf A}$ and the definitions ${\bf D}$--- is a proof under
${\bf A}$ and ${\bf D}$ for which the assertion in the last step is
$\mathcal{A}$.  A {\bf valid justification} for a step is an explanation
showing how the step's assertion is either:

\vspace{-2mm}
\bi
\item{} an axiom,

\vspace{-2mm}
\item{} a definition,

\vspace{-2mm}
\item{} a hypothesis,

\vspace{-2mm}
\item{} a consequence of previous steps by a rule of inference.
\ei

\noindent To complete this definition of ``proof,'' we have to list the 
rules of inference. This will be done  below.

\subsection{{\bf Some examples of rules}}

Before we present the complete list, we show some examples of rules
and  of steps involving them. 

\subsubsection{Modus Ponens}

One of our rules (called ``Modus Ponens,'' or ``$\lto$-out'') 
will say that if you have
two sentences of the form $\mathcal{A}$ and 
$\mathcal{A}\imply\mathcal{B}$, then you can go to
$\mathcal{B}$. 

So, for example, suppose that you are writing a proof, and you
just finished Step 94. Suppose you had the following in Step 25:

\medbreak

\pline{(25)\ste $3>0$, \hfill($\ldots\ldots\ldots\ldots\ldots\ldots\ldots$)}  

\medbreak\noindent and, later, in Step 47:

\medbreak
\pline{(47)\ste $3>0\rightarrow(\exists x,(x^2=3))$. \hfill
($\ldots\ldots\ldots\ldots\ldots\ldots\ldots$)} 

\medbreak\noindent Then you are permitted to add a new step to you proof
(say Step 95), by saying:

\medbreak
\pline{(95)\ste $\exists x,(x^2=3)$. \hfill 
(Modus Ponens,  from (25) and (47)).} 

\subsubsection{The rule for using a conjunction}

Another rule (``Rule $\wedge$-out,'' or the ``rule for using a conjunction'') 
will tell us that if you have a step 
with a sentence of the form  $\mathcal{A}\wedge\mathcal{B}$, 
then you can go to $\mathcal{A}$ and to $\mathcal{B}$.
For example, suppose that at some point 
of a proof  you have 

\medbreak\pline{(238)\ste $3>0\wedge 3<4\,$.\hfill
($\ldots\ldots\ldots\ldots\ldots\ldots\ldots$)} 

\medbreak\noindent Then, if you have just finished Step 454, 
you can write

\medbreak\pline{(455)\ste $3>0$.   
\hfill (By Rule $\wedge$-out, from (238).)}

\noindent or

\medbreak\pline{(455)\ste $3<4$.   
\hfill (By Rule $\wedge$-out, from (238).)}


\subsubsection{The rule for proving a conjunction}

Another rule (``Rule $\wedge$-in,'' or the ``rule for proving a conjunction'') 
will tell us that if you have two steps
with sentences $\mathcal{A}$ and to $\mathcal{B}$, 
then you can go to $\mathcal{A}\wedge\mathcal{B}$.
For example, suppose that in a proof  you have 

\medbreak\pline{(238)\ste $3>0$.\hfill
($\ldots\ldots\ldots\ldots\ldots\ldots\ldots$)} 

\medbreak\noindent and 

\medbreak\pline{(703)\ste $3<4$.\hfill
($\ldots\ldots\ldots\ldots\ldots\ldots\ldots$)} 

\medbreak\noindent Then, if you have just finished Step 40356, 
you can write


\medbreak\pline{(40357)\ste $3>0\wedge 3<4\,$.\hfill
(By Rule $\wedge$-in from (238) and (703).)}

\subsubsection{Universal specialization}

Another rule (``Rule $\forall$-out,'' also 
called the ``rule for using a universal 
\mbox{sentence},'' or ``universal specialization rule'') 
will tell us that if you have a universal sentence---say 
``all elephants have a trunk and tusks''---and a constant---say
``Dumbo''---then you can apply the general statement to the 
special case, and conclude that ``Dumbo has a trunk and tusks.''

For example, suppose that at some point 
of a proof  you have 

\medbreak\pline{(977)\ste $\forall n,(n\in\nn\imply (n+1)^2=n^2+2\cdot n+1)
\,$.\hfill
($\ldots\ldots\ldots\ldots\ldots\ldots\ldots$)} 

\medbreak\noindent Then, if you want to, you can have a later
step 

\medbreak\pline{(1088)\ste $3\in\nn\imply (3+1)^2=3^2+2\cdot 3+10$.   
\hfill (Specialization, plugging in $3$ for $n$ in (977).)}

\subsection{{\bf Proofs within proofs}}

\medbreak\noindent There is one more thing you need to know, which is quite
easy to understand but somehow confuses many people:

\medbreak
\bi
\item{} {\sl Whenever you want, you can start a ``subproof,'' or ``proof 
within
a proof,'' in which you can make {\bf any assumption you want}}.  However,
when you do that then all the things you prove are proved {\bf under that
assumption}.  
\ei

\medbreak\noindent 
For example, suppose we are reading a mystery novel, and I am trying to
prove to you that it was Bob that murdered Bill.  Suppose we got to a point
where I have established that the murderer must have been Bob or John.  Now
I want to convince you that it's not John, so it must have been Bob.

Here is one thing I could say: ``Suppose John murdered Bill.  We know that
Bill's body was found in his house, so the killing must have taken place in
the house itself, or nearby, because even if the body had been moved it
still couldn't have been moved very far. So John must have been in or near
Bill's house at the time of the murder. But Bill was killed on September 8
between 9 and 10 p.m.  EST.  So John must have been in or near Bill's house
on September 8 between 9 and 10 p.m.  EST.  On the other hand, we know that
John gave a public lecture in San Diego on September 8, starting at 6
p.m. Pacific time, i.e.  at 9 p.m. EST. So he must have traveled from New
York to San Diego in one hour or less, which is impossible. So John did not
murder Bill.''

Notice that what we did here is construct, within our main proof that Bob
is the murderer, a ``subproof,'' or ``proof within a proof,'' whose goal is
to prove that John is not the murderer.  We did this by {\sl introducing a
new hypothesis}, namely, by assuming that John is the murderer.  In other
words, {\sl we created and set out to explore an imaginary world}, in which
John did indeed kill Bill, in order to find out what are the consequences
and ramifications of the new hypothesis.  In this imaginary world, we
proved a number of things, such as, for example, that ``John traveled from
New York to San Diego in one hour or less.''  But we proved these things
{\sl under the hypothesis that John killed Bill}.  In order words, we did
not really prove that ``John traveled from New York to San Diego in one
hour or less,'' but only that this must have been so {\sl if John killed
Bill.}

The ultimate consequence of our ``proof within a proof'' is that 
this world we have imagined, in which John killed Bill, is impossible,
because in this world something impossible happened.   So we get out of
this ``proof within a proof'' the conclusion that {\sl John did not kill
Bill}. And {\sl this conclusion no longer depends on the new hypothesis
that ``John killed Bill.''}   The final conclusion, that 
{\sl John did not kill Bill}, is valid {\sl without any extra hypotheses},
so it is part of our main proof.    

In our mathematical formalism, we will be allowed to start a ``proof within
a proof'' any time we want, by assuming anything we want.  However,
anything we prove will only be part of this ``proof within a proof.''
There will be rules telling us how to get out of the ``proof within a proof'' 
and go back to the main proof.  The most important one is the following: 

\medbreak\noindent{{\bf RULE $\lto$-in.}}\ \ (The 
``conditional proof rule,'' also  called ``Rule
$\lto$-in,'' or ``rule for proving an implication.'')
{\sl If assuming $\mathcal{A}$ you get to $\mathcal{B}$,
then you can go, without assuming $\mathcal{A}$, to 
$\mathcal{A}\imply\mathcal{B}$.}

\medbreak For example, suppose that, in some argument you are writing,
you have established that 

\medbreak
\pline{(3591)\ste If Gore wins Florida then Gore will become president.
\hfill($\ldots\ldots\ldots\ldots$)}

\medbreak\noindent and, later, that

\medbreak
\pline{(4507)\ste If Gore becomes president then the next Attorney 
General will not}
\pline{\phantom{(4507)}\ste be a 
conservative.\hfill($\ldots\ldots\ldots\ldots\ldots\ldots\ldots$)}

\medbreak\noindent That means that, if we use the letters 
$\mathcal{A}$, $\mathcal{B}$, $\mathcal{C}$ to represent
the sentences ``Gore wins Florida,'' ``Gore becomes president,'' 
and ``the next Attorney General will not be a
conservative,'' then we already got

\medbreak
\pline{(3591)\ste $\mathcal{A}\imply\mathcal{B}$\,.
\hfill($\ldots\ldots\ldots\ldots\ldots\ldots\ldots$)}

\pline{(4507)\ste $\mathcal{B}\imply\mathcal{C}$\,.
\hfill($\ldots\ldots\ldots\ldots\ldots\ldots\ldots$)}

\medbreak\noindent Suppose you just finished writing 
Step 6812, and now you want to prove
$\mathcal{A}\imply\mathcal{C}$.
Here is one thing you could do:

\medbreak
\pline{(6813)\ste\ste\ste\ste  Assume $\mathcal{A}$.\hfill  
(Preparation to apply Rule $\lto$-in)} 

\pline{(6814)\ste\ste\ste\ste  $\mathcal{B}$.\hfill(Modus Ponens from 
(3591) and  (6813))}

\pline{(6815)\ste\ste\ste\ste  $\mathcal{C}$.\hfill  (Modus Ponens from 
(4507) and (6814))}

\pline{(6816)\ste $\mathcal{A}\imply\mathcal{C}$.\hfill  (Rule $\lto$-in, 
from (6813) and (6815))}

\medbreak\noindent Steps 6813, 6814, 6815 constitute a ``proof
within a proof,'' in which you \mbox{introduce} the new assumption 
$\mathcal{A}$, and under
this assumption you prove first $\mathcal{B}$ and then $\mathcal{C}$. 
Then in Step 6816 you go back to the main proof, using Rule 4.P.  

Notice that we have used extra indentation to indicate that we are writing
a proof within a proof.   The way we have organized our proof makes it
clear that {\sl at no point are we proving $\mathcal{B}$ or 
$\mathcal{C}$}. We are proving $\mathcal{B}$ and $\mathcal{C}$ 
{\em under the assumption $\mathcal{A}$}, from which we can 
conclude that $\mathcal{A}\lto\mathcal{C}$, 
as we do in Step 6816.   For all we know, 
{\em $\mathcal{B}$ and $\mathcal{C}$ could perfectly well be false}, 
and nothing in what we wrote says otherwise.   (Actually,
$\mathcal{B}$ and $\mathcal{C}$ {\em are} false.)
All our ``proof within a proof'' says is that 
{\em if you assume that $\mathcal{A}$ is true, then
$\mathcal{C}$ must be true.}

The ``proof within a proof'' tells us nothing about what happens if
$\mathcal{A}$ is false. And our final conclusion, that 
$\mathcal{A}\rightarrow\mathcal{C}$, is of course valid if 
$\mathcal{A}$ is false, because {\bf an implication such as
$\mathcal{A}\rightarrow\mathcal{C}$ is true when 
$\mathcal{A}$ is false.}



\subsection{Introducing assumptions}

\noindent Let us look at what 
we have just said from a slightly different angle.

{\bf In a proof you can introduce any assumption you want, 
at any time. It does not matter if the assumption is true, of if you 
know whether it is true.}

Students often find this statement shocking, and ask questions
such as ``how can I assume something if I do not know that it 
is true?'' 

The answer is that you can, and in fact you do precisely that
most of the time, but for some mysterious reason when students
write about mathematics they do not believe that the same thing
that they are used to doing in their everyday life is O.K. and works
the same way in mathematics.

In you everyday life, you often imagine some possibility in order to figure
out what would happen if that was the case. For example, 
before the last presidential election you probably tried to imagine
what would happen if Candidate $X$ won, and 
what would happen if Candidate $Y$ won. Then you compared the results
and came to the conclusion that you liked better what would happen
if one of those two candidates won, and decided for that reason to vote for 
that candidate.

To imagine what would happen if Candidate $X$ won, you almost certainly
started thinking along the following lines: ``let me suppose that 
$X$ been elected president; then I guess he would appoint so-and-so
as secretary of state, and this person would probably push 
our foreign policy in sushc-and-such direction, given what I know
about his views.'' And you would have continued like that.

In other words, {\bf you made the assumption that $X$ won without
knowing that it was true, and then you explored its consequences}.

You do the same kind of thing all the time. For example, to decide if
you will go to Restaurant R for dinner, you would try to imagine what
you would eat if you were there, and you might very well end up
concluding that none of the dishes that you can imagine yourself
ordering looks appealing, so in fact you will not go to Restaurant R.
In other words: {\bf you made the assumption that you had gone to
Restaurant R and then concluded that you did not like its 
consequences, so in the end you rendered the assumption}

\begin{center}
\fbox{\fbox{
\begin{minipage}{12cm}

\boxon{HYPOTHESES (A.K.A. ASSUMPTIONS)\label{pigs-box}}

\noindent{\bf Hypotheses}, or {\bf assumptions},
are statements that we {\bf assume} to be true in a particular
situation.

When we discuss proofs later on, we will see that 
that there are certain statements that you are free to bring in any time you want,
because you know them to be true.  (Such statements are called
``axioms,'' or ``postulates.'') In additions, {\em definitions}
function exactly like axioms, the only difference being 
that an axiom is something you {\em accept} as true (say, because 
you are convinced it is true but you do not know how to prove it)
whereas a definition (say, for example, $2=1+1$) is something
that you {\em declare}, or {\em decide} to be true.
{\bf Within a particular proof, hypotheses/assumptions
function exactly like 
axioms and definitions: they are statements that you can bring
in any time.} 

There is, however, a big difference. Axioms and definitions
are things that we take to be
true forever, because we believe they are true. Hypotheses/assumptions
are taken to be
true not because we believe they are true, but {\bf because we want to know
the consequences of their being true.}  

For example: suppose we want to find out what the world would be like
if pigs had wings.  To do this, we first
make the assumption ``pigs have wings,'' by saying

\medbreak\noindent($\ldots$) $\qquad$ Assume that pigs have wings. 

\medbreak Then we would set out to explore the consequences of this 
assumption.
That is, if you prefer, we would set out to study an {\bf imaginary world}
in which pigs have wings, and try to understand what that world would
have to be like. We might then be able to ``prove'' all kind of ``theorems,''
such as

\medbreak THEOREM 1: {\it Pigs can fly}.

\medbreak THEOREM 2: {\it If a pigsty does not have a roof, then the 
pigs will fly away}. 

\medbreak (Proving these theorems might not be easy. For example,
it is not true that ``every animal that has wings can fly,'' since, for example,
ostriches, penguins and dodos do not fly. But you might notice that
all the exceptions to the general rule seem to be birds, so perhaps
you could make a convincing case that 
``every animal that has wings and is not a bird can fly.'' If you manage 
to do that, then you might go on to argue that pigs can fly, since pigs 
clearly are not birds.) 

All these theorems would be proved {\bf under the hypothesis}
that pigs have wings.  That is, we would never be saying that we have
proved that pigs can fly.  All we would be saying is that {\bf IF} pigs
had wings {\bf THEN} pigs could fly.  In other words, all the facts
we would ``prove'' about pigs under the ``pigs have wings'' hypothesis would
be valid {\bf in the imaginary world of pigs with wings}, which, in principle,
is not our real world.
\end{minipage}}}\end{center}

\vbox{\noindent {\bf false by not going to the restaurant.}

In mathematics we do the same thing. We introduce assumptions, 
and then explore their consequences. We do not care if the assumptions
are true, because all we are trying to find out is ``what else
would have to be the case if these assumptions were true?''
}

\medbreak

\begin{center}
\fbox{\fbox{
\begin{minipage}{11cm}
\boxon{ENTERING AND LEAVING IMAGINARY WORLDS}

\noindent As we explained in Box \ref{pigs-box}, when you assume something
you are setting 
out to explore an {\bf imaginary world}, namely, a world in which that thing
you are assuming is true. When can you leave that world and go back to the
real world, taking with you the things you have discovered in your
imaginary world? The answer is simple: if the thing you assumed is actually
true in the real world, then everything you proved {\bf under that
assumption} is true, because in that case the imaginary world really 
is the real world.  

Our rules of inference capture this very obvious idea as follows: 

\bi
\item{} You are always allowed to introduce anything you want as an
assumption, any time you want. 

\item{} When you do that, whatever you have proved will have been proved 
{\bf under your assumption}.

\item{} If, assuming a statement $\mathcal{A}$, you prove some other 
statement $\mathcal{B}$, then you will
be allowed to go back to ``the real world'' and assert there that 
$\mathcal{A}\imply\mathcal{B}$.  

\item{} If, in addition, you can prove $\mathcal{A}$, then the Modus 
Ponens rule allows you to go to $\mathcal{B}$.
\ei

In simpler terms: whatever you prove under the assumption
$\mathcal{A}$ will be valid unrestrictedly (that is, without having to
assume that you are under the assumption $\mathcal{A}$) if you can
also prove $\mathcal{A}$.

\medbreak\noindent EXAMPLE: If you prove that ``pigs can fly''
under the assumption that ``pigs have wings,'' then the conclusion
that ``pigs have wings'' will have been established in a world
where pigs have wings. You can also go back from such an imaginary 
world to the real world by stating that ``if pigs have wings
then pigs can fly.''  This, however, is not enough 
to be able to conclude that in the real world 
pigs can fly, because in the real world you do not know
that pigs have wings, and {\bf if you do not know
that pigs have wings then you cannot go from 
``if pigs have wings then pigs can fly'' to 
``pigs can fly.''}
\end{minipage}}}
\end{center}

\subsubsection{Proofs by contradiction}

Let us start with an example.

\medbreak\noindent{\bf AN EXAMPLE OF A PROOF BY CONTRADICTION:}

\noindent QUESTION: {\sl Prove that the number $30$ cannot be expressed as 
the difference of the squares of two integers.}

\medbreak\noindent PROOF: Suppose $30$ can be expressed as the
difference of the squares of two integers. ({\em Comment: this is a
typical proof by contradiction.  We want to prove Sthat something isn't
true. To do so, we imagine it is true, that is, we explore what things
would be like in an imaginary world where it is true. We then set out
to show that this imaginary world is impossible, because in it
something impossible would have to be true.})  Pick two integers $n$
and $m$ such that $n^2-m^2=30$. Then $(n-m)(n+m)=30$. Now
$n+m=(n-m)+2m$. Therefore $n-m$ and $n+m$ are either both odd or both
even.  If $n-m$ and $n+m$ are both odd then their product, i.e., the
number $30$, would have to be odd. If $n-m$ and $n+m$ are both even
then their product, i.e., the number $30$, would have to be divisible
by $4$.  So $30$ is either odd or divisible by $4$. But this is false,
because $30$ is neither odd nor divisible by $4$. So the assumption that
$30$ can be expressed as the difference of the squares of two integers
leads to an impossible conclusion. Therefore
$30$ cannot be expressed as the difference of the squares of two integers.
\proofend

\medbreak\noindent{\bf ANOTHER EXAMPLE OF A PROOF BY CONTRADICTION:}

\medbreak\noindent QUESTION: {\sl Prove that the number $2$ is not the square
of a rational number.}
(That is, ``prove that $\sqrt{2}$ is irrational.'')

\medbreak\noindent PROOF: Suppose $2$ is the square of a rational number.
This means that $2$ can be expressed as the
quotient of the square of an integer divided by the square of
a nonzero integer. 
Pick two integers $n$
and $m$ such that $2=\frac{n^2}{m^2}$ and $m\neq 0$. Then, after 
cancelling all common factors $>1$, we may assume that 
$n$ and $m$ have no common factors $>1$. In particular, 
$n$ and $m$ are not both even, for if they were both
even then they would have the factor $2$ in common. 
Now, the equality $2=\frac{n^2}{m^2}$ implies 
$2m^2=n^2$. So $n^2$ is even. But then $n$ is even, because
if $n$ was odd then $n^2$ would be odd. So $n=2k$ for some integer $k$.
But then $2m^2=n^2=(2k)^2=4k^2$. So $m^2=2k^2$. So $m^2$ is even.
Then $m$ is even, because
if $m$ was odd then $m^2$ would be odd. 
Therefore $n$ and $m$ are both even, and at the same time
$n$ and $m$ are not both even. These two assertions together
add up to an impossible conclusion. Therefore
$2$ is not the square of a rational number.
\proofend

\begin{center}
\fbox{\fbox{
\begin{minipage}{11cm}
\vspace{1mm}
\begin{center}
\boxon{{\bf PROOFS BY CONTRADICTION}\label{contrad-box}}
\end{center}
One of the most common reasons for assuming something is to prove it
cannot happen. In other words, you set out to explore the consequences
of something in order to prove it is impossible. This is called
``proof by contradiction.'' We have just seen an example: to prove by
contradiction that $30$ cannot be expressed as the difference of the
squares of two integers, we assumed that $30$ could be expressed as
the difference of the squares of two integers,
and ended up with something false,
namely, that $30$ is either odd or divisible by $4$. 
That is, {\bf we set out to explore an imaginary world in which 
$30$ can be expressed as the difference of the squares of two integers,
until we saw that in this world impossible 
things would happen, and then we concluded that such a world could not
exist, so 
$30$ cannot be expressed as the difference of the squares of two integers.}

This should answer once and for all one of the most frequently asked 
students' questions: {\large{\bf How can I assume something if I don't know
it is is true?}} Or, even worse, {\large{\bf how can I assume something if I
know it is not true?}}

The answer is very simple: you assume something that you don't know to be
true because you want to find out what would happen if it was true. 
And often you assume it {\bf precisely in order to prove it is not true.}

\vspace{1mm}
\end{minipage}
}}
\end{center}




\subsection{Introducing arbitrary objects}
A very important way of starting subproofs by introducing
assumptions is to introduce {\em arbitrary objects}. 

This will be useful because there will be a rule
(``Rule $\forall$-in,'' also called ``universal generalization'') telling us
that, if you prove that something is true for an object $a$ 
under the assumption that $a$ is arbitrary, then 
you can conclude that what you proved about $a$ is true {\em for
all} objects.

\begin{example} {\rm Suppose you want to
prove that ``if you take a natural number and add it to its square,
then the result is an even number.'' (Symbolically, 
this is translated as
$$
\forall n,(n\in\nn\imply 2|(n^2+n))\,,\quad\quad\quad
{\rm or}\quad\quad\quad\forall n\in\nn,2|(n^2+n)\,,
$$
or, if it has been stated before that we are working 
in the world of natural numbers, we could just
write $\forall n,(2|(n^2+n))$.)

Then you could say: ``let us pick an {\bf
arbitrary} natural number and let us call it $k$. 
Then $k^2+k=k(k+1)$. So $k^2+k$ is the product of two consecutive
integers. Since one of these two integers must be even,
it follows that $k^2+k$ is even.  So we have proved that
$\forall n(2|n^2+n)$.''

Notice that here we introduced a new letter $k$, which serves as the name
of a number that is {\sl fixed} throughout our analysis, until we get to
the final step, in which we say that, since what we did was O.K.  no matter
what $k$ was, then we have shown that $\forall n(2|n^2+n)$.  
In our ``proof within a proof,'' the letter $k$ is treated as a constant.    

We could organize this as follows:

\medbreak\noindent 
\pline{(***)\ste\ste  Let $k\in\nn$ be arbitrary.\hfill
(Preparation to apply Rule $\forall$-in)} 

\centerline{$\vdots\qquad\qquad\qquad\qquad\qquad\qquad$}

\pline{(!!!)\ste\ste \ $k^2+k$ is even.\hfill
(\ $\cdots\cdots\cdots\cdots$\ )}

\pline{(\$\$\$)\ste $\forall n\in\nn,(n^2+n\,\,{\rm is\,\,even})$.
\hfill (Rule $\forall$-in, from (***) and (!!!))}

\medbreak\noindent or


\medbreak\noindent 
\pline{(***)\ste\ste  Let $k$ be arbitrary.\hfill
(Preparation to apply Rule $\forall$-in)} 

\pline{(\&\&\&)\ste\ste\ste  Assume $k\in\nn$.\hfill
(Preparation to apply Rule $\lto$-in)} 

\pline{\phantom{(\&\&\&)}\ste\ste\ste\ste  \phantom{Assume}$\vdots$
\phantom{$k\in\nn$.}} 


\pline{(!!!)\ste\ste\ste\ste $k^2+k$ is even.\hfill
(\ $\cdots\cdots\cdots\cdots$\ )}

\pline{(\$\$\$)\ste\ste $k\in\nn\imply(k^2+k\,\,{\rm is\,\,even})$.
\hfill (Rule $\lto$-in, from (\&\&\&) and (!!!))}


\pline{(\%\%\%)\ste $\forall n,(n\in\nn\imply(n^2+n\,\,{\rm is\,\,even}))$.
\hfill (Rule $\forall$-in, from (***) and (\$\$\$))}


}\end{example}


\noindent {\bf
When we start a subproof by introducing a letter by saying ``let such
and such be arbitrary,'' then this has automatically the \mbox{effect}
of declaring that letter to be a constant for this subproof.} But,
{\bf this declaration is ``local,'' that is, valid within the subproof
only.  Once the subproof is finished, then the effect of this
declaration is undone.}

\subsection{{\bf The basic logical rules for proofs}}

\medbreak\noindent Let us first review our conditions telling us 
when a step in a proof is valid. 

\vspace{-2mm}
\bi
\item[(P.a)] It is always permitted to bring in an 
{\it axiom} (or ``postulate'') as a new step.

\vspace{-2mm}
\item[(P.b)] It is always permitted to bring in a {\it definition}
as a new step. 

\vspace{-2mm}
\item[(P.c)] It is always permitted to bring in one of the {\it hypotheses}
as a new step.

\vspace{-2mm}
\item[(P.d)] It is always permitted to bring in as a new step
something that follows from previous steps by applying a valid {\it rule of
inference}.

\vspace{-2mm}
\item[(P.e)] It is always permitted to start a proof within a proof
by introducing any sentence you want  as an assumption, and in particular
to bring in a {\bf new} letter as an arbitrary constant.  However, 
whatever is proved 
after this is done, is only valid in the ``proof within a proof'', and one
can only get out of it by applying one of the rules
that allow you to get out of a subproof (that is, Rules
 1.P, 1.U, 3.P, 6.P, 7.U).
\ei

And here, finally,  are the basic rules of inference.

\noindent$\!\!\!$\fbox{\fbox{\begin{minipage}{13cm}
\boxon{THE BASIC LOGICAL RULES\label{logic-box}}

{\small
\baselineskip=6pt

\vspace{-2.5mm}
\rulonn{T}  You are allowed to bring in any statement which is
an instance of a tautology.
(This is called the ``tautology proof rule.'')

\vspace{-1.5mm}
\rulonn{$\neg$-in} Let $\mathcal{A}$ and $\mathcal{B}$ be sentences. 
If you have started a subproof $P'$ of a proof $P$ with ``Assume
$\mathcal{A}$'' and have obtained $\mathcal{B}$ in a step of $P'$, 
and $\mathcal{B}$ is a contradiction, then you can get out of $P'$
and go to $\neg\mathcal{A}$ in $P$. 
(This is the ``rule for proving a negation,'' and is one of several 
rules of ``proof by contradiction.'')

\vspace{-1.5mm}
\rulonn{$\neg$-out} Let $\mathcal{A}$ and $\mathcal{B}$ be sentences. 
If you have $\neg\mathcal{A}$ in a step of your proof, and then
you start a subproof $P'$ of your proof $P$ with ``Assume
$\mathcal{B}$'' and obtain $\mathcal{A}$ in a step of $P'$, 
then you can get out of $P'$ and go to $\neg\mathcal{B}$ in $P$. 
(This is another version of the ``rule of proof by contradiction.'')

\vspace{-1.5mm}
\rulonn{$\wedge$-in} \ Let $\mathcal{A}$ and $\mathcal{B}$ be sentences. 
If you have $\mathcal{A}$ and $\mathcal{B}$ in previous steps,
then you can go to $\mathcal{A}\wedge\mathcal{B}$.
(This is called the ``rule for proving a conjunction.'')

\vspace{-1.5mm}
\rulonn{$\wedge$-out} \ Let $\mathcal{A}$ and $\mathcal{B}$ be sentences. 
If you have $\mathcal{A}\wedge\mathcal{B}$ in a previous step,
then you can go to $\mathcal{A}$ and you can also 
go to $\mathcal{B}$.
(This is called the ``rule for using a conjunction.'')

\vspace{-1.5mm}
\rulonn{$\vee$-in} 
Let $\mathcal{A}$ and $\mathcal{B}$ be sentences. If you have 
$\mathcal{A}$ in a previous step,
then you can go to $\mathcal{A}\vee\mathcal{B}$.If you have 
$\mathcal{B}$ in a previous step,
then you can go to $\mathcal{A}\vee\mathcal{B}$.
(This is the ``rule for proving a disjunction.'')

\vspace{-1.5mm}
\rulonn{$\vee$-out} Let $\mathcal{A}$, $\mathcal{B}$,  $\mathcal{C}$,
be sentences. If you have 
$\mathcal{A}\vee\mathcal{B}$,  
$\mathcal{A}\imply\mathcal{C}$,
and $\mathcal{B}\imply\mathcal{C}$,
in previous steps, then you can go to $\mathcal{C}$.
(This is the ``rule for using a disjunction,''
or ``rule of proof by cases.'')

\vspace{-1.5mm}
\rulonn{$\lto$-in} Let $\mathcal{A}$ and $\mathcal{B}$ be sentences. 
If you have 
started  a subproof $P'$ of a proof $P$ with ``Assume $\mathcal{A}$''
and have obtained $\mathcal{B}$ in a step of $P'$, 
then you can get out of $P'$ and go to
$\mathcal{A}\imply\mathcal{B}$ in $P'$.
(This is the ``rule for proving an implication,''
or ``conditional proof rule.'')

\vspace{-1.5mm}
\rulonn{$\lto$-out} Let $\mathcal{A}$ and $\mathcal{B}$ be sentences. 
If you have $\mathcal{A}$ and $\mathcal{A}\rightarrow\mathcal{B}$ 
in previous steps, then you can go to $\mathcal{B}$. 
(This is the ``rule for using an implication,''
or ``modus ponens.'')

\vspace{-1.5mm}
\rulonn{$\iff$-in} Let $\mathcal{A}$ and $\mathcal{B}$ be sentences. 
If you have 
$\mathcal{A}\imply\mathcal{B}$ and $\mathcal{B}\imply\mathcal{A}$ in
previous steps then you can go to
$\mathcal{A}\iff\mathcal{B}$ in your proof.
(This is called the ``rule for proving a biconditional.'') 

\vspace{-1.5mm}
\rulonn{$\iff$-out} Let $\mathcal{A}$ and $\mathcal{B}$ be sentences. If
you have 
$\mathcal{A}\iff\mathcal{B}$ in a previous step then you can go to
$\mathcal{A}\imply\mathcal{B}$, and also to $\mathcal{B}\imply\mathcal{A}$,
in your proof.
(This is called the ``rule for using a biconditional.'') 

\vspace{-1.5mm}
\rulonn{$\forall$-in} Suppose that

\vspace{-1.5mm}
\begin{itemize}
\item[S1.] $x$ is a variable and $\mathcal{A}(x)$ is a formula where there 
is no quantifier involving $x$, 

\vspace{-1.5mm}
\item[S2.] $a$ is a constant and $\mathcal{A}(a)$ is what you get from 
$\mathcal{A}(x)$ 
by substituting $a$ for $x$ in {\bf all} the occurrences of $x$ in
$\mathcal{A}(x)$.
\end{itemize}

\vspace{-3mm}\noindent Suppose you are in a proof $P$ (which may be itself
be a subproof of some other proof) and you have started a subproof $P'$ of $P$
by saying ``Let $a$ be arbitrary,'' and that until that point
$a$ had never appeared in $P$.  Suppose that in $P'$
you got to $\mathcal{A}(a)$. Then you can get
out of $P'$ and go to $\forall x,\mathcal{A}(x)$ in $P$.
(This the ``rule for proving a universal statement,'' or
``universal generalization rule.'')

\vspace{-1.5mm}
\rulonn{$\forall$-out} Suppose S1, S2 are true.
Then, if you have $\forall x,\mathcal{A}(x)$ in a previous step,
you can go to $\mathcal{A}(a)$. (This is the ``rule
for using a universal statement,'' or ``universal specialization rule.'')

\vspace{-1.5mm}
\rulonn{$\exists$-in}  Suppose S1, S2 are true.
Suppose you got $\mathcal{A}(a)$ in a previous 
step. Then you can go to $\exists x,\mathcal{A}(x)$.  
(This is the ``rule for proving an existential statement,
or ``existential generalization rule.'')

\vspace{-1.5mm}
\rulonn{$\exists$-out} Suppose S1, S2 are true.  Suppose you have started a
subsubproof $P''$ within a proof $P$ by saying ``Let $a$ be
arbitrary,'' and ``Assume $\mathcal{A}(a)$.'' Suppose that until that
point $a$ had never appeared in $P$.  Suppose that in $P''$ you got to
$\mathcal{B}$, where $\mathcal{B}$ is a sentence that does not contain
the constant $a$. Suppose that in a previous step of $P$, before you
started $P''$, you had $(\exists x,\mathcal{A}(x))$.  Then you can get
out of $P''$ and go to $\mathcal{B}$ in $P$.  (This is the ``rule for
using an existential statement, or ``existential specification
rule.'')}
\end{minipage}}}

\begin{center}
\fbox{
\fbox{\begin{minipage}{13cm}
\begin{center}
\begin{minipage}{12cm}
\noindent{\Large That's it. These are {\bf all} the rules
of inference.

%\medbreak 
There are exactly {\bf fifteen} rules.  Only fifteen!!!!}

\end{minipage}\end{center}\end{minipage}}}
\end{center}

\subsection{{\bf Some comments on the logical rules}}

There are fifteen rules. Maybe you think this is too much, and that
remembering $15$ rules requires a lot of effort on your part.  I will
show you now that this is not so, because {\bf the rules of Box
\ref{logic-box} are just plain common sense, so you should have no
difficulty understanding them and remembering them}.

Actually, there is no need to have $15$ rules. The number of rules can
be cut down a lot, because several of the rules in Box \ref{logic-box}
are really not needed. On the other hand, having these $15$ rules
makes it much easier to write proofs than if you had fewer rules.
(In many cases, our rules enable you to do in one step
what might require five or six steps without using the rule.)

Let us notice that the rules obey a nice simple pattern.  In addition
to the ``tautology rule'' (i.e., Rule $0$), our rules are neatly
organized into seven pairs consisting of two rules each. The seven
pairs correspond to the {\bf seven logical connectives}:
$$
\neg\qquad\qquad\wedge\qquad\qquad\vee\qquad\qquad
\imply\qquad\qquad\iff\qquad\qquad\forall\qquad\qquad\exists\qquad.
$$

Remember that {\bf every mathematical 
sentence is of one and only one of the following eight types}:

\begin{itemize}

\vspace{-2.2mm}
\item{} negation (``not'', i.e, ``$\neg$''), 

\vspace{-2.2mm}
\item{} conjunction (``and'', i.e, ``$\wedge$''), 

\vspace{-2.2mm}
\item{} disjunction (``or'', i.e, ``$\vee$''), 

\vspace{-2.2mm}
\item{} implication (``implies'', or ``if $\ldots$ then'', i.e, 
``$\imply$''), 

\vspace{-2.2mm}
\item{} biconditional (``if and only if'', i.e, ``$\iff$''), 

\vspace{-2.2mm}
\item{} universal (``for all'', i.e, ``$\forall$''), 

\vspace{-2.2mm}
\item{} existential (``for some'', or ``there exists $\ldots$ such that'',
i.e, ``$\exists$''),

\vspace{-2.2mm}
\item{} atomic.
\end{itemize}

\medbreak\noindent {\em Atomic sentences} (for example, $2+2=4$)
cannot be analyzed into smaller parts put together by logical connectives.
This means that if you want to prove or use an atomic sentence
you need to do mathematics, rather than pure logic.  The main part
of the course will be devoted to the mathematics, but at this point we are 
concentrating on the logical part. That is why we are presenting
rules that tell us how to work with non-atomic sentences
and use their logical structure to figure out how to use them
and how to prove them.

As we indicated before, all the rules other than 
Rule T come in pairs of two rules each. There are seven such pairs,
one for each of the seven logical \mbox{connectives}. For each connective,
there are two rules. One rule (the ``in'' rule) tells you how to {\em get
to} a sentence $S$ (i.e. how to {\em prove} $S$)
if the logical form of $S$ is that of the corresponding connective. 
The other rule (the ``out'' rule) tells you how to {\em get out}
of a  sentence $S$ (i.e. how to {\em use} $S$) 
if the logical form of $S$ is that of the corresponding connective. 


Now let us look at the rules one at a time, and show that they are no
more than plain common sense.	

\subsubsection{The tautology proof rule}

Rule T just tells us that you are always allowed to bring in 
instances of tautologies. {\em Why is this reasonable?}
Because {\bf instances of tautologies 
are always true}, so it is perfectly reasonable
to allow yourself to bring them in any time you want.

\subsubsection{Proofs by contradiction}

Rules $\neg$-in and $\neg$-out enable us to do {\bf proofs by
contradiction}. How does a proof by contradiction work? 

Let us say you want to prove that a statement $\mathcal{S}$ is false, i.e.,
that you want to prove $\neg S$. To do that, {\bf assume that $\mathcal{S}$
is true and try to get to something that you can be sure is false}.

This can be done in two ways. One way is to {\bf get a to a
contradiction}. This works, because a contradiction is false for sure. Rule
$\neg$-in just says that if you get to a contradiction by assuming
$\mathcal{S}$, then you can go to $\neg\mathcal{S}$. {\em Why is this
reasonable?}  Because if assuming $\mathcal{S}$ you derive a contradiction
then $\mathcal{S}$ cannot be true, since if $\mathcal{S}$ was true it would
follow that the contradiction is true.

Another way is to proceed as in Rule $\neg$-out. That is, you assume that
$\mathcal{S}$ is true and try to prove, under that assumption, a statement
$\mathcal{A}$ that has been proved to be false in a previous step.  Then
you can conclude $\neg\mathcal{S}$ again.


\begin{remark}
{\bf Proofs by contradiction are used all the time.} When you have to
prove something, you should always seriously consider the possibility of
doing your proof by contradiction. 

Here is the main reason. Suppose you know several things, say for example
you know five statements $\mathcal{A}$, $\mathcal{B}$, $\mathcal{C}$,
$\mathcal{D}$, $\mathcal{E}$. Suppose you are asked to prove some other
statement, say $\mathcal{E}$. If you try a ``direct proof'' (that is, a
proof which is not by contradiction) then you have five statements you can
use, namely $\mathcal{A}$, $\mathcal{B}$, $\mathcal{C}$, $\mathcal{D}$, and
$\mathcal{E}$, and from these statements you have to work your way 
to $\mathcal{S}$. Suppose instead that you do a proof by contradiction. 
You do this by saying ``let me assume $\neg\mathcal{S}$ and see 
what happens.''  Now you have {\em six} things that you can use, namely,
$\mathcal{A}$, $\mathcal{B}$, $\mathcal{C}$, $\mathcal{D}$, 
$\mathcal{E}$, and $\mathcal{S}$. So you have more room to manoeuvre, 
and you can do more things.   

{\bf A piece of advice:} {\Large\bf Most of your proofs should be by
contradiction}.  When you have to prove something and you do not 
know what to do, the best strategy is to 
try saying ``let me imagine that what I want to prove was false, and let
me see what would have to happen.''  \proofend
\end{remark}


\subsubsection{The rules for conjunction and disjunction}

These rules are fairly trivial, so let me just go over them quickly.

Rule $\wedge$-in tells us how to prove a conjunction. It is a reasonable
rule because it is obvious that if you know that two things are true then
you can conclude that their conjunction is true.

Rule $\wedge$-out tells us how to make use of a conjunction: if you know
that the conjunction of two things is true then you can conclude that each
one of them is true.

Rule $\vee$-in gives us a way to prove a
disjunction: to prove that the disjunction of two things is true,
prove one of them. 

Rule $\vee$-in gives us a way to prove a
disjunction: to prove that the disjunction of two things is true,
prove one of them. 

Rule $\vee$-out is the ``rule of proof by cases.'' It says that,
if we want to conclude $\mathcal{C}$ and
we know $\mathcal{A}\wedge\mathcal{B}$, then we consider the case
when $\mathcal{A}$ is true, and then the case when $\mathcal{B}$ is true,
and show that in each case $\mathcal{C}$  must be true. 

\medbreak\noindent EXAMPLE: suppose I tell you that 
``Karl was born is Oslo or in Stockholm. I don't know in which city,
exactly,  but I know it was one of those two. Is true that Karl is
Scandinavian?''  Then you could argue as follows:

\medbreak
\pline{(1) Karl was born in Oslo $\vee$ Karl was born in Stockholm.
\hfill[Given]}

\pline{(2) \ste Assume Karl was born in Oslo.\hfill[Preparation to apply
Rule $\lto$-in]}

\pline{(3) \ste Oslo is in Norway.\hfill[$\ldots$]}

\pline{(4) \ste Norway is a Scandinavian country.\hfill[$\ldots$]}

\pline{(5) \ste Karl was born in a Scandinavian country.\hfill[$\ldots$]}

\pline{(6) \ste Karl is Scandinavian.\hfill[$\ldots$]}

\pline{(7) Karl was born in Oslo $\lto$ Karl is Scandinavian.\hfill}

\pline{\hfill [Rule$\lto$-in, from (2) and (6)]}

\pline{(8) \ste Assume Karl was born in Stockholm.\hfill}

\pline{\hfill[Preparation to apply Rule $\lto$-in]}

\pline{(9) \ste Stockholm is in Sweden.\hfill[$\ldots$]}

\pline{(10) \ste Sweden is a Scandinavian country.\hfill[$\ldots$]}

\pline{(11) \ste Karl was born in a Scandinavian country.\hfill[$\ldots$]}

\pline{(12) \ste Karl is Scandinavian.\hfill[$\ldots$]}

\pline{(13) Karl was born in Stockholm $\lto$ Karl is Scandinavian.\hfill}

\pline{\hfill[Rule$\lto$-in, from (2) and (6)]}

\pline{(14) Karl is Scandinavian.\hfill[Rule $\wedge$-out, from (1),
(7) and (12)}

\pline{{\bf END OF PROOF.}\hfill}



\subsubsection{The rules for implication}


Rule $\lto$-in gives us a way to prove an
implication: to prove $\mathcal{A}\imply\mathcal{B}$, 
assume $\mathcal{A}$ and prove $\mathcal{B}$.  (When you 
``assume $\mathcal{A}$'' you enter a new level of ``proof within 
a proof,'' as was explained before.)


Rule $\lto$-out is called ``Modus Ponens,'' and 
is one of the most important
of all the rules. It is an ``out'' rule. It gives us a way to put to use
an implication  $\mathcal{A}\imply\mathcal{B}$. If you manage 
in addition to prove  $\mathcal{A}$, then the rule
tells you that you can go to $\mathcal{B}$. 

\subsubsection{The rules for the biconditional}

Rule $\iff$-in tells us that you can 
prove a biconditional of the form 
$\mathcal{A}\iff\mathcal{B}$ by proving 
$\mathcal{A}\imply\mathcal{B}$ and $\mathcal{B}\imply\mathcal{A}$. 

Rule $\iff$-out is a trivial ``out'' rule. It tells us that if 
you have a biconditional $\mathcal{A}\iff\mathcal{B}$ then you can
use it by concluding from it the implications 
$\mathcal{A}\imply\mathcal{B}$ and $\mathcal{B}\imply\mathcal{A}$. 

\subsubsection{The rules for the universal quantifier}

Rule $\forall$-in gives us a way to prove a
universal statement: to prove that some statement $S$ is true for all
possible values of the variable $x$,
pick an arbitrary object, call it $a$, and prove that
$S$ is true of $a$.

Rule $\forall$-out---the universal  specialization rule---is an ``out'' 
rule. It
is extremely easy to understand, and the name is easy to remember. The
rule basically says: if you know that something is true for all
things, then you can plug in any particular thing and you will get a
true statement.  (For example: if you know that ``everybody is smart''
you can conclude that ``Alice is smart.'') The name {\em
specialization} comes from the fact that in going from $\forall 
x,\mathcal{A}(x)$ to $\mathcal{A}(a)$, you are going from a {\em
general statement} (for example, ``all people are smart'') to a {\em
special case} (``Alice is smart'').

\subsubsection{The rules for the existential quantifier}

Rule $\exists$-in  gives us a way to prove an
existential statement: to prove that 
$\exists x,\mathcal{A}(x)$, exhibit an $a$ such that
$\mathcal{A}(a)$. (Such as $a$ is called a {\bf witness}
for $\exists x,\mathcal{A}(x)$.)

Finally, Rule $\exists$-out is another ``out'' rule which just reflects 
plain common sense. All it says is that
if you know that there exists an object of a certain kind, then you can 
introduce one such object and give it a name.

The most common way you would apply this rule is this. Say you
are trying to prove $\mathcal{B}$ and you know that 
$\exists x,\mathcal{A}(x)$.  Then you would say ``since I know that there
exists an $x$ such that $\mathcal{A}(x)$, let me pick one and call it
$a$.'' You could do that by starting a subproof with ``Let $a$ be
arbitrary,'' and then a subsubproof with ``Assume $\mathcal{A}(a)$.''
Suppose you then work your way to $\mathcal{B}$. Then you can get out
of the subsubproof and land in the proof with
$\mathcal{B}$.

{\bf It is very important that the new object $a$ be given a
name that has not been used before.} For example, suppose 
``$\mathcal{A}(x)$'' stands for ``$x$ killed Polonius,'' and we are told
that $\exists x,\mathcal{A}(x)$, i.e., that somebody killed
Polonius. Then you can introduce a name for this individual.  You
can call him/her $a$ or, if you prefer, ``the killer,'' in which case you
would be able to say that ``$\mathcal{A}(a)$'' 
or that ``$\mathcal{A}({\rm the\,\,killer})$.''  But you
cannot say ``let's call this person Hamlet,'' or ``let's call him
Laertes,'' because Hamlet and Laertes are names of characters that have
already appeared in the play. If you call the killer ``Hamlet'' or
``Laertes'' then you would be {\it prejudging}, and declaring that 
$\mathcal{A}({\rm Hamlet})$, i.e. that Hamlet killed Polonius, or that 
$\mathcal{A}({\rm Laertes})$,
i.e. that Laertes killed Polonius. One of these happens to be true, and the
other one is false, but in either case you cannot just conclude that it is
true by merely choosing a name for the killer.)

{\bf Also, notice that the rule only allows you to conclude that 
$\mathcal{B}$ holds if you know that 
$\exists x,\mathcal{A}(x)$.} If you do not know that
such an $x$ exists, then you cannot do anything with the rule, and in 
particular you cannot get to $\mathcal{B}$.

For a typical example of the kind of outrageous mistakes
that one can make by failing to pay attention to the requirement
that you must know that $\exists x,\mathcal{A}(x)$, look carefully
at the Peano paradox, described in Box No. \ref{peano-box} below.
{\bf Make sure you understand and can explain what is wrong
with that proof.}

\begin{center}
\fbox{\fbox{
\begin{minipage}{11cm}
\vspace{1mm}
\begin{center}
\boxon{{\bf THE PEANO PARADOX}\label{peano-box}}
\end{center}

Here is a ``theorem'' that is obviously false:


\medbreak
THEOREM: {\em $1$ is the largest natural number}. 
 
\medbreak\noindent
And here is a ``proof'':

\medbreak PROOF: Let $n$ be the largest natural number. Then $n^2$ is a 
natural number too.  Since $n$ is the largest natural number, $n^2\le n$. 
On the other hand, $n^2\ge n$. (Proof by cases: either 
$n\ge 1$ or $n=0$. If $n\ge 1$ then
so $n^2=n.n\ge n.1=n$. So $n^2\ge n$. If $n=0$ then 
$n^2=0$, so $n^2=n$ and then $n^2\ge n$.)
Therefore $n^2=n$. The only solutions $x$ of $x^2=x$ are 
$x=1$ and $x=0$.  So $n=1$ or $n=0$. But $n$ is the largest natural number,
so $n$ cannot be $0$ because $1>0$. Therefore $n$ has to be equal to 
$1$. {\bf QED}

\medbreak WHAT IS WRONG WITH THIS ``PROOF''?  The mistake occurs
in the very first sentence, ``let $n$ be the largest natural number.''
{\large\em This step is not permissible, because we do not know that
there exists a ``largest natural number.''}  The author must have
been thinking of appliyng Rule $\exists$-out here. But the rule
only allows to introduce an object of a certai kind 
{\em if you know that one 
such an object exists.}

\end{minipage}
}}

\end{center} 

\subsection{An example of an almost completely formal proof}

The definition of the empty set says:
$$
\forall x,(\neg x\in\emptyset)\,.
$$
(That is, ``nothing belongs to the empty set.'')

The definition of {\em set inclusion} says that if $X$, $Y$ are sets
then
$$
X\subseteq Y\iff(\forall x,(x\in X\imply x\in Y))\,.
$$
(That is, ``$X$ is a subset of $Y$ if and only if 
every member of $X$ belongs to $Y$.'')

Using these two definitions plus our logical rules, let us give a completely
formal proof of the following.

\begin{theorem}
If $A$ is any set then $\emptyset\subseteq A$.
\end{theorem}

\medbreak\noindent{\bf PROOF:}

\medbreak
\pline{\ (1) \ste $\forall x,(\neg x\in\emptyset)$.\hfill[Definition
of $\emptyset$]}

\pline{\ (2) \ste\ste Let $a$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\pline{\ (3) \ste\ste\ste Assume $a\in\emptyset$.\hfill[Preparation to apply 
Rule $\lto$-in]}

\pline{\ (4) \ste\ste\ste\ste Assume $\neg a\in A$.\hfill[Preparation to apply 
Rule $\neg$-out]}

\pline{\ (5) \ste\ste\ste\ste $\neg a\in\emptyset$.\hfill[Rule $\forall$-out, 
plugging $a$ for $x$ in (1)]}

\pline{\ (6) \ste\ste\ste\ste $a\in\emptyset\wedge(\neg a\in\emptyset)$.\hfill
[Rule $\wedge$-in, from (3) and (5)]}

\pline{\ (7) \ste\ste\ste $\neg(\neg(a\in A))$.\hfill[Rule $\neg$-out, from
(4) and(6),}


\pline{\hfill 
since $a\in\emptyset\wedge(\neg a\in\emptyset)$ is a contradiction]}

\pline{\ (8) \ste\ste\ste $(\neg(\neg(a\in A)))\imply a\in A$.
\hfill[Rule T]}

\pline{\ (9) \ste\ste\ste $a\in A$.\hfill[Rule $\lto$-out, from (7) and (8)]}

\pline{(10) \ste\ste $a\in\emptyset\imply a\in A$.\hfill[Rule
$\lto$-in, from (3) and (9)]}

\pline{(11) \ste $\forall x,(x\in\emptyset\imply x\in A)$.\hfill
[Rule $\forall$-in, from (2) and (10)]}

\pline{(12) \ste $\emptyset\subseteq A\iff
(\forall x,(x\in\emptyset\imply x\in A))$.\hfill[Definition of 
$\subseteq$]}

\pline{(13) \ste $(\forall x,(x\in\emptyset\imply x\in A))\imply
\emptyset\subseteq A$.\hfill[Rule $\iff$-out, from (12)]}

\pline{(14) \ste $\emptyset\subseteq A$.\hfill[Rule $\lto$-out, from (11) 
(13).]}

\pline{{\bf END OF PROOF}\hfill}

\subsection{An example of a completely formal proof}\label{exacom}


The previous example was ``almost completely formal'' 
but something was still missing: we had not  formalized
the definitions of ``empty set'' and ``subset.'' Now let us write
down these definitions in formal language, and give a completely 
formal proof of the statement of the previous section. 

Furthermore, we have not been careful about specifying the ranges
of our variables. Are there things other than sets, or is everything is a 
set? This is important because, for example, if we want to characterize
the empty set $\emptyset$ by saying $\forall x,(\neg x\in\emptyset)$ 
(that is, ``nothing belongs to $\emptyset$'') then this does not tell us that
$\emptyset$ is a set. If everything is a set, then this is no problem.
But if we work in universe where there are sets as well as other things
that are not sets, then if we want to guarantee that 
$\emptyset$ is a set we have to say it.  This leads us to the 
following formula, which you can regard as the definition of the empty set,
or as an axiom characterizing the empty set, as you prefer:
\begin{equation}\label{defempty}
\emptyset\,\,{\rm is\,\,a\,\,set}\wedge\forall x,(\neg x\in\emptyset)\,.
\end{equation}
(That is, ``nothing belongs to the empty set.'')

\medbreak
The definition of {\em set inclusion} says that if $X$, $Y$ are sets
then $X$ is a subset of $Y$ if and only if  
every member of $X$ belongs to $Y$.  In other words, 

\medbreak\noindent FORMAL DEFINITION OF ``SUBSET'' IN A UNIVERSE WHERE THERE 
ARE SETS AND OTHER THINGS:
$$
\forall X,\forall Y,((X\,\,{\rm is\,\,a\,\,set}\wedge
Y\,\,{\rm is\,\,a\,\,set})\lto(X\subseteq Y\iff
(\forall x,(x\in X\imply x\in Y))))\,.
$$


Using these two definitions plus our logical rules, let us give a completely
formal proof of the following.

\begin{theorem}
If $X$ is any set then $\emptyset\subseteq X$.
\end{theorem}


\medbreak\noindent{\bf PROOF:}

\medbreak
\noindent{\em Comment}: we have to prove that 
``$\forall X,(X\,\,{\rm is\,\,a\,\,set}\lto\emptyset\subseteq X)$.''

\medbreak
\pline{\ (1) $\forall X,\forall Y,((X\,\,{\rm is\,\,a\,\,set}\wedge
Y\,\,{\rm is\,\,a\,\,set})\lto$\hfill}

\pline{\hfill$(X\subseteq Y\iff
(\forall x,(x\in X\imply x\in Y))))$\hfill[Definition of set inclusion]}

\pline{\ (2) $\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
\forall x,(\neg x\in\emptyset)$.\hfill[Definition
of $\emptyset$]}

\pline{\ (3) $\emptyset\,\,{\rm is\,\,a\,\,set}$.\hfill
[Rule $\wedge$-out, from (2)]}

\pline{\ (4) $\forall x,(\neg x\in\emptyset)$.\hfill
[Rule $\wedge$-out, from (2)]}

\pline{\ (5) \ste Let $A$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we want to prove that 
``$A\,\,{\rm is\,\,a\,\,set}\lto\emptyset\subseteq A$.''

\medbreak
\pline{\ (6) \ste\ste Assume $A$ is a set. \hfill[Preparation to apply 
Rule $\lto$-in]}

\medbreak
\noindent{\em Comment}: we want to prove that ``$\emptyset\subseteq A$.''

\medbreak
\pline{\ (7) \ste\ste $\forall Y,((\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
Y\,\,{\rm is\,\,a\,\,set})\lto(\emptyset\subseteq Y\iff$\hfill}

\pline{\hfill $(\forall x,(x\in \emptyset\imply x\in Y))))$\hfill
[Rule $\forall$-out, from (1), specializing $X$ to $\emptyset$]}

\pline{\ (8) \ste\ste $(\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
A\,\,{\rm is\,\,a\,\,set})\lto(\emptyset\subseteq A\iff
(\forall x,(x\in \emptyset\imply x\in A)))$\hfill}

\pline{ \hfill
[Rule $\forall$-out, from (7), specializing $Y$ to $A$]}

\pline{\ (9) \ste\ste $\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
A\,\,{\rm is\,\,a\,\,set}$\hfill[Rule $\wedge$-in, from (3) and (6)]}

\pline{(10) \ste\ste $\emptyset\subseteq A\iff
(\forall x,(x\in \emptyset\imply x\in A))$\hfill
[Rule $\lto$-out, from (8)\&(9)]}

\pline{(11) \ste\ste $\forall x,(x\in \emptyset\imply x\in A)
\lto\emptyset\subseteq A$\hfill[Rule $\iff$-out, from (10)]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$\forall x,(x\in \emptyset\imply x\in A)\,.$''

\medbreak

\pline{(12) \ste\ste\ste Let $a$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$a\in \emptyset\lto a\in A\,.$''

\medbreak

\pline{(13) \ste\ste\ste\ste Assume $a\in\emptyset$.\hfill[Preparation 
to apply Rule $\lto$-out]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$a\in A\,.$'' We do it by contradiction. That is, we assume 
$\neg(a\in A)$ and get something impossible. 
\medbreak

\pline{(14) \ste\ste\ste\ste\ste Assume $\neg(a\in A)$.[Preparation
to apply Rule $\neg$-out]}

\pline{(15) \ste\ste\ste\ste\ste $\neg a\in\emptyset$.\hfill[Rule
$\forall$-out, plugging $a$ for $x$ in (4)]}

\pline{(16) \ste\ste\ste\ste\ste $a\in\emptyset\wedge(\neg a\in\emptyset)$.
\hfill [Rule $\wedge$-in, from (13) and (15)]}

\pline{(17) \ste\ste\ste\ste $\neg(\neg(a\in A))$.\hfill[Rule $\neg$-in,
from (14) and (16),}

\pline{\hfill  since $a\in\emptyset\wedge(\neg a\in\emptyset)$
is a contradiction]}

\pline{(18) \ste\ste\ste\ste $(\neg(\neg(a\in A)))\imply a\in A$.
\hfill[Rule T]}

\pline{(19) \ste\ste\ste\ste $a\in A$.\hfill[Rule $\lto$-out, from (17) 
and (18)]}

\pline{(20) \ste\ste\ste $a\in\emptyset\imply a\in A$.\hfill[Rule
$\lto$-in, from (13) and (19)]}

\pline{(21) \ste\ste $\forall x,(x\in\emptyset\imply x\in A)$.\hfill
[Rule $\forall$-in, from (12) and (21)]}

\pline{(22) \ste\ste $\emptyset\subseteq A$.\hfill[Rule 
$\lto$-out, from (11) and (21)]}

\pline{(23) \ste $A\,\,{\rm is\,\,a\,\,set}\lto
\emptyset\subseteq A$.\hfill[Rule 
$\lto$-in, from (6) and (22)]}

\pline{(24) $\forall X,(X\,\,{\rm is\,\,a\,\,set}\lto
\emptyset\subseteq X$).\hfill[Rule 
$\forall$-in, from (3) and (23)]}

\pline{{\bf END OF PROOF}\hfill}

\subsection{Another example of a completely formal proof}\label{exacomallsets}

Now let us redo the above proof but {\em working in a universe where
there are only sets and nothing but sets.} Since everything is a set,
now there is no need to specify, every time we bring in an object,
that it is a set.  

Now our definition of the empty set (or our
axiom characterizing the empty set, if you prefer), just says:
\begin{equation}\label{defempty-allsets}
\forall x,(\neg x\in\emptyset)\,.
\end{equation}
(That is, ``nothing belongs to the empty set.'')

\medbreak
The definition of {\em set inclusion} says that if $X$, $Y$ are 
any objects (that is, any sets)
then $X$ is a subset of $Y$ if and only if  
every member of $X$ belongs to $Y$.  In other words, 

\medbreak\noindent FORMAL DEFINITION OF ``SUBSET'' IN A UNIVERSE WHERE THERE 
ARE SETS AND NOTHING ELSE:
$$
\forall X,\forall Y,(X\subseteq Y\iff(\forall x,(x\in X\imply x\in Y)) )\,.
$$


Using these two definitions plus our logical rules, let us give a completely
formal proof of the following.

\begin{theorem}
If $X$ is anything (that is, any set), then $\emptyset\subseteq X$.
\end{theorem}

\medbreak\noindent{\bf PROOF:}

\medbreak
\noindent{\em Comment}: we have to prove that 
``$\forall X,(\emptyset\subseteq X)$.''

\medbreak
\pline{\ (1) $\forall X,\forall Y,(X\subseteq Y\iff
(\forall x,(x\in X\imply x\in Y)))$\hfill[Definition of set inclusion]}

\pline{\ (2) $\forall x,(\neg x\in\emptyset)$.\hfill[Definition
of $\emptyset$]}

\pline{\ (3) \ste Let $A$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we want to prove that ``$\emptyset\subseteq A$.''

\medbreak

\pline{\ (4) \ste $\forall Y,(\emptyset\subseteq Y\iff
(\forall x,(x\in \emptyset\imply x\in Y)))$\hfill}


\pline{\hfill
[Rule $\forall$-out, from (1), specializing $X$ to $\emptyset$]}

\pline{\ (5) \ste $\emptyset\subseteq A\iff
(\forall x,(x\in \emptyset\imply x\in A))$\hfill}

\pline{ \hfill
[Rule $\forall$-out, from (4), specializing $Y$ to $A$]}

\pline{\ (6) \ste $\forall x,(x\in \emptyset\imply x\in A)
\lto\emptyset\subseteq A$\hfill[Rule $\iff$-out, from (10)]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$\forall x,(x\in \emptyset\imply x\in A)\,.$''

\medbreak

\pline{\ (7) \ste\ste Let $a$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$a\in \emptyset\lto a\in A\,.$''

\medbreak

\pline{\ (8) \ste\ste\ste Assume $a\in\emptyset$.\hfill[Preparation 
to apply Rule $\lto$-out]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$a\in A\,.$'' We do it by contradiction. That is, we assume 
$\neg(a\in A)$ and get something impossible. 
\medbreak

\pline{\ (9) \ste\ste\ste\ste Assume $\neg(a\in A)$.[Preparation
to apply Rule $\neg$-out]}

\pline{(10) \ste\ste\ste\ste $\neg a\in\emptyset$.\hfill[Rule
$\forall$-out, plugging $a$ for $x$ in (2)]}

\pline{(11) \ste\ste\ste\ste $a\in\emptyset\wedge(\neg a\in\emptyset)$.
\hfill [Rule $\wedge$-in, from (8) and (10)]}

\pline{(12) \ste\ste\ste $\neg(\neg(a\in A))$.\hfill[Rule $\neg$-in,
from (9) and (11),}

\pline{\hfill  since $a\in\emptyset\wedge(\neg a\in\emptyset)$
is a contradiction]}

\pline{(13) \ste\ste\ste $(\neg(\neg(a\in A)))\imply a\in A$.
\hfill[Rule T]}

\pline{(14) \ste\ste\ste $a\in A$.\hfill[Rule $\lto$-out,
from (12) and (13)]}

\pline{(15) \ste\ste $a\in\emptyset\imply a\in A$.\hfill[Rule
$\lto$-in, from (8) and (14)]}

\pline{(16) \ste $\forall x,(x\in\emptyset\imply x\in A)$.\hfill
[Rule $\forall$-in, from (7) and (15)]}

\pline{(17) \ste $\emptyset\subseteq A$.\hfill[Rule 
$\lto$-out, from (6) and (16)]}

\pline{(18) $\forall X,\emptyset\subseteq X$.\hfill[Rule 
$\forall$-in, from (3) and (17)]}

\pline{{\bf END OF PROOF}\hfill}

\subsection{Remarks on proof levels}

We have explained earlier that {\em every time we introduce
an assumption (for \mbox{example}, when we say ``let $a$ be arbitrary,''
or ``assume $a\in A$'') we initiate a ``subproof,''
or ``proof within a proof,'' in which we place ourselves in an 
\mbox{imaginary}
world where this assumption is true.} 

For example, if I say
``assume I was born in Oslo,'' then I am setting out to explore
an imaginary world in which I was born in Oslo. Whatever 
I prove is proved {\em under the assumption that 
I was born in Oslo.} So, if I show that ``I am Norwegian,'' it does not mean
that I now know that I am Norwegian. All it means is that I know
that {\em the fact that I am Norwegian has been proved under the assumption
that I was born in Oslo.} We can then, if we want, get out from being
``under  the assumption that I was born in Oslo'' and assert
that {\em if I was born in Oslo then I am Norwegian.}  

We indicate these different ``levels of proof''
by introducing extra indentation:

\medbreak
\pline{\phantom{(77)} $\vdots$\hfill}

\pline{(77) I am a mathematician.\hfill[$\ldots$]}

\pline{(78) \ste Assume I was born in Oslo.\hfill[Preparation to apply Rule
$\lto$-in]}

\pline{(79) \ste Oslo is in  Norway\hfill[$\ldots$]}

\pline{(80) \ste  I was born in Norway.\hfill[$\ldots$]}

\pline{(81) \ste  I am Norwegian.\hfill[$\ldots$]}

\pline{(82) If I was born in Olso then I am Norwegian.\hfill
[Rule $\lto$-in, from (78)\&(80)]}

\subsection{A different way of indicating proof levels} 

If we have several proof levels, then it becomes cumbersome to use
indentation. An alternative possibility is to use a number 
to indicate what proof level we are at. For example, the above 
lines about being a Norwegian could be written as follows:

\medbreak
\pline{\phantom{(77)} $\vdots$\hfill}

\pline{(77.0) I am a mathematician.\hfill[$\ldots$]}

\pline{(78.1) Assume I was born in Oslo.\hfill[Preparation to apply Rule
$\lto$-in]}

\pline{(79.1) Oslo is in  Norway\hfill[$\ldots$]}

\pline{(80.1) I was born in Norway.\hfill[$\ldots$]}

\pline{(81.1) I am Norwegian.\hfill[$\ldots$]}

\pline{(82.0) If I was born in Olso then I am Norwegian.\hfill
[Rule $\lto$-in, from (78)\&(80)]}

\bigbreak\noindent
{\bf AN EXAMPLE}:  As an example of how to write proofs using numbers
instead of indentation to indicate proof levels, here is the 
proof of \S\ref{exacom}, rewritten in the new way:


\medbreak\noindent{\bf PROOF:}

\medbreak
\noindent{\em Comment}: we have to prove that 
``$\forall X,(X\,\,{\rm is\,\,a\,\,set}\lto\emptyset\subseteq X)$.''

\medbreak
\pline{\ (1.0) $\forall X,\forall Y,((X\,\,{\rm is\,\,a\,\,set}\wedge
Y\,\,{\rm is\,\,a\,\,set})\lto$\hfill}

\pline{\hfill$(X\subseteq Y\iff
(\forall x,(x\in X\imply x\in Y))))$\hfill[Definition of set inclusion]}

\pline{\ (2.0) $\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
\forall x,(\neg x\in\emptyset)$.\hfill[Definition
of $\emptyset$]}

\pline{\ (3.0) $\emptyset\,\,{\rm is\,\,a\,\,set}$.\hfill
[Rule $\wedge$-out, from (2)]}

\pline{\ (4.0) $\forall x,(\neg x\in\emptyset)$.\hfill
[Rule $\wedge$-out, from (2)]}

\pline{\ (5.1) Let $A$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we want to prove that 
``$A\,\,{\rm is\,\,a\,\,set}\lto\emptyset\subseteq A$.''

\medbreak
\pline{\ (6.2) Assume $A$ is a set. \hfill[Preparation to apply 
Rule $\lto$-in]}

\medbreak
\noindent{\em Comment}: we want to prove that ``$\emptyset\subseteq A$.''

\medbreak
\pline{\ (7.2) $\forall Y,((\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
Y\,\,{\rm is\,\,a\,\,set})\lto(\emptyset\subseteq Y\iff$\hfill}

\pline{\hfill $(\forall x,(x\in \emptyset\imply x\in Y))))$\hfill
[Rule $\forall$-out, from (1), specializing $X$ to $\emptyset$]}

\pline{\ (8.3) $(\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
A\,\,{\rm is\,\,a\,\,set})\lto(\emptyset\subseteq A\iff
(\forall x,(x\in \emptyset\imply x\in A)))$\hfill}

\pline{ \hfill
[Rule $\forall$-out, from (7), specializing $Y$ to $A$]}

\pline{\ (9.2) $\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
A\,\,{\rm is\,\,a\,\,set}$\hfill[Rule $\wedge$-in, from (3) and (6)]}

\pline{(10.2) $\emptyset\subseteq A\iff
(\forall x,(x\in \emptyset\imply x\in A))$\hfill
[Rule $\lto$-out, from (8)\&(9)]}

\pline{(11.2) $\forall x,(x\in \emptyset\imply x\in A)
\lto\emptyset\subseteq A$\hfill[Rule $\iff$-out, from (10)]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$\forall x,(x\in \emptyset\imply x\in A)\,.$''

\medbreak

\pline{(12.3) Let $a$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$a\in \emptyset\lto a\in A\,.$''

\medbreak

\pline{(13.4) Assume $a\in\emptyset$.\hfill[Preparation 
to apply Rule $\lto$-out]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$a\in A\,.$'' We do it by contradiction. That is, we assume 
$\neg(a\in A)$ and get something impossible. 
\medbreak

\pline{(14.5) Assume $\neg(a\in A)$.[Preparation
to apply Rule $\neg$-out]}

\pline{(15.5) $\neg a\in\emptyset$.\hfill[Rule
$\forall$-out, plugging $a$ for $x$ in (4)]}

\pline{(16.5) $a\in\emptyset\wedge(\neg a\in\emptyset)$.
\hfill [Rule $\wedge$-in, from (13) and (15)]}

\pline{(17.4) $\neg(\neg(a\in A))$.\hfill[Rule $\neg$-in,
from (14) and (16), since $a\in\emptyset\wedge(\neg a\in\emptyset)$
is a}

\pline{\hfill  contradiction]}

\pline{(18.4) $(\neg(\neg(a\in A)))\imply a\in A$.
\hfill[Rule T]}

\pline{(19.4) $a\in A$.\hfill[Rule $\lto$-out, from (17) 
and (18)]}

\pline{(20.3) $a\in\emptyset\imply a\in A$.\hfill[Rule
$\lto$-in, from (13) and (19)]}

\pline{(21.2) $\forall x,(x\in\emptyset\imply x\in A)$.\hfill
[Rule $\forall$-in, from (12) and (21)]}

\pline{(22.2) $\emptyset\subseteq A$.\hfill[Rule 
$\lto$-out, from (11) and (21)]}

\pline{(23.1) $A\,\,{\rm is\,\,a\,\,set}\lto
\emptyset\subseteq A$.\hfill[Rule 
$\lto$-in, from (6) and (22)]}

\pline{(24.0) $\forall X,(X\,\,{\rm is\,\,a\,\,set}\lto
\emptyset\subseteq X$).\hfill[Rule 
$\forall$-in, from (3) and (23)]}

\pline{{\bf END OF PROOF}\hfill}

\bigbreak\noindent
{\bf A SECOND EXAMPLE}:  As a second
example of how to write proofs using numbers
instead of indentation to indicate proof levels, here is the 
proof of \S\ref{exacomallsets}, rewritten in the new way:

\medbreak\noindent{\bf PROOF:}

\medbreak
\noindent{\em Comment}: we have to prove that 
``$\forall X,(\emptyset\subseteq X)$.''

\medbreak
\pline{\ (1.0) $\forall X,\forall Y,(X\subseteq Y\iff
(\forall x,(x\in X\imply x\in Y)))$\hfill}

\pline{\hfill[Definition of set inclusion]}

\pline{\ (2.0) $\forall x,(\neg x\in\emptyset)$.\hfill[Definition
of $\emptyset$]}

\pline{\ (3.1) Let $A$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we want to prove that ``$\emptyset\subseteq A$.''

\medbreak

\pline{\ (4.1) $\forall Y,(\emptyset\subseteq Y\iff
(\forall x,(x\in \emptyset\imply x\in Y)))$\hfill}


\pline{\hfill
[Rule $\forall$-out, from (1), specializing $X$ to $\emptyset$]}

\pline{\ (5.1) $\emptyset\subseteq A\iff
(\forall x,(x\in \emptyset\imply x\in A))$\hfill}

\pline{ \hfill
[Rule $\forall$-out, from (4), specializing $Y$ to $A$]}

\pline{\ (6,1) $\forall x,(x\in \emptyset\imply x\in A)
\lto\emptyset\subseteq A$\hfill[Rule $\iff$-out, from (10)]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$\forall x,(x\in \emptyset\imply x\in A)\,.$''

\medbreak

\pline{\ (7.2) Let $a$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$a\in \emptyset\lto a\in A\,.$''

\medbreak

\pline{\ (8.3) Assume $a\in\emptyset$.\hfill[Preparation 
to apply Rule $\lto$-out]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$a\in A\,.$'' We do it by contradiction. That is, we assume 
$\neg(a\in A)$ and get something impossible. 
\medbreak

\pline{\ (9.4) Assume $\neg(a\in A)$.[Preparation
to apply Rule $\neg$-out]}

\pline{(10.4) $\neg a\in\emptyset$.\hfill[Rule
$\forall$-out, plugging $a$ for $x$ in (2)]}

\pline{(11.4) $a\in\emptyset\wedge(\neg a\in\emptyset)$.
\hfill [Rule $\wedge$-in, from (8) and (10)]}

\pline{(12.3) $\neg(\neg(a\in A))$.\hfill[Rule $\neg$-in,
from (9) and (11),}

\pline{\hfill  since $a\in\emptyset\wedge(\neg a\in\emptyset)$
is a contradiction]}

\pline{(13.3) $(\neg(\neg(a\in A)))\imply a\in A$.\hfill[Rule T]}

\pline{(14.3) $a\in A$.\hfill[Rule $\lto$-out, from (12) and (13)]}

\pline{(15.2) $a\in\emptyset\imply a\in A$.\hfill[Rule
$\lto$-in, from (8) and (14)]}

\pline{(16.1) $\forall x,(x\in\emptyset\imply x\in A)$.\hfill
[Rule $\forall$-in, from (7) and (15)]}

\pline{(17.1) $\emptyset\subseteq A$.\hfill[Rule 
$\lto$-out, from (6) and (16)]}

\pline{(18.0) $\forall X,\emptyset\subseteq X$.\hfill[Rule 
$\forall$-in, from (3) and (17)]}

\pline{{\bf END OF PROOF}\hfill}

%\end{document}

\medbreak\noindent{\bf PROOF:}

\medbreak
\noindent{\em Comment}: we have to prove that\\
``$\forall x,\forall A((A\,\,is\,\,a\,\,set)\lto
(\{x\}\subseteq A\iff x\in A))$.''

\medbreak
\pline{\ (1.0) $\forall X,\forall Y,((X\,\,{\rm is\,\,a\,\,set}\wedge
Y\,\,{\rm is\,\,a\,\,set})\lto$\hfill}

\pline{\hfill$(X\subseteq Y\iff
(\forall x,(x\in X\imply x\in Y))))$\hfill[Definition of set inclusion]}

\pline{\ (2.0) $\forall x,(\{x\}\,\,{\rm is\,\,a\,\,set}\wedge
\forall y,(y\in\{x\}\iff y=x\neg x\in\emptyset)$.\hfill[Definition
of $\emptyset$]}

\pline{\ (3.0) $\emptyset\,\,{\rm is\,\,a\,\,set}$.\hfill
[Rule $\wedge$-out, from (2)]}

\pline{\ (4.0) $\forall x,(\neg x\in\emptyset)$.\hfill
[Rule $\wedge$-out, from (2)]}

\pline{\ (5.1) Let $A$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we want to prove that 
``$A\,\,{\rm is\,\,a\,\,set}\lto\emptyset\subseteq A$.''

\medbreak
\pline{\ (6.2) Assume $A$ is a set. \hfill[Preparation to apply 
Rule $\lto$-in]}

\medbreak
\noindent{\em Comment}: we want to prove that ``$\emptyset\subseteq A$.''

\medbreak
\pline{\ (7.2) $\forall Y,((\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
Y\,\,{\rm is\,\,a\,\,set})\lto(\emptyset\subseteq Y\iff$\hfill}

\pline{\hfill $(\forall x,(x\in \emptyset\imply x\in Y))))$\hfill
[Rule $\forall$-out, from (1), specializing $X$ to $\emptyset$]}

\pline{\ (8.3) $(\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
A\,\,{\rm is\,\,a\,\,set})\lto(\emptyset\subseteq A\iff
(\forall x,(x\in \emptyset\imply x\in A)))$\hfill}

\pline{ \hfill
[Rule $\forall$-out, from (7), specializing $Y$ to $A$]}

\pline{\ (9.2) $\emptyset\,\,{\rm is\,\,a\,\,set}\wedge
A\,\,{\rm is\,\,a\,\,set}$\hfill[Rule $\wedge$-in, from (3) and (6)]}

\pline{(10.2) $\emptyset\subseteq A\iff
(\forall x,(x\in \emptyset\imply x\in A))$\hfill
[Rule $\lto$-out, from (8)\&(9)]}

\pline{(11.2) $\forall x,(x\in \emptyset\imply x\in A)
\lto\emptyset\subseteq A$\hfill[Rule $\iff$-out, from (10)]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$\forall x,(x\in \emptyset\imply x\in A)\,.$''

\medbreak

\pline{(12.3) Let $a$ be arbitrary.\hfill[Preparation to apply 
Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$a\in \emptyset\lto a\in A\,.$''

\medbreak

\pline{(13.4) Assume $a\in\emptyset$.\hfill[Preparation 
to apply Rule $\lto$-out]}

\medbreak
\noindent{\em Comment}: we now set out to prove that 
``$a\in A\,.$'' We do it by contradiction. That is, we assume 
$\neg(a\in A)$ and get something impossible. 
\medbreak

\pline{(14.5) Assume $\neg(a\in A)$.[Preparation
to apply Rule $\neg$-out]}

\pline{(15.5) $\neg a\in\emptyset$.\hfill[Rule
$\forall$-out, plugging $a$ for $x$ in (4)]}

\pline{(16.5) $a\in\emptyset\wedge(\neg a\in\emptyset)$.
\hfill [Rule $\wedge$-in, from (13) and (15)]}

\pline{(17.4) $\neg(\neg(a\in A))$.\hfill[Rule $\neg$-in,
from (14) and (16), since $a\in\emptyset\wedge(\neg a\in\emptyset)$
is a}

\pline{\hfill  contradiction]}

\pline{(18.4) $(\neg(\neg(a\in A)))\imply a\in A$.
\hfill[Rule T]}

\pline{(19.4) $a\in A$.\hfill[Rule $\lto$-out, from (17) 
and (18)]}

\pline{(20.3) $a\in\emptyset\imply a\in A$.\hfill[Rule
$\lto$-in, from (13) and (19)]}

\pline{(21.2) $\forall x,(x\in\emptyset\imply x\in A)$.\hfill
[Rule $\forall$-in, from (12) and (21)]}

\pline{(22.2) $\emptyset\subseteq A$.\hfill[Rule 
$\lto$-out, from (11) and (21)]}

\pline{(23.1) $A\,\,{\rm is\,\,a\,\,set}\lto
\emptyset\subseteq A$.\hfill[Rule 
$\lto$-in, from (6) and (22)]}

\pline{(24.0) $\forall X,(X\,\,{\rm is\,\,a\,\,set}\lto
\emptyset\subseteq X$).\hfill[Rule 
$\forall$-in, from (3) and (23)]}

\pline{{\bf END OF PROOF}\hfill}

\bigbreak\noindent{\bf ANOTHER EXAMPLE:} Given that ``not all
borogoves are mimsy,'' prove that ``there exist borogoves that are not
mimsy.''  (That is, given the hypothesis that 
``$\neg(\forall x,(x\,\,{\rm is\,\,a\,\,borogove}\lto x\,\,{\rm
is\,\,mimsy}))$,'' we want to conclude that 
``$\exists x,(x\,\,{\rm is\,\,a\,\,borogove}\wedge x\,\,{\rm
is\,\,not\,\,mimsy})$.'')


\medbreak\noindent{\bf PROOF:}

\medbreak
\noindent{\em Comment}: We will prove 
``$\exists x,(x\,\,{\rm is\,\,a\,\,borogove}\wedge x\,\,{\rm
is\,\,not\,\,mimsy})$'' by contradiction. That is, we will assume
that ``$\neg\exists x,(x\,\,{\rm is\,\,a\,\,borogove}\wedge x\,\,{\rm
is\,\,not\,\,mimsy})$'' and will get to something  that we know is false.
The most obvious false thing we could try to get is
``$\forall x,(x\,\,{\rm is\,\,a\,\,borogove}\lto x\,\,{\rm
is\,\,mimsy})$.''  So the basic structure of our proof will be:
assume  ``$\neg\exists x,(x\,\,{\rm is\,\,a\,\,borogove}\wedge x\,\,{\rm
is\,\,not\,\,mimsy})$'' and prove 
``$\forall x,(x\,\,{\rm is\,\,a\,\,borogove}\lto x\,\,{\rm
is\,\,mimsy})$.''  
\medbreak

\pline{\,\,\,(1) $\neg(\forall x,(x$ is a borogove$\lto$ $x$ is mimsy)).\hfill
[Assumption]}

\pline{(1a) \ste Assume $\neg\exists x,(x\,\,{\rm is\,\,a\,\,borogove}
\wedge(\neg\, x\,\,{\rm is\,\,mimsy}))$.\hfill}

\pline{\hfill[Preparation to apply Rule $\neg$-out]}

\medbreak
\noindent{\em Comment}: We set out to prove 
``$\forall x,(x\,\,{\rm is\,\,a\,\,borogove}\lto x\,\,{\rm
is\,\,mimsy})$.''  
\medbreak

\pline{\,\,\,(2) \ste\ste Let $a$ be arbitrary.\hfill[Preparation to apply Rule
$\forall$-in]}

\medbreak
\noindent{\em Comment}: We try to prove 
``$a\,\,{\rm is\,\,a\,\,borogove}\lto a\,\,{\rm
is\,\,mimsy}$.''  
\medbreak

\pline{\,\,\,(3) \ste\ste\ste Assume $a$ is a borogove.\hfill[Preparation to 
apply Rule $\lto$-in]}

\medbreak 
\noindent{\em Comment}: We try to prove ``$a\,\,{\rm is\,\,mimsy}$.''
Since we cannot think of any other way to do it, we try a proof by
contradiction: assume $a$ is not mimsy and see what happens.
\medbreak

\pline{\,\,\,(4) \ste\ste\ste\ste Assume $\neg\,a$ is mimsy.\hfill[Preparation to 
apply Rule $\neg$-in]}

\pline{\,\,\,(5) \ste\ste\ste\ste $a$ is a borogove $\wedge\neg\,a$ is mimsy.
[Rule $\wedge$-in, from (3)\&(4)]}

\pline{\,\,\,(6) \ste\ste\ste\ste $\exists x, (x$ is a borogove $\wedge\neg\,x$ is mimsy).
\hfill[Rule $\exists$-in, from (5)]}

\pline{\,\,\,(7) \ste\ste\ste\ste $\neg\exists x,(x\,\,{\rm is\,\,a\,\,borogove}
\wedge(\neg\, x\,\,{\rm is\,\,mimsy}))\wedge
\exists x, (x$ is a \hfill}

\pline{\hfill borogove $\wedge\neg\,x$ is mimsy).
[Rule $\wedge$-in, from (1a) and (6)]}

\pline{\,\,\,(8) \ste\ste\ste $\neg(\neg\,a$ is mimsy).\hfill[Rule $\neg$-in,
from (4) and (7), since the]}

\pline{\hfill statement of (7) is a contradiction]}

\pline{\,\,\,(9) \ste\ste\ste $(\neg(\neg\,a$ is mimsy$))\lto a$ is mimsy.\hfill[
Rule T]}

\pline{(10) \ste\ste\ste $a$ is mimsy.\hfill[Rule $\lto$-out, from
(8) and (9)]}

\pline{(11) \ste\ste $a$ is a borogove$\lto$ $a$ is mimsy.\hfill
[Rule $\lto$-in, from (3) and (10)]}

\pline{(12) \ste $\forall x,(x$ is a borogove$\lto$ $x$ is mimsy).\hfill
[Rule $\forall$-in, from (2) and (11)]}

\newpage

\pline{(13) $\neg(\neg,(\exists x,(x\,\,{\rm is\,\,a\,\,borogove}
\wedge(\neg\, x\,\,{\rm is\,\,mimsy}))))$.\hfill}

\pline{\hfill[Rule $\neg$-out, from (1), (1a) and (12)}

\pline{(14) $\neg(\neg,(\exists x,(x\,\,{\rm is\,\,a\,\,borogove}
\wedge(\neg\, x\,\,{\rm is\,\,mimsy}))))\lto$.\hfill}

\pline{\phantom{(14) $\neg(\neg,($} $\exists x,(x\,\,{\rm is\,\,a\,\,borogove}
\wedge(\neg\, x\,\,{\rm is\,\,mimsy}))$.\hfill[Rule T]}

\pline{(15) $\exists x,(x\,\,{\rm is\,\,a\,\,borogove}
\wedge(\neg\, x\,\,{\rm is\,\,mimsy}))$.\hfill[Rule $\lto$-out, from
(13) and (14)]}

\pline{\ \ \ {\bf END OF PROOF.}\hfill}



\end{document}


\medbreak\noindent{\bf ATTEMPTED PROOF:}

\medbreak
\noindent{\em Comment}: we have to prove that\\
``$\forall x\in\zz,((x>0\wedge\neg\, x\,\,{\rm is\,\,prime})
\lto x\,\,{\rm is\,\,composite})$.''


\medbreak
\pline{\ (1.0) $\forall x\in\zz,(x\,\,{\rm is\,\,prime}
\iff(x>1\wedge\forall y\in\zz,\forall z\in\zz,$\hfill}

\pline{\hfill$(((1\le y\wedge 1\le z)\wedge x=y.z)\lto(y=1\vee z=1))))$
\hfill[Definition of ``prime'']}

\pline{\ (2.0) $\forall x\in\zz,(x\,\,{\rm is\,\,composite}
\iff(\exists y\in\zz,\exists z\in\zz,((1<y\wedge 1<z)\wedge x=y.z)))$\hfill}

\pline{\hfill\hfill[Definition of ``composite'']}

\pline{\ (3.1) Let $a\in\zz$ be arbitrary.\hfill
[Preparation to apply Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we will prove that 
``$(a>0\wedge\neg\,a\,\,{\rm is\,\,prime})
\lto a\,\,{\rm is\,\,composite}$.''

\medbreak

\pline{\ (4.2) Assume $a>0\wedge\neg\,a$ is prime.\hfill
[Preparation to apply Rule $\lto$-in]}

\medbreak
\noindent{\em Comment}: we will prove that 
``$a\,\,{\rm is\,\,composite}$.''

\medbreak

\pline{\ (5.2) $a>0$.\hfill[Rule $\wedge$-out, from (4)]}

\pline{\ (6.2) $\neg\,a$ is prime.\hfill
[Rule $\wedge$-out, from (4)]}

\pline{\ (7.2) $a\,\,{\rm is\,\,prime}
\iff(a>1\wedge\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto$\hfill}

\pline{\hfill$(y=1\vee z=1)))$
\hfill[Rule $\forall$-out, from (1), specializing $x$ to $a$]}

\medbreak
\noindent{\em Comment}: at this point we know that 
``$a$ is prime $\iff$ something,'' and we also know that
``$\neg\,a$ is prime.'' From these two things, it should follow
that the ``something'' isn't true. A simple propositional logic 
argument will do the trick: if we have $A\iff B$, and also $\neg\,A$,
then from $A\iff B$ we can get $B\lto A$ by Rule $\iff$-out, and
then we can get $\neg\,B$ by arguing as follows: assume $B$; then
we get $A$ by Modus Ponens; but we have $\neg\,A$; so Rule 
$\neg$-out enables us to go to $\neg\,B$.

\medbreak
\pline{\ (8.2) $(a>1\wedge\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1)))$\hfill}

\pline{\hfill$\lto\,a\,\,{\rm is\,\,prime}$
\hfill[Rule $\forall$-out, from (1), specializing $x$ to $a$]}

\pline{\ (9.3) Assume $(a>1\wedge\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)$\hfill}

\pline{\hfill$\lto(y=1\vee z=1)))$\hfill
[Preparation to apply Rule $\neg$-out]}

\pline{(10.3) $a\,\,{\rm is\,\,prime}$\hfill[Rule $\lto$-out, from
(8) and (9)]}

\pline{(11.2) $\neg(a>1\wedge\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1)))$\hfill}

\pline{\hfill[Rule $\neg$-out, from (6), (9)  and (10)]}

\medbreak\noindent{\em Comment}: at this point we know that a certain
conjunction $A\wedge B$ is false, where 
\begin{itemize}\item[1.] $A$ is ``$a>1\,$,''
\end{itemize}
and 
\begin{itemize}\item[2.] $B$ is 
``$\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))\,$.''
\end{itemize}
We should be able to infer from this that 
``$(\neg\,A)\vee(\neg\,B)$,'' by the so-called ``De Morgan laws.''
One way to do that is to use the tautology $(\neg\,(A\wedge B))
\lto((\neg\,A)\vee(\neg\,B))$.
\medbreak

\pline{(12.2) $(\neg(a>1\wedge$\hfill}

\pline{\phantom{(12.2)}\ $\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))))\lto$\hfill}

\pline{\hfill $((\neg\,a>1)\vee(\neg\,\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))))$\hfill}

\pline{(13.2) $(\neg\,a>1)\vee$\hfill}

\pline{\hfill $(\neg\,\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1)))$\hfill}

\pline{\hfill [Rule $\lto$-out, from (11) and (12)]}

\medbreak\noindent{\em Comment}: at this point we know that either
$\neg\,a>1$ or it's not true that $\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))$.
{\bf If we could exclude the possibility that 
$\neg\,a>1$,} then we would know that 
it's not true that $\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))$.
Now, to say that ``for all $y$ and for all $z$ something happens''
is not true, amounts to saying that for some 
$y$ and some $z$ the ``something'' does not  happen. In other words,
there exist integers $y$ and $z$ such that the sentence
``$((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1)$'' isn't true.
But this sentence is an implication, and the only way an implication
can be false is when the premiss is true but the conclusion is false. That is,
our integers $y$ and $z$ must be such that 
$1\le y$ and $1\le z$ and $\neg\,(y=1\vee z=1)$. Now
``$\neg\,(y=1\vee z=1)$'' implies that 
$y\neq 1$ and $z\neq 1$ by the De Morgan laws. Since we already know
that $y\ge 1$, the fact that $y\neq 1$ tells us that 
$y>1$. Since we already know
that $z\ge 1$, the fact that $z\neq 1$ tells us that
$z>1$. So $y>1$, $z>1$ and $a=y.z$. But this tells us precisely that
$a$ is composite, which is exactly what we wanted.

All this, however, is predicated on our ability to exclude the possibility
that $\neg\,a>1$.  In other words, we know what to do if we manage
to show that $a>1$. Since we know that $a>0$, our problem
is to exclude the possibility that $a=1$. 

Now, can we exclude this possibility? If we look at all the
information we have, there seems to be no way to get from it to
``$a>1$.''  So {\large\bf we are stuck!!!}. We do {\bf not} know how
to go on with our proof.

Once we get to such a situation, we have to consider the alternative
possibility, namely, that our statement cannot be proved because
it is false. Let us see. If we could take care of the 
case $a=1$ and exclude it, then we know how to finish our 
proof. So if our statement is false, it has to be because
of the truble caused by7 the case $a=1$. Let us look at this case. 
If $a=1$, then
\begin{itemize}
\item[1.] $a$ is a positive integer,
\item[2.] $a$ is not prime,
\end{itemize}
but
\begin{itemize}
\item[3.] $a$ is not composite!!!!!
\end{itemize}
Therefore, the  statement that we were trying to prove,
namely, ``a positive integer which is not prime is
composite,'' is {\bf false}, because $1$ is a counterexample.

\medbreak\noindent CONCLUSION: the statement cannot be proved because
it is false. Our attempt to write a proof {\large\bf being careful
and not cheating} ended in  failure, because we discovered 
a possible case that could arise under which the result we wanted
to prove is false. 

\medbreak\noindent{\bf PROOF:}

\medbreak
\noindent{\em Comment}: we have to prove that\\
``$\forall x\in\zz,((x>1\wedge\neg\, x\,\,{\rm is\,\,prime})
\lto x\,\,{\rm is\,\,composite})$.''


\medbreak
\pline{\ (1.0) $\forall x\in\zz,(x\,\,{\rm is\,\,prime}
\iff(x>1\wedge\forall y\in\zz,\forall z\in\zz,$\hfill}

\pline{\hfill$(((1\le y\wedge 1\le z)\wedge x=y.z)\lto(y=1\vee z=1))))$
\hfill[Definition of ``prime'']}

\pline{\ (2.0) $\forall x\in\zz,(x\,\,{\rm is\,\,composite}
\iff(\exists y\in\zz,\exists z\in\zz,((1<y\wedge 1<z)\wedge x=y.z)))$\hfill}

\pline{\hfill\hfill[Definition of ``composite'']}

\pline{\ (3.1) Let $a\in\zz$ be arbitrary.\hfill
[Preparation to apply Rule $\forall$-in]}

\medbreak
\noindent{\em Comment}: we will prove that 
``$(a>1\wedge\neg\,a\,\,{\rm is\,\,prime})
\lto a\,\,{\rm is\,\,composite}$.''

\medbreak

\pline{\ (4.2) Assume $a>1\wedge\neg\,a$ is prime.\hfill
[Preparation to apply Rule $\lto$-in]}

\medbreak
\noindent{\em Comment}: we will prove that 
``$a\,\,{\rm is\,\,composite}$.''

\medbreak

\pline{\ (5.2) $a>1$.\hfill[Rule $\wedge$-out, from (4)]}

\pline{\ (6.2) $\neg\,a$ is prime.\hfill
[Rule $\wedge$-out, from (4)]}

\pline{\ (7.2) $a\,\,{\rm is\,\,prime}
\iff(a>1\wedge\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto$\hfill}

\pline{\hfill$(y=1\vee z=1)))$
\hfill[Rule $\forall$-out, from (1), specializing $x$ to $a$]}

\medbreak
\noindent{\em Comment}: at this point we know that 
``$a$ is prime $\iff$ something,'' and we also know that
``$\neg\,a$ is prime.'' From these two things, it should follow
that the ``something'' isn't true. A simple propositional logic 
argument will do the trick: if we have $A\iff B$, and also $\neg\,A$,
then from $A\iff B$ we can get $B\lto A$ by Rule $\iff$-out, and
then we can get $\neg\,B$ by arguing as follows: assume $B$; then
we get $A$ by Modus Ponens; but we have $\neg\,A$; so Rule 
$\neg$-out enables us to go to $\neg\,B$.

\medbreak
\pline{\ (8.2) $(a>1\wedge\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1)))$\hfill}

\pline{\hfill$\lto\,a\,\,{\rm is\,\,prime}$
\hfill[Rule $\forall$-out, from (1), specializing $x$ to $a$]}

\pline{\ (9.3) Assume $(a>1\wedge\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)$\hfill}

\pline{\hfill$\lto(y=1\vee z=1)))$\hfill
[Preparation to apply Rule $\neg$-out]}

\pline{(10.3) $a\,\,{\rm is\,\,prime}$\hfill[Rule $\lto$-out, from
(8) and (9)]}

\pline{(11.2) $\neg(a>1\wedge\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1)))$\hfill}

\pline{\hfill[Rule $\neg$-out, from (6), (9)  and (10)]}

\medbreak\noindent{\em Comment}: at this point we know that a certain
conjunction $A\wedge B$ is false, where 
\begin{itemize}\item[1.] $A$ is ``$a>1\,$,''
\end{itemize}
and 
\begin{itemize}\item[2.] $B$ is 
``$\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))\,$.''
\end{itemize}
We should be able to infer from this that 
``$(\neg\,A)\vee(\neg\,B)$,'' by the so-called ``De Morgan laws.''
One way to do that is to use the tautology $(\neg\,(A\wedge B))
\lto((\neg\,A)\vee(\neg\,B))$.
\medbreak

\pline{(12.2) $(\neg(a>1\wedge$\hfill}

\pline{\phantom{(12.2)}\ $\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))))\lto$\hfill}

\pline{\hfill $((\neg\,a>1)\vee(\neg\,\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))))$\hfill}

\pline{(13.2) $(\neg\,a>1)\vee$\hfill}

\pline{\hfill $(\neg\,\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1)))$\hfill}

\pline{\hfill [Rule $\lto$-out, from (11) and (12)]}

\medbreak\noindent{\em Comment}: at this point we know that either
$\neg\,a>1$ or it's not true that $\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))$.
{\bf If we could exclude the possibility that 
$\neg\,a>1$,} then we would know that 
it's not true that $\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))$.
Now, to say that ``for all $y$ and for all $z$ something happens''
is not true, amounts to saying that for some 
$y$ and some $z$ the ``something'' does not  happen. In other words,
there exist integers $y$ and $z$ such that the sentence 
``$((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1)$'' isn't true.
But this sentence is an implication, and the only way an implication
can be false is when the premiss is true but the conclusion is false. That is,
our integers $y$ and $z$ must be such that 
$1\le y$ and $1\le z$ and $\neg\,(y=1\vee z=1)$. Now
``$\neg\,(y=1\vee z=1)$'' implies that 
$y\neq 1$ and $z\neq 1$ by the De Morgan laws. Since we already know
that $y\ge 1$, the fact that $y\neq 1$ tells us that 
$y>1$. Since we already know
that $z\ge 1$, the fact that $z\neq 1$ tells us that
$z>1$. So $y>1$, $z>1$ and $a=y.z$. But this tells us precisely that
$a$ is composite, which is exactly what we wanted.

The possibility that $\neg\,a>1$ is easily excluded, because we know
(thanks to Step 5) that $a>1$.  Formally, we find ourselves in the
following situation: we know that $(\neg\,A)\vee B$, where $A$ is
``$a>1$'' and $B$ is the horribly long sentence ``$\neg\,\forall
y\in\zz,\forall z\in\zz, (((1\le y\wedge 1\le z)\wedge
a=y.z)\lto(y=1\vee z=1))$.''  We also know that $A$ is true.
Using the tautology $((\neg\,A)\vee B)\lto(A\lto B)$, we can 
get to $B$ by two applications of Modus Ponens. Let us do it. 
\medbreak

\pline{(14.2) $((\neg\,a>1)\vee$\hfill}

\pline{\hfill $(\neg\,\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))))$\hfill}

\pline{\phantom{(14.2)} $\lto$\hfill}

\pline{\phantom{(14.2)} $(a>1\lto$\hfill}


\pline{\hfill $(\neg\,\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))))$\hfill}

\pline{\hfill [Rule T]}

\pline{(15.2) $a>1\lto$\hfill}


\pline{\hfill $(\neg\,\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1)))$\hfill}

\pline{\hfill [Rule $\lto$-out, from (13) and (14)]}

\pline{(16.2) $\neg\,\forall y\in\zz,\forall z\in\zz,
(((1\le y\wedge 1\le z)\wedge a=y.z)\lto(y=1\vee z=1))$\hfill}

\pline{\hfill [Rule $\lto$-out, from (5) and (15)]}




\end{document}


