\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{-5em}$}

\def\tto{\to\hspace{-5pt}\!\!\to}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large second order propositional logic}

\red{logical verification} \\
week 11 \\
2004 11 24

\end{slide}

\begin{slide}
\slidetitle{the course}
\begin{center}
$\hspace{-1em}$\begin{tabular}{rcl}
1st order \textbf{propositional} logic &$\leftrightarrow$& {simple} type theory \\
&& \green{$\qquad\lambda{\to}$} \\
\noalign{\medskip}
1st order \textbf{predicate} logic &{$\leftrightarrow$}& {type theory with \textbf{dependent types}} \\
&& \green{$\qquad\lambda P$} \\
\noalign{\medskip}
\red{\textbf{2nd order} propositional logic} &{$\leftrightarrow$}& {\textbf{polymorphic} type theory} \\
&& \green{$\qquad\lambda 2$}
\end{tabular}$\hspace{-1em}$
\end{center}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{2nd order propositional logic}
\slidetitle{propositional logic}

$
\begin{array}{l}
\mbox{\green{$a$} \green{$b$} \green{$c$} \green{\dots}} \\
{\gray{A} \to \gray{B}} \\
\bot \\
\top \\
\neg \gray{A} \\
\gray{A} \land \gray{B} \\
\gray{A} \lor \gray{B}
\end{array}
\hspace{20em}
$
\vfill
\end{slide}

\begin{slide}
\slidetitle{predicate logic}

$
\begin{array}{l}
\ \\
\green{a}\red{(\dots)}\mbox{ }\green{b}\red{(\dots)}\mbox{ }\green{c}\red{(\dots)}\mbox{ }\dots \\
{\gray{A} \to \gray{B}} \\
\bot \\
\top \\
\neg \gray{A} \\
\gray{A} \land \gray{B} \\
\gray{A} \lor \gray{B} \\
\red{\forall\hspace{.6pt}\blue{x}\,.}\, \gray{A} \\
\red{\exists\,\blue{x}\,.}\, \gray{A}
\end{array}
\hspace{2em}
\begin{array}{l}
\mbox{\blue{$x$ $y$ $z$ \dots}} \\
\red{{f}(\dots)}\mbox{ }\red{g}\red{(\dots)}\mbox{ }\red{h}\red{(\dots)}\mbox{ }\red{\dots}
\\\ \\\ \\\ \\\ \\\ \\\ \\\ \\\ 
\end{array}
\hspace{-3em}
$
\vfill
\end{slide}

\begin{slide}
\slidetitle{second order propositional logic}

$
\begin{array}{l}
\mbox{\green{$a$} \green{$b$} \green{$c$} \green{\dots}} \\
{\gray{A} \to \gray{B}} \\
\bot \\
\top \\
\neg \gray{A} \\
\gray{A} \land \gray{B} \\
\gray{A} \lor \gray{B} \\
\red{\forall\hspace{.6pt}\green{a}\,.}\, \gray{A} \\
\red{\exists\,\green{a}\,.}\, \gray{A}
\end{array}
\hspace{20em}
$
\vfill
\end{slide}

\begin{slide}
\slidetitle{example}
$$\green{a} \to \green{a}$$
$$\red{\forall a.}\, a \to a$$
\bigskip
\adviwait

\begin{center}
if \green{it's tuesday}, then \green{it's tuesday}%
\smallskip
\smallskip

for \red{every} proposition, that proposition implies itself
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the rules}

