\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
\usepackage[all]{xypic}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\definecolor{slidelightblue}{rgb}{.8,.8,1}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\def\lightblue#1{\textcolor{slidelightblue}{#1}}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\large\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-3em}$}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large normalization \& classical logic}

\red{logical verification} \\
week 3 \\
2004 09 22

\end{slide}

\begin{slide}
\slidetitle{practical work}
\begin{itemize}
\item[$\bullet$]
monday noon is the limit
\item[$\bullet$]
importance of precise notation
\begin{itemize}
\item
labels in assumptions should go inside the brackets

\green{
\red{$\begin{array}{c}{\phantom{{}^x}[A]^x}\\\noalign{\vspace{-.8\medskipamount}}\vdots\end{array}$}
should be
\red{$\begin{array}{c}{[A^x]}\\\noalign{\vspace{-.8\medskipamount}}\vdots\end{array}$}
}

\item
left-right order of hypotheses matters

\green{
\red{$\displaystyle{\begin{array}{c}\vdots\\\noalign{\vspace{-\medskipamount}}A\\\noalign{\vspace{-.5\smallskipamount}}\end{array}\quad\begin{array}{c}\vdots\\\noalign{\vspace{-\medskipamount}}A\to B\\\noalign{\vspace{-.5\smallskipamount}}\end{array}\over\strut B}$}
should be
\red{$\displaystyle{\begin{array}{c}\vdots\\\noalign{\vspace{-\medskipamount}}A\to B\\\noalign{\vspace{-.5\smallskipamount}}\end{array}\quad\begin{array}{c}\vdots\\\noalign{\vspace{-\medskipamount}}A\\\noalign{\vspace{-.5\smallskipamount}}\end{array}\over\strut B}$}
}

