Continue reworking the introduction to quantifiers (maybe done?).

1 files changed, 156 insertions, 1 deletions

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index b16fb58..867d04d 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -313,6 +313,7 @@ $\exists v. P$.
 \end{frame}
 %
 \begin{frame}
+\label{natural-deduction-rules-with-quantifiers}
 \frametitle{Aperçu d'ensemble des règles de la déduction naturelle}
 
 \begin{tabular}{c|c|c}
@@ -346,7 +347,7 @@ $\forall$
 \\\hline
 $\exists$
 &$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[v\backslash t]}{\Gamma\vdash \exists (v:I).\, Q}$
-&$\inferrule{\Gamma\vdash \exists (v:I). P\\\Gamma, {\color{mydarkgreen}v:I}, {\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash Q}$
+&$\inferrule{\Gamma\vdash \exists (v:I).\, P\\\Gamma, {\color{mydarkgreen}v:I}, {\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash Q}$
 ($v$ \alert{frais})
 \\
 \end{tabular}
@@ -365,6 +366,160 @@ p.ex. $v:I$).
 \end{frame}
 %
 \begin{frame}
+\frametitle{Notations des $\lambda$-termes pour $\forall$}
+
+{\footnotesize
+
+\itempoint On a vu en calcul propositionnel qu'on peut noter les
+démonstrations par des « $\lambda$-termes » qui peuvent ensuite être
+réinterprétés comme des programmes (c'est Curry-Howard).  Complétons
+ces notations pour $\forall, \exists$ :
+
+\par}
+
+\medskip
+
+\itempoint \textcolor{blue}{\underline{Introduction du $\forall$ :}}
+si $s$ désigne une preuve de $Q$ faisant intervenir $v$ variable libre
+de type $I$, on notera $\lambda(v:I).\,s$ la preuve de
+$\forall(v:I).\,Q$ obtenue par introduction du $\forall$.
+\[
+\inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q}
+\]
+
+\medskip
+
+\itempoint \textcolor{blue}{\underline{Élimination du $\forall$ :}} si
+$f$ désigne une preuve de $\forall(v:I).\,Q$ et $t$ un terme de
+type $I$, on notera $ft$ la preuve de $Q[v\backslash t]$ {\footnotesize
+  (c'est-à-dire $Q$ avec $v$ remplacé par $t$)} obtenue par
+élimination du $\forall$ sur ce terme.
+\[
+\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}
+\]
+
+\medskip
+
+\itempoint Ceci est conforme à l'idée de BHK : une preuve de
+$\forall(v:I).\, Q(v)$ prend un $t$ de type $I$ et renvoie une preuve
+de $Q(t)$.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Notations des $\lambda$-termes pour $\exists$}
+
+\itempoint \textcolor{blue}{\underline{Introduction du $\exists$ :}}
+si $t$ désigne un terme de type type $I$ et $z$ une preuve de
+$Q[v\backslash t]$ (pour ce $t$-là, donc), on notera $\langle
+t,z\rangle$ la preuve de $\exists(v:I).\,Q$ obtenue par introduction
+du $\exists$.
+\[
+\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash z \;:\; Q[v\backslash t]}{\Gamma\vdash \langle t,z\rangle \;:\; \exists (v:I).\, Q}
+\]
+
+\medskip
+
+\itempoint \textcolor{blue}{\underline{Élimination du $\exists$ :}} si
+$z$ désigne une preuve de $\exists(v:I).\,P$ et $s$ une preuve de $Q$
+faisant intervenir $v$ variable libre de type $I$ et $h$ hypothèse
+supposant $P$ (pour ce $v$-là, donc), on notera
+$(\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s)$ la
+preuve de $Q$ obtenue par élimination du $\exists$.
+\[
+\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}
+\]
+
+\medskip
+
+\itempoint Ceci est conforme à l'idée de BHK : une preuve de
+$\exists(v:I).\, P(v)$ est la donnée d'un $t$ de type $I$ d'une preuve
+de $Q(t)$.
+
+\end{frame}
+%
+\begin{frame}
+\label{natural-deduction-rules-with-quantifiers-and-notations}
+\frametitle{Récapitulatif des notations}
+
+{\footnotesize(À comparer au
+  transp. \ref{natural-deduction-rules-with-quantifiers}.)\par}
+
+\medskip
+
+\begin{tabular}{c|c|c}
+&Intro&Élim\\\hline
+$\Rightarrow$
+&\scalebox{0.65}{$\inferrule{\Gamma,v:P\vdash s:Q}{\Gamma\vdash \lambda(v:P).\,s : P\Rightarrow Q}$}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash f:P\Rightarrow Q\\\Gamma\vdash z:P}{\Gamma\vdash fz:Q}$}
+\\\hline
+$\land$
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash z_1:Q_1\\\Gamma\vdash z_2:Q_2}{\Gamma\vdash \langle z_1,z_2\rangle : Q_1\land Q_2}$}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash z:Q_1\land Q_2}{\Gamma\vdash \pi_1 z:Q_1}$}
+\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash z:Q_1\land Q_2}{\Gamma\vdash \pi_2 z:Q_2}$}
+\\\hline
+$\lor$
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash z:Q_i}{\Gamma\vdash \iota_i^{(Q_1,Q_2)}z : Q_1\lor Q_2}$} {\footnotesize ($i\in\{1,2\}$)}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash r:P_1\lor P_2\\\Gamma,h_1:P_1\vdash s_1:Q\\\Gamma,h_2:P_2\vdash s_2:Q}{\Gamma\vdash (\texttt{match~}r\texttt{~with~}\iota_1 h_1 \mapsto s_1,\; \iota_2 h_2 \mapsto s_2):Q}$}
+\\\hline
+$\top$
+&\scalebox{0.65}{$\inferrule{\strut}{\Gamma\vdash \bullet:\top}$}
+&\scalebox{0.65}{(néant)}
+\\\hline
+$\bot$
+&\scalebox{0.65}{(néant)}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash r:\bot}{\Gamma\vdash \texttt{exfalso}^{(Q)} r:Q}$}
+\\\hline
+$\forall$
+&\scalebox{0.80}{$\inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q}$}
+&\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}$}
+\\\hline
+$\exists$
+&\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash z \;:\; Q[v\backslash t]}{\Gamma\vdash \langle t,z\rangle \;:\; \exists (v:I).\, Q}$}
+&\scalebox{0.80}{$\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}$}
+\\
+\end{tabular}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Que peut-on quantifier au juste ?}
+
+\itempoint Les règles pour les démonstrations écrites notamment
+transp. \ref{natural-deduction-rules-with-quantifiers} à \ref{natural-deduction-rules-with-quantifiers-and-notations}
+\alert{ne sont pas complètes}, il manque les explications sur les
+« individus » :
+\begin{itemize}
+\item qu'est-ce que c'est que ce « type » $I$ sur lequel on a le droit
+  de quantifier ?
+\item comment forme-t-on des « termes » de type $I$ ?  (d'où sortent
+  ces $\Gamma \vdash t:I$ écrits en gris ?)
+\end{itemize}
+
+\medskip
+
+\itempoint Différents systèmes logiques diffèrent dans la réponse à
+ces questions, notamment, les $8$ systèmes du « $\lambda$-cube » de
+Barendregt (certains mélangent complètement preuves et individus).
+
+\medskip
+
+\itempoint On ne va décrire plus loin que le cas le plus simple, la
+\alert{logique du 1\textsuperscript{er} ordre}, où on ne peut
+quantifier que sur \alert{un seul type} très spécial, l'« univers des
+individus ».
+
+\medskip
+
+\itempoint Évoquons néanmoins auparavant deux problèmes généraux :
+\begin{itemize}
+\item l'extraction d'informations du $\exists$,
+\item l'imprédicativité dans la quantification.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
 \frametitle{Le problème du $\exists$ et des types sommes}
 
 Doit-on croire à ceci (pour $U$ et $V$ deux types) ?