\begin{center}
\begin{tabular}{cc}
\llap{\green{introduction rules}\hspace{-1.5em}} & \rlap{\hspace{-1.5em}\green{elimination rules}} \\
\noalign{\medskip}
$I[x]{\to}$ & $E{\to}$ \\
& $E\bot$ \\
$I\top$ & \\
$I[x]\neg$ & $E\neg$ \\
$I\land$ & $El\land \quad Er\land$ \\
$Il\lor \quad Ir\lor$ & $E\lor$ \\
$\red{I\forall}$ & $\red{E\forall}$ \\
$\red{I\exists}$ & $\red{E\exists}$ \\
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{propositional logic: rules for implication}
$$
{
\begin{array}{c}
[A^x] \\
\vdots \\
B
\end{array}
\over
\strut
\red{A \to B}
}
\enskip
\green{I[x]{\to}}
\leqno{\mbox{\rlap{{implication 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{{implication elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{propositional logic: rules for falsum and truth}
$$
{
\begin{array}{c}
\vdots \\
\red{\bot}
\end{array}
\over
\strut
A
}
\enskip
\green{E{\bot}}
\leqno{\mbox{\rlap{{falsum elimination}}}}
$$

$$
{
\strut
\over
\strut
\enskip
\red{\top}
\enskip
}
\enskip
\green{I\top}
\leqno{\mbox{\rlap{{truth introduction}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{propositional logic: rules for conjunction}
$$
{
\begin{array}{c}
\vdots \\
A
\end{array}
\qquad
\begin{array}{c}
\vdots \\
B
\end{array}
\over
\strut
\red{A \land B}
}
\enskip
\green{I\land}
\leqno{\mbox{\rlap{{conjunction introduction}}}}
$$

$$
{
\begin{array}{c}
\vdots \\
\red{A \land B}
\end{array}
\over
\strut
A
}
\enskip
\green{El\land}
\qquad
{
\begin{array}{c}
\vdots \\
\red{A \land B}
\end{array}
\over
\strut
B
}
\enskip
\green{Er\land}
\leqno{\mbox{\rlap{{conjunction elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{propositional logic: rules for disjunction}
$$
{
\begin{array}{c}
\vdots \\
A
\end{array}
\over
\strut
\red{A \lor B}
}
\enskip
\green{Il\lor}
\qquad
{
\begin{array}{c}
\vdots \\
B
\end{array}
\over
\strut
\red{A \lor B}
}
\enskip
\green{Il\lor}
\leqno{\mbox{\rlap{{disjunction introduction}}}}
$$

$$
{
\begin{array}{c}
\vdots \\
\red{A \lor B}
\end{array}
\qquad
\begin{array}{c}
\vdots \\
A \to C
\end{array}
\qquad
\begin{array}{c}
\vdots \\
B \to C
\end{array}
\over
\strut
C
}
\enskip
\green{E\lor}
\leqno{\mbox{\rlap{{disjunction elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{2nd order propositional logic: rules for universal quantification}
$$
{
\begin{array}{c}
\vdots \\
A
\end{array}
\over
\strut
\red{\forall a.\, A}
}
\enskip
\green{I\forall}
\leqno{\mbox{\rlap{{universal quantification introduction}}}}
$$

\gray{\textbf{variable condition:}\quad $a$ not a free variable in any open assumption}

$$
{
\begin{array}{c}
\vdots \\
\red{\forall a.\, A}
\end{array}
\over
\strut
A[a:=B]
}
\enskip
\green{E\forall}
\leqno{\mbox{\rlap{{universal quantification elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{2nd order propositional logic: rules for existential quantification\toolong}
$$
{
\begin{array}{c}
\vdots \\
A[a:=B]
\end{array}
\over
\strut
\red{\exists a.\, A}
}
\enskip
\green{I\exists}
\leqno{\mbox{\rlap{{existential quantifier introduction}}}}
$$
$$
{
\begin{array}{c}
\vdots \\
\red{\exists a.\, A}
\end{array}
\qquad
\begin{array}{c}
\vdots \\
\forall a.\, (A \to B)
\end{array}
\over
\strut
B
}
\enskip
\green{E\exists}
\leqno{\mbox{\rlap{{existential quantifier elimination}}}}
$$

\gray{\textbf{variable condition:}\quad $a$ not a free variable in $B$}
\vfill
\end{slide}

\begin{slide}
\slidetitle{variable conditions}
\begin{itemize}
\item[$\bullet$]
{for rule \red{$I\forall$}}
\medskip

\textbf{check:} \\
variable does not occur in \green{any of the available assumptions}
\bigskip

\item[$\bullet$]
{for rule \red{$E\exists$}}
\medskip

\textbf{check:} \\
variable does not occur in \green{the conclusion}

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

\begin{slide}
\sectiontitle{examples}
\slidetitle{example 1}

$$\red{(\forall b.\, b) \to a}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 2}

$$\red{a \to \forall b.\, ((a \to b) \to b)}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 3}

$$\red{(\exists b.\, a) \to a}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 4}

$$\red{\exists b. ((a \to b) \lor (b \to a))}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 5}

$$\red{\forall a.\, \forall b.\, ((a \to b) \lor (b \to a))}$$
\bigskip

\green{this needs classical logic}

$$\green{\forall a.\, (a \lor \neg a)}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{non-example 6}

$$\red{a \to \forall a.\, a}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{non-example 7}

$$\red{(\exists a.\, a) \to a}$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{higher order logic}
\slidetitle{the `order' of a variable}

\begin{tabular}{ll}
first order & object \\
\noalign{\medskip}
\red{second order}$\quad$ & set of objects \\
& \red{predicate on objects} \\
& function from objects to objects \\
\noalign{\medskip}
\green{third order} & set of second order objects \\
& \green{predicate on predicates on objects} \\
& function from second order objects to \dots \\
\noalign{\medskip}
etc.
\end{tabular}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example from 2nd order predicate logic}
induction principle for natural numbers

$${\forall} \red{a}.\, \big(\red{a}(\blue{0}) \to ({\forall} \green{m}.\, \red{a}(\green{m}) \to \red{a}(\blue{S}(\green{m}))) \to {\forall} \green{n}.\, \red{a}(\green{n})\big)$$
\bigskip

\begin{tabular}{ll}
$\green{m}$ & \green{1st order variable} \\
$\green{n}$ & \green{1st order variable} \\
$\blue{0}$ & 1st order constant \\
\noalign{\medskip}
$\red{a}$ & \red{2nd order variable} \\
$\blue{S}$ & {2nd order constant}
\end{tabular}

\vfill
\end{slide}

\begin{slide}
\slidetitle{only predicates without arguments}
\vspace{0pt}

\begin{center}
\begin{tabular}{lcl}
\green{quantify over predicates} &$\to$& \textbf{2nd order} predicate logic \\
\noalign{\bigskip}
{\dots} the same \red{without terms} &$\to$& 2nd order \textbf{propositional} logic
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{impredicative encoding of inductive types}
\slidetitle{the connectives in Coq}
\vspace{0pt}

\begin{center}
\begin{tabular}{cl}
$\to$ & hard-wired into the type theory \\
$\forall$ & hard-wired into the type theory \\
\noalign{\medskip}
$\red{\bot}$ & inductive type \\
$\red{\land}$ & inductive type \\
$\red{\lor}$ & inductive type \\
$\exists$ & inductive type
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{inductive definition of \texttt{False}}
\begin{alltt}
Inductive \red{False} : Prop :=  
  .
\end{alltt}

$$\texttt{\green{False\char`\_ind} : }\!\!
\forall a.\, \bot \to a
\bigskip$$

\blue{the constructors are the introduction rules \\
the induction principle is the elimination rule}
\vfill
\end{slide}

\begin{slide}
\slidetitle{inductive definition of \texttt{and}}
\begingroup
\def\\{\char`\\}%
\def\a{$a$}%
\def\b{$b$}%
\def\conj{$a \to b \to a \land b$}%
\begin{alltt}
Inductive \red{and} (\a \b : Prop) : Prop :=  
  \green{conj} : \conj .
\end{alltt}
\endgroup

$$\texttt{\green{and\char`\_ind} : }\!\!
\forall a\;b\;c.\, (a \to b \to c) \to (a \land b) \to c
\bigskip$$

\blue{the constructor is the introduction rule \\
the induction principle gives the elimination rules}
\vfill
\end{slide}

\begin{slide}
\slidetitle{alternative version of conjunction elimination}
$$
{
\begin{array}{c}
\vdots \\
\red{A \land B}
\end{array}
\qquad
\begin{array}{c}
\vdots \\
A \to B \to C
\end{array}
\over
\strut
C
}
\enskip
\green{E\land}
\leqno{\mbox{\rlap{{conjunction elimination: alternative version}}}}
$$
\vspace{-1.15\bigskipamount}
\adviwait

$$
{
\begin{array}{c}
\vdots \\
\red{A \land B}
\end{array}
\over
\strut
A
}
\enskip
\green{El\land}
\qquad
{
\begin{array}{c}
\vdots \\
\red{A \land B}
\end{array}
\over
\strut
B
}
\enskip
\green{Er\land}
\leqno{\mbox{\rlap{{conjunction elimination: normal version}}}}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{inductive definition of \texttt{or}}
\begingroup
\def\\{\char`\\}%
\def\a{$a$}%
\def\b{$b$}%
\def\orintrol{$a \to a \lor b$}%
\def\orintror{$b \to a \lor b$}%
\begin{alltt}
Inductive \red{or} (\a \b : Prop) : Prop :=  
  \green{or_introl} : \orintrol
| \green{or_intror} : \orintror .
\end{alltt}
\endgroup

$$\texttt{\green{or\char`\_ind} : }\!\!
\forall a\;b\;c.\, (a \to c) \to (b \to c) \to (a \lor b) \to c
\bigskip$$

\blue{the constructors are the introduction rules \\
the induction principle is the elimination rule}
\vfill
\end{slide}

\begin{slide}
\slidetitle{impredicative definition of \texttt{False}}

$$\green{\bot} \quad := \quad \red{\forall a.\, a}$$

\bigskip
\bigskip
\adviwait

\blue{induction principle next to impredicative definition}
$$
\begin{array}{c}
\forall a.\, \green{\bot} \to a \\
\forall a.\, \phantom{\bot \to{}} a
\end{array}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{impredicative definition of \texttt{and}}

$$\green{a \land b} \quad := \quad \red{\forall c.\, (a \to b \to c) \to c}$$

\bigskip
\bigskip
\adviwait

\blue{induction principle next to impredicative definition}
$$
\begin{array}{c}
\llap{\gray{$\forall a\;b.\;$}}
\forall c.\, \green{(a \land b)} \to (a \to b \to c) \to c \\
%\llap{\gray{$\lambda a\;b.\;$}}
\forall c.\, \phantom{(a \land b) \to{}} (a \to b \to c) \to c
\end{array}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{impredicative definition of \texttt{or}}

$$\green{a \lor b} \quad := \quad \red{\forall c.\, (a \to c) \to (b \to c) \to c}$$

\bigskip
\bigskip
\adviwait

\blue{induction principle next to impredicative definition}
$$
\begin{array}{c}
\llap{\gray{$\forall a\;b.\;$}}
\forall c.\, \green{(a \lor b)} \to (a \to c) \to (b \to c) \to c \\
%\llap{\gray{$\lambda a\;b.\;$}}
\forall c.\, \phantom{(a \lor b) \to{}} (a \to c) \to (b \to c) \to c
\end{array}
$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{impredicative definitions for other inductive types}
\slidetitle{impredicative definition of the booleans}

$$\red{\forall a.\, a \to a \to a}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{impredicative definition of the natural numbers}

$$\red{\forall a.\, a \to (a \to a) \to a}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{why have inductive types as primitive then?}
\begin{itemize}
\item[$\bullet$]
one can prove less equalities

\item[$\bullet$]
one gets weaker induction principles

\item[$\bullet$]
\red{\textbf{some} people don't like impredicativity}

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

\end{document}