\end{itemize}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{contents for today}
\begin{itemize}
\item[$\bullet$]
recap
\item[$\bullet$]
term \& proof \red{normalization}
\item[$\bullet$]
\red{variants} of propositional logic
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{recap}
\slidetitle{minimal logic}
$$
{
\begin{array}{c}
[A^x] \\
\vdots \\
B
\end{array}
\over
\strut
\red{A \to B}
}
\enskip
\green{I[x]{\to}}
\leqno{\mbox{\rlap{\textbf{$\to$ introduction}}}}
$$
$$
{
\begin{array}{c}
\vdots \\
\red{A \to B}
\end{array}
\qquad
\begin{array}{c}
\vdots \\
A
\end{array}
\over
\strut
B
}
\enskip
\green{E{\to}}
\leqno{\mbox{\rlap{\textbf{$\to$ elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{$\lambda{\to}\;\;$ simply typed $\lambda$-calculus}
$$
{
\Gamma,\, x : A,\, \Gamma' \,\vdash\, \red{x} : A
}
\leqno{\mbox{\rlap{\textbf{variable rule}}}}
$$

\rightline{\green{$x$ does not occur in $\Gamma'$}}

$$
{
\strut
\Gamma,\, x : A \,\vdash\, t : B
\over
\strut
\Gamma \,\vdash\, (\red{\lambda x : A.\, t}) : (A \to B)
}
\leqno{\mbox{\rlap{\textbf{abstraction rule}}}}
$$

$$
{
\strut
\Gamma \,\vdash\, t : A \to B
\qquad
\Gamma \,\vdash\, u : A
\over
\strut
\Gamma \,\vdash\, \red{t\,u} : B
}
\leqno{\mbox{\rlap{\textbf{application rule}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{Currying}
$$
\begin{array}{l}
\red{A} \to \red{B} \to\; (C \to D) \adviwait\\
\lambda (\red{x:A}) \; (\red{y:B}).\, (\advirecord{a1}{\lambda z:C.\, M}) \adviwait\adviplay{a1}\adviwait\\
(f \, \red{a} \, \red{b}) \, c \\
\noalign{\bigskip\adviwait}
\red{A} \to \red{B} \to \red{C} \to D \\
\lambda (\red{x:A}) \; (\red{y:B}) \; (\red{z:C}).\, M \\
f \, a \, b \, c \\
\noalign{\bigskip\adviwait}
\red{A} \to (B \to (C \to D)) \\
\lambda \red{x:A}.\, \lambda y:B.\, \lambda z:C.\, M \\
((f \, \red{a}) \, b) \, c
\end{array}
$$
\vspace{-4pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{examples}
\begin{itemize}
\item[$\bullet$]
\green{permutation}
$$
\red{(A \to B \to C) \to (B \to A \to C)}
\medskip
$$
\item[$\bullet$]
\green{weak version of Peirce's law}
$$
\red{((((A \to B) \to A) \to A) \to B) \to B}
$$
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Curry-Howard-de Bruijn isomorphism}
\begin{itemize}
\item[$\bullet$]
\textbf{propositions as types}
\medskip

a \red{term} inhabits a \green{type} \\
a \red{proof} inhabits a \green{proposition}
\medskip

\item[$\bullet$]
\textbf{Brouwer-Heyting-Kolmogorov interpretation}
$$\red{\lambda x:A.\, M} \;:\; \green{A \to B}$$
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{normalization}
\slidetitle{term normalization}
\green{$\beta$-step}

\begin{eqnarray*}
\dots\, (\red{(\lambda x:A.\, M)\, N}) \dots \quad &\green{\to_\beta}& \quad  \dots\, (\red{M[x:=N]}) \dots \\
\noalign{\bigskip\bigskip\adviwait}
\dots\, (\red{(\lambda x:{\mathbb R}.\; x^2 - 2)\; 4}) \dots \quad &\green{\to_\beta}& \quad  \dots\, (\red{4^2 - 2}) \dots \\
\noalign{\medskip\adviwait}
\dots\, (\red{(\lambda x:A.\; x)\, y}) \dots \quad &\green{\to_\beta}& \quad  \dots\, \red{y} \dots
\end{eqnarray*}
\vfill
\end{slide}

\begin{slide}
\slidetitle{substitution}
renaming bound variables: \green{$\alpha$-equivalence}
$$\lambda \red{x}:A.\, (\dots\, \red{x} \dots) \quad \green{=_\alpha} \quad \lambda \red{y}:A.\, (\dots\, \red{y} \dots)\adviwait$$
\begin{eqnarray*}
\hspace{-0em}\lambda x:A\to B.\, \red{(\lambda y:A\to B.\, \lambda x:A.\, y\, x)\, x} \adviwait&{{\not\to}_\beta}& \lambda x:A\to B.\, \red{(\lambda x:A.\, x\, x)}\hspace{-2em} \adviwait\\
{\dots\, \green{\lambda \phantom{x}\llap{$z$}:A.\, y\, \rlap{$z$}\phantom{x}}\rlap{$\;\dots$}}\phantom{)\, x} &{\to_\beta}& \lambda x:A\to B.\, \red{(\lambda z:A.\, x\, z)}\hspace{-2em} \\
\noalign{
\adviwait
\bigskip
\medskip
\blue{de Bruijn indices}
\medskip
}
\lambda_{A\to B}.\, \red{(\lambda_{A\to B}.\, \lambda_A.\, 1\; 0)\; 0} &{\to_\beta}& \lambda _{A\to B}.\, \red{(\lambda _A.\, 1\; 0)}
\end{eqnarray*}
\vfill
\end{slide}
    
\def\tto{\to\hspace{-5pt}\!\!\to}

\begin{slide}
\slidetitle{reduction}
\green{iterated beta steps}
$$
M_1 \;\to_\beta\; M_2 \;\to_\beta\; M_3 \;\to_\beta\; ... \;\to_\beta\; \red{M_n}
$$
$$
M_1 \;\;\green{\tto_\beta}\;\; \red{M_n}
$$

\red{normal form}
\vfill
\end{slide}

\begin{slide}
\slidetitle{detours}
combination of \green{$\;I[\dots]{\to}\;$} and \green{$\;E{\to}\;$}

$$
{
\displaystyle
{
\begin{array}{c}
[\red{A}^x] \\
\vdots \\
\red{B}
\end{array}
\over
\strut
A \to B
}
\enskip
\green{I[x]{\to}}
\qquad
\begin{array}{c}
\vdots \\
\red{A}
\end{array}
\over
\strut
\red{B}
}
\enskip
\green{E{\to}}
\bigskip
$$

{`proof of $\red{B}$ using a \textbf{lemma} $\red{A}$'}
\vfill
\end{slide}

\begin{slide}
\slidetitle{example}

\begin{center}
\medskip
proof of \red{$\;A \to B \to A\;$} with a $\;$\green{detour}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{detour elimination}
\blue{(cut elimination)}
%\adviwait

$$
\begin{array}{c}
\displaystyle
{
\displaystyle
{
\begin{array}{c}
\red{[A^x]} \\
\vdots \\
\green{B}
\end{array}
\over
\strut
A \to B
}
\enskip
I[x]{\to}
\qquad
\red{
\begin{array}{c}
\vdots \\
A
\end{array}
}
\over
\strut
B
}
\enskip
E{\to}
\end{array}
\qquad
\mbox{\Large $\to$}
\qquad\quad
\begin{array}{c}
\red{\vdots} \\
\red{A} \\
\vdots \\
\green{B}
\end{array}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{Curry-Howard-De Bruijn}
\begin{center}
\begin{tabular}{rcl}
\red{detour} &\red{$\sim$}& \red{$\beta$-redex} \\
\noalign{\bigskip}
\noalign{\rlap{$\hspace{-1em}$\red{$\beta$-redex}: combination of \green{abstraction} and \green{application}}}
\noalign{\medskip}
\noalign{\rlap{$\hspace{-1em}$\red{detour}: combination of \green{$\to$ introduction} and \green{$\to$ elimination}}}
\noalign{\bigskip\medskip}%\adviwait}
proof normalization &\red{$\sim$}& $\beta$-reduction \\
normalization step &\red{$\sim$}& reduction step$\quad$ \\
normal proof &\red{$\sim$}& normal form \\
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{consistency}
\slidetitle{proof checking \& type checking}

\begingroup
\large
$$
\green{
\mathop{\vdash}^{\textstyle \red{?}}\, M : A
}
\bigskip
$$
\endgroup

\begin{itemize}
\item[$\bullet$]
decidable?
\item[$\bullet$]
complexity?
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{provability \& inhabitation}

\begingroup
\large
$$
\green{
\vdash\, \red{?} : A
}
\bigskip
$$
\endgroup

\begin{itemize}
\item[$\bullet$]
decidable?
\item[$\bullet$]
complexity?
\end{itemize}
\adviwait
\bigskip

%\begin{center}
%\blue{consistency}
%\end{center}
\begingroup
\large
$$
\green{
\vdash\, \red{?} : \bot
}
\leqno{\mbox{\normalsize\blue{consistency}}}
\bigskip
$$
\endgroup

\vfill
\end{slide}

\begin{slide}
\sectiontitle{\gray{second hour}}
\slidetitle{confluence}

\textbf{proposition} \green{(not proved in the course)}

$$
\xymatrix{
& M\ar@{->>}[ld]\ar@{->>}[rd] & \\
M_1\ar@{-->>}[rd] & & M_2\ar@{-->>}[ld] \\
& \red{M'} & \\
}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{termination}

\textbf{proposition} \green{(not proved in the course)}
\medskip

\begin{quote}
\red{weak termination:} every term has a normal form

\red{strong termination:} no term has an infinite reduction
\end{quote}
\bigskip
\bigskip

does hold for \textbf{typed} $\lambda$-calculus

does \textbf{not} hold for untyped $\lambda$-calculus
$$\green{(\lambda x.\, x x)\,(\lambda x.\, x x) \quad \tto_\beta \quad (\lambda x.\, x x)\,(\lambda x.\, x x)}$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{subject reduction}

\textbf{proposition} \green{(not proved in the course)}
\medskip

\begin{quote}
\red{types are preserved under computation}
$$
\Gamma \vdash M : A  \quad\enskip\&\quad\enskip  M \tto_\beta M'  \quad\Rightarrow\quad  \Gamma \vdash M' : A
$$
\end{quote}
\vfill
\end{slide}

\begin{slide}
\slidetitle{characterization of normal forms}

$$
\red{x} \, N_1 \, N_2 \, \dots \, N_k
\medskip
$$
$$
\red{\lambda x:A.}\, N
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{consistency}

\textbf{proposition}
\medskip

\begin{quote}
\red{there is no proof of $\;\bot\;$ in minimal logic}
\end{quote}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{classical logic}
\slidetitle{$\bot$ elimination}

$$
{
\begin{array}{c}
\vdots \\
\bot
\end{array}
\over
\strut \red{A}
}
\enskip
\green{E\bot}
\bigskip
$$

\red{`ex falso [sequitur] quodlibet'}
\adviwait
\bigskip
\bigskip

\begin{center}
%\large
\blue{\texttt{elimtype False.}}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{$\neg$ rules}
negation is \textbf{defined}: \red{$\neg A := A \to \bot$}

$$
{
\begin{array}{c}
[A^x] \\
\vdots \\
\bot
\end{array}
\over
\strut
\red{\neg A}
}
\enskip
\green{I[x]{\neg}}
\leqno{\mbox{\rlap{\textbf{$\neg$ introduction}}}}
$$
$$
{
\begin{array}{c}
\vdots \\
\neg A
\end{array}
\qquad
\begin{array}{c}
\vdots \\
A
\end{array}
\over
\strut
\red{\bot}
}
\enskip
\green{E{\neg}}
\leqno{\mbox{\rlap{\textbf{$\neg$ elimination}}}}
$$
\vspace{-10pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{variants of propositional logic}
\begin{itemize}
\item[$\bullet$]
\green{minimal logic}

only implication
\medskip

\item[$\bullet$]
\green{minimal logic $+$ falsum}

%$+$ falsum
\medskip

\item[$\bullet$]
\green{intuitionistic logic}

{\dots} $+$ conjunction $+$ disjunction
\medskip

\item[$\bullet$]
\red{classical logic}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a classical proof}

\textbf{proposition}

\begin{quote}
there are \red{$x$} and \red{$y$} such that $\red{x\not\in{\mathbb Q}}$ and $\red{y\not\in{\mathbb Q}}$, but $\green{x^y\in{\mathbb Q}}$
\end{quote}

\textbf{proof}

\begin{quote}
$\red{\sqrt{2}\not\in{\mathbb Q}}\,$%, but $2\in{\mathbb Q}$
\medskip

$\green{(\sqrt{2}^{\sqrt{2}})\strut^{\sqrt{2}}} = \sqrt{2}^{\,(\!\sqrt{2} \cdot \sqrt{2})} = \sqrt{2}\,\strut^2 = 2 \;\green{\in{\mathbb Q}}$
\medskip

now either $\green{\sqrt{2}^{\sqrt{2}}\in{\mathbb Q}}\,$ or $\red{\sqrt{2}^{\sqrt{2}}\not\in{\mathbb Q}}$
\medskip

in the first case \red{$x = \sqrt{2}$} and \red{$y = \sqrt{2}$} does the job \\
in the second case \red{$x = \sqrt{2}^{\sqrt{2}}$} and \red{$y = \sqrt{2}$} does the job
\end{quote}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the same proof in Mizar}

\begingroup
\scriptsize
\begin{alltt}
theorem
 ex x, y st \red{x is irrational} & \red{y is irrational} & \green{x.^.y is rational}
proof
 set \red{w = sqrt 2};
 w>0 by AXIOMS:22,SQUARE_1:84;
 then A1: \green{(w.^.w).^.w =} w.^.(w*w) by POWER:38
  .= w.^.(w^2) by SQUARE_1:def 3
  .= w.^.2 by SQUARE_1:def 4
  .= w^2 by POWER:53
  .= \green{2} by SQUARE_1:def 4;
 per cases;
 suppose A2: \green{w.^.w is rational};
  take \red{w}, \red{w};
  thus thesis by A2,Th1,INT_2:44;
 end;
 suppose A3: \red{w.^.w is irrational};
  take \red{w.^.w}, \red{w};
  thus thesis by A1,A3,Th1,INT_2:44;
 end;
end;
\end{alltt}
\endgroup
\vspace{-6em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{classical logic}
\setlength{\fboxrule}{1pt}
\begin{itemize}
\item[$\bullet$]
\green{excluded middle}
$$\advirecord{b1}{\red{\fbox{\advirecord{b2}{\black{$A \vee \neg A$}}}}}
\adviplay{b2}$$
\item[$\bullet$]
\green{double negation rule}
$$\neg\neg A \to A$$
\item[$\bullet$]
\green{Peirce's law}
$$((A \to B) \to A) \to A$$
\end{itemize}
\adviwait
\adviplay{b1}
\vfill
\end{slide}

\begin{slide}
\slidetitle{examples of intuitionistic natural deduction}
\begin{itemize}
\item[$\bullet$]
\green{contraposition}
$$(A \to B) \to (\neg B \to \neg A)$$
\item[$\bullet$]
\green{many negations}
$$\neg\neg (\neg\neg A \to A)$$
\end{itemize}
\vfill
\end{slide}
      
\begin{slide}
\slidetitle{examples of classical natural deduction}
\begin{itemize}
\item[$\bullet$]
\green{using $\;\red{A \vee \neg A}\;$ one can prove} $$\neg\neg A \to A$$
\item[$\bullet$]
\green{using $\;\red{\neg\neg A \to A}\;$ one can prove} $$((A \to B) \to A) \to A$$

\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{summary}
\begin{itemize}
\item[$\bullet$]
term \& proof \red{normalization}

\textbf{\green{consistency}}

\item[$\bullet$]
\red{variants} of propositional logic

\textbf{\green{classical logic}}
\end{itemize}
\vfill
\end{slide}

\end{document}