\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}$}

\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 predicate logic}

\red{logical verification} \\
week 6 \\
2004 10 13

\end{slide}

\begin{slide}
\sectiontitle{advertisement}
\slidetitle{workshop in Nijmegen}
\vspace{0pt}

\begin{center}
%Small TYPES workshop \\
\textbf{Types for Mathematics / Libraries of Formal Mathematics}

November 1--2, 2004 
\bigskip
\end{center}

\green{invited speakers} \\
Bruno Buchberger (of the Theorema system) \\
Bob Constable (of the NuPRL system)
\bigskip

\begin{center}
\quad\red{\url{http://www.cs.ru.nl/fnds/typesworkshop/}} \\
\red{\url{typesworkshop@cs.ru.nl}}
\end{center}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{overview}
\slidetitle{from propositional to predicate logic}

\begin{center}
$\hspace{-2em}$\begin{tabular}{rcl}
\green{first order propositional logic} &\green{$\longleftrightarrow$}&
\green{simply typed lambda calculus} \\
&&
\green{type theory called $\lambda{\to}$} \\
\noalign{\medskip}
\red{first order \textbf{predicate logic}} &$\longleftrightarrow$& type theory called $\lambda P$ \\
\noalign{\medskip}
second order propositional logic &$\longleftrightarrow$& type theory called $\lambda 2$ \\
\noalign{\bigskip}
\noalign{\medskip}
& \rlap{\hspace{-2.5em}\green{inductive types}}\phantom{$\longleftrightarrow$} \\
\noalign{\medskip}
& \rlap{\hspace{-2.5em}program extraction}\phantom{$\longleftrightarrow$}
\end{tabular}$\hspace{-2em}$
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{applications of logic}
\begin{itemize}
\item[$\bullet$]
\textbf{propositional logic}

\red{logical circuits}

\green{correctness of train track switching}
\adviwait
\medskip

\item[$\bullet$]
\textbf{predicate logic}

\red{software correctness}
\quad
`Hoare logic'

\green{correctness of driverless metro in Paris}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{predicate logic}
\slidetitle{`a logic'}

\begin{itemize}
\item[$\bullet$]
\red{syntax} of
\begin{itemize}
\item
terms
\item
formulas
\item
\green{judgments}
\end{itemize}
\item[$\bullet$]
derivation \red{rules}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{terms}

\begin{itemize}
\item[$\bullet$]
$\green{x}$
\item[$\bullet$]
$\red{f}(M_1, \dots, M_n)$
\end{itemize}
\bigskip

symbols $\red{f}$ taken from a fixed finite set of \red{function symbols}

\vfill
\end{slide}

\begin{slide}
\slidetitle{formulas}

\begin{itemize}
\item[$\bullet$]
$\red{P}(M_1, \dots, M_n)$
\item[$\bullet$]
$\top$
\item[$\bullet$]
$\bot$
\item[$\bullet$]
$\neg A$
\item[$\bullet$]
$A \to B$
\item[$\bullet$]
$A \land B$
\item[$\bullet$]
$A \lor B$
\item[$\bullet$]
$\green{\forall x.\, A}$
\item[$\bullet$]
$\green{\exists x.\, A}$
\end{itemize}
\bigskip

symbols $\red{P}$ taken from a fixed finite set of \red{predicate symbols}

\vspace{-2.1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{random example}
\vspace{0pt}

$$\green{(\forall x.\, \exists y.\, P(f(c,y)) \land Q(g(g(x)),y)) \to (\exists z.\, \forall w.\, \neg R(z,w))}$$
\bigskip

here the signature is

\begin{tabular}{ll}
\red{function symbols} & $\{f, c, g, \dots\}$ \\
\red{predicate symbols} & $\{P, Q, R, \dots\}$
\end{tabular}
\bigskip

each symbol has an \blue{arity}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the rules of predicate logic}

\begin{center}
\begin{tabular}{cc}
\llap{\textbf{introduction rules}\hspace{-1.5em}} & \rlap{\hspace{-1.5em}\textbf{elimination rules}} \\
$I\top$ & \\
& $E\bot$ \\
$I[x]\neg$ & $E\neg$ \\
$I[x]{\to}$ & $E{\to}$ \\
$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{rules for $\top$ and $\bot$}
$$
{
\over
\strut
\enskip
\red{\top}
\enskip
}
\enskip
\green{I\top}
\leqno{\mbox{\rlap{\textbf{$\top$ introduction}}}}
$$

$$
{
\begin{array}{c}
\vdots \\
\red{\bot}
\end{array}
\over
\strut
A
}
\enskip
\green{E{\bot}}
\leqno{\mbox{\rlap{\textbf{$\bot$ elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules for $\neg$}
$$
{
\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 \\
\red{\neg A}
\end{array}
\qquad
\begin{array}{c}
\vdots \\
A
\end{array}
\over
\strut
\bot
}
\enskip
\green{E\neg}
\leqno{\mbox{\rlap{\textbf{$\neg$ elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules for $\to$}
$$
{
\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{rules for $\land$}
$$
{
\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{\textbf{$\land$ 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{\textbf{$\land$ elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules for $\lor$}
$$
{
\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{\textbf{$\lor$ 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{\textbf{$\lor$ elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules for $\forall$}
$$
{
\begin{array}{c}
\vdots \\
A
\end{array}
\over
\strut
\red{\forall x.\, A}
}
\enskip
\green{I\forall}
\leqno{\mbox{\rlap{\textbf{$\forall$ introduction}}}}
$$

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

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

\begin{slide}
\slidetitle{rules for $\exists$}
$$
{
\begin{array}{c}
\vdots \\
A[x:=M]
\end{array}
\over
\strut
\red{\exists x.\, A}
}
\enskip
\green{I\exists}
\leqno{\mbox{\rlap{\textbf{$\exists$ introduction}}}}
$$
$$
{
\begin{array}{c}
\vdots \\
\red{\exists x.\, A}
\end{array}
\qquad
\begin{array}{c}
\vdots \\
\forall x.\, (A \to B)
\end{array}
\over
\strut
B
}
\enskip
\green{E\exists}
\leqno{\mbox{\rlap{\textbf{$\exists$ elimination}}}}
$$

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

\begin{slide}
\slidetitle{alternative versions of $E\lor$ and $E\exists$}
$$
\gray{
{
\begin{array}{c}
\\
\vdots \\
\red{A \lor B}
\end{array}
\qquad
\begin{array}{c}
[A] \\
\vdots \\
C
\end{array}
\qquad
\begin{array}{c}
[B] \\
\vdots \\
C
\end{array}
\over
\strut
C
}
%\enskip
%\green{E[x]\lor}
}
\leqno{\mbox{\rlap{\gray{\textbf{$\lor$ elimination}}}}}
$$
$$
\gray{
{
\begin{array}{c}
\\
\vdots \\
\red{\exists x.\, A}
\end{array}
\qquad
\begin{array}{c}
[A] \\
\vdots \\
B
\end{array}
\over
\strut
B
}
}
%\enskip
%\green{E\exists}
\leqno{\mbox{\rlap{\gray{\textbf{$\exists$ elimination}}}}}
$$

\green{\textbf{variable condition:}\quad $x$ not a free variable in $B$ or any open assumption}

\vspace{-.6em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{minimal versus intuitionistic versus classical}
\begin{itemize}
\item[$\bullet$]
\textbf{minimal predicate logic}

just the connectives \red{$\to$} and \red{$\forall$}

\item[$\bullet$]
\textbf{intuitionistic predicate logic}

the system just presented

\item[$\bullet$]
\textbf{classical predicate logic}

add any of
\begin{itemize}
\item[]
\green{$A \lor \neg A$}
\item[]
\green{$\neg\neg A \to A$}
\item[]
\green{$((A \to B) \to A) \to A$}\quad (Peirce's law)
\end{itemize}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{empty domains}

$$
\quad\enskip
{
\begin{array}{c}
{
\displaystyle
{
\over
\strut
\enskip
\top
\enskip
}
\rlap{$
\enskip
I\top
$}
}
\end{array}
\over
\strut
\exists x.\, \top
}
\enskip
\green{I\exists}
%\leqno{\mbox{\rlap{\textbf{$\exists$ introduction}}}}
$$
\vspace{0pt}

\begin{center}
\red{$\exists x.\, \top$ \\
means \\
`there exists an object $x$'}
\end{center}
\bigskip

\green{the $\,I\exists\,$ rule is not valid when the domain is empty!}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{coq}
\slidetitle{terms}
\begin{itemize}
\item[$\bullet$]
\verb|x|
\item[$\bullet$]
\verb|f M1 M2 |\dots\verb| Mn|
\end{itemize}
\bigskip

\green{curried function application: not a first order system!}

\vfill
\end{slide}

\begin{slide}
\slidetitle{formulas}
\begin{itemize}
\item[$\bullet$]
\verb|P M1 M2 |\dots\verb| Mn|
\item[$\bullet$]
\verb|True|
\item[$\bullet$]
\verb|False|
\item[$\bullet$]
\verb|~A|
\item[$\bullet$]
\verb|A -> B|
\item[$\bullet$]
\verb|A /\ B|
\item[$\bullet$]
\verb|A \/ B|
\item[$\bullet$]
\verb|forall x:D, A|
\item[$\bullet$]
\verb|exists x:D, A|
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{tactics}
\begin{center}
\begin{tabular}{rcl}
\noalign{\medskip}
%$I[x]\neg$\quad
$I[x]{\to}$\quad
\red{$I\forall$} && \verb|intro| \\
%$E\neg$\quad
$E{\to}$\quad
\red{$E\forall$} && \verb|apply| \\
$E\bot$\quad
$El\land$\quad
$Er\land$\quad
$E\lor$\quad
\red{$E\exists$} && \verb|elim| \\
$I\land$ && \verb|split| \\
$Il\lor$ && \verb|left| \\
$Ir\lor$ && \verb|right| \\
\red{$I\exists$} && \green{\texttt{exists}} \\
$I\top$ && \verb|exact |\texttt{\green{I}}
\end{tabular}$\qquad\qquad$
\end{center}

\vfill
\end{slide}

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

$$\red{(\forall x.\, P(x) \to Q(x)) \to (\forall x.\, P(x)) \to \forall y.\, Q(y)}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 2}

$$\red{\forall x.\, (P(x) \to \neg (\forall y.\, \neg P(y)))}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 3}

$$\red{(\exists x.\, P(x) \lor Q(x)) \to (\exists x.\, P(x)) \lor (\exists x.\, Q(x))}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{variable conditions}
$$
{
\begin{array}{c}
\vdots \\
A
\end{array}
\over
\strut
\red{\forall x.\, A}
}
\enskip
\green{I\forall}
\leqno{\mbox{\rlap{\textbf{$\forall$ introduction}}}}
$$

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

$$
{
\begin{array}{c}
\vdots \\
\red{\exists x.\, A}
\end{array}
\qquad
\begin{array}{c}
\vdots \\
\forall x.\, (A \to B)
\end{array}
\over
\strut
B
}
\enskip
\green{E\exists}
\leqno{\mbox{\rlap{\textbf{$\exists$ elimination}}}}
$$

\green{\textbf{variable condition:}\quad $x$ not a free variable in $B$}

\vspace{-.8em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{example 4: violates the variable condition of $\,I\forall$}

$$\red{\forall x.\, (P(x) \to \forall x.\, P(x))}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 5: violates the variable condition of $\,E\exists$}

$$\red{\forall x.\, ((\exists x.\, P(x)) \to P(x))}$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{detour elimination}
\slidetitle{detours}
\green{often called `cuts'}
\bigskip

\begin{center}
introduction rule of a connective

\red{directly followed by the}

elimination rule of the \textbf{same} connective
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{detour elimination for $\to$}

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

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

\begin{slide}
\slidetitle{detour elimination for $\land$}

$$
\begin{array}{c}
\displaystyle
{
{
\displaystyle
{
\begin{array}{c}
\green{\vdots} \\
\green{A}
\end{array}
\qquad
\begin{array}{c}
\red{\vdots} \\
\red{B}
\end{array}
\over
\strut
A \land B
}
\enskip
I\land
}
\over
\strut
\green{A}
}
\enskip
El\land
\end{array}
\qquad
\adviwait
\mbox{\Large $\to$}
\qquad\quad
\begin{array}{c}
\green{\vdots} \\
\green{A}
\end{array}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{detour elimination for $\forall$}

$$
\begin{array}{c}
\displaystyle
{
{
\displaystyle
{
\begin{array}{c}
\red{\vdots} \\
\red{A}
\end{array}
\over
\strut
\forall x.\, A
}
\enskip
I\forall
}
\over
\strut
\green{A[x:=M]}
}
\enskip
E\forall
\end{array}
\qquad
\adviwait
\mbox{\Large $\to$}
\qquad\quad
\begin{array}{c}
\red{\vdots}\rlap{$\;^{\textstyle\green{*}}$} \\
\red{A[x:=M]}
\end{array}
\medskip
$$
\hspace{16em}\green{${}^{\textstyle{*}}$ replace $x$ everywhere by $M$}
\adviwait
\bigskip

`proof of \green{$A[x:=M]$} from the \textbf{generalization} \red{$A$}'
\vfill
\end{slide}

\begin{slide}
\sectiontitle{decidability}
\slidetitle{a theorem by G{\"o}del}
\begin{itemize}
\item[$\bullet$]
\textbf{propositional logic}

provability is \red{decidable}
\medskip

\item[$\bullet$]
\textbf{predicate logic}

provability is \red{undecidable}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{first order provers}
\begin{itemize}
\item[$\bullet$]
\textbf{programs that search for proofs in predicate logic}

\red{Otter} \\
Bliksem \\
\red{Vampire} \\
{\small E-SETHEO} \\
\dots
\medskip

\item[$\bullet$]
\textbf{tactics that search for proofs in predicate logic}

\green{coq:}
\red{jprover}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the CASC competition}
\begin{eqnarray*}
\mbox{\green{CASC}} &=& \mbox{CADE ATP System Competition} \\
\mbox{CADE} &=& \mbox{Conference on Automated Deduction} \\
\mbox{ATP} &=& \mbox{Automated Theorem Proving}
\end{eqnarray*}

\green{yearly competition of first order provers}
\medskip

this year the winner was: \red{Vampire} \\
(solved 180 out of 200 problems)

\vfill
\end{slide}

\end{document}