Rework presentation of first-order logic.

1 files changed, 165 insertions, 103 deletions

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 0e1891f..78b6e27 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -643,7 +643,7 @@ imprédicatif) :
 \medskip
 
 \itempoint Côté typage, elle n'est pas très heureuse : les
-« individus » apparaissent comme un type unique, \textit{ad hoc},
+« individus » apparaissent comme un type $I$ unique, \textit{ad hoc},
 qu'on ne peut presque pas manipuler (la logique ne permet pas de faire
 des couples, fonctions, etc., des individus).
 
@@ -695,7 +695,8 @@ généralement omise (elle peut se lire sur la formule).
 \item l'application d'un connecteur : $(P\Rightarrow Q)$, $(P\land
   Q)$, $(P\lor Q)$ où $P,Q$ sont deux formules, ou encore $\top$,
   $\bot$,
-\item une quantification : $\forall x.P$ ou $\exists x.P$, qui
+\item une quantification : $\forall x.P$ ou $\exists x.P$
+  {\footnotesize (pour $\forall (x:I).P$ ou $\exists (x:I).P$)}, qui
   \alert{lie} la variable d'individu $x$ dans $P$.
 \end{itemize}
 
@@ -745,7 +746,46 @@ $B(x,y)$.
 \end{frame}
 %
 \begin{frame}
-\frametitle{Logique du premier ordre : aperçu des règles}
+\frametitle{Remarques sur la logique du premier ordre}
+
+\itempoint Le type $I$ (non écrit) des « individus », le seul sur
+lequel on peut quantifier, est \alert{complètement spécial} en logique
+du premier ordre : on ne l'écrit même pas, on ne peut pas former
+$I\times I$ ni $I\to I$ ni rien d'autre.
+
+\medskip
+
+\itempoint Ce type $I$ ne se « mélange » pas aux relations
+$A,B,C,\ldots$ : les individus vivent dans un monde hermétiquement
+séparé des preuves.
+
+\medskip
+
+\itempoint Dans la variante la plus simple, les seuls termes
+d'individus sont les variables d'individus (i.e., la seule façon
+d'obtenir $t:I$ est d'avoir $t:I$ dans le contexte !).
+
+\medskip
+
+\itempoint On ne suppose pas $I$ habité, i.e. $\exists x.\top$ n'est
+pas démontrable (pas plus que $\forall x. A(x) \Rightarrow \exists
+x. A(x)$).  Cf. transp. \ref{caveat-inhabited-domain}.
+
+\medskip
+
+\itempoint Pour avoir le droit d'écrire $A(x)$, la variable $x$ doit
+avoir été introduite : la règle d'axiome devrait s'écrire
+correctement :
+\[
+\inferrule{ }{\Gamma,\; x:I\vdash x:I}
+\quad\text{~et~}\quad
+\inferrule{\Gamma\vdash x_1:I\\\cdots\\\Gamma\vdash x_n:I}{\Gamma,\;A(x_1,\ldots,x_n)\vdash A(x_1,\ldots,x_n)}
+\]
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Logique du premier ordre : reprise des règles}
 
 \begin{tabular}{c|c|c}
 &Intro&Élim\\\hline
@@ -773,102 +813,19 @@ $\bot$
 (ou pour la logique classique : $\inferrule{\Gamma,\neg Q\vdash \bot}{\Gamma\vdash Q}$)}
 \\\hline
 $\forall$
-&$\inferrule{\Gamma, {\color{mydarkgreen}x}\vdash Q}{\Gamma\vdash \forall x. Q}$ ($x$ \alert{frais})
-&$\inferrule{\Gamma\vdash \forall x. Q}{\Gamma\vdash Q[x\backslash t]}$
-(v.l. de $t$ sont ds $\Gamma$)
+&$\inferrule{\Gamma, {\color{mydarkgreen}x:I}\vdash Q}{\Gamma\vdash \forall x.\, Q}$ ($x$ \alert{frais})
+&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall x.\, Q}{\Gamma\vdash Q[x\backslash t]}$
 \\\hline
 $\exists$
-&$\inferrule{\Gamma\vdash Q[x\backslash t]}{\Gamma\vdash \exists x. Q}$
-(v.l. de $t$ sont ds $\Gamma$)
-&$\inferrule{\Gamma\vdash \exists x. P\\\Gamma, {\color{mydarkgreen}x}, {\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash Q}$
+&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[x\backslash t]}{\Gamma\vdash \exists x.\, Q}$
+&$\inferrule{\Gamma\vdash \exists x.\, P\\\Gamma, {\color{mydarkgreen}x:I}, {\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash Q}$
 ($x$ \alert{frais})
 \\
 \end{tabular}
 
-\smallskip
-
-\itempoint « $x$ frais » = « $x$ n'apparaît nulle part ailleurs »,
-cf. transp. suivants.
-
-\smallskip
-
-\itempoint $\Gamma$ peut contenir des formules et des variables
-d'individus « introduites libres ».
-
-\smallskip
-
-\itempoint « v.l. de $t$ sont ds $\Gamma$ » = les variables libres de
-$t$ doivent être dans $\Gamma$,
-cf. transp. \ref{caveat-inhabited-domain}.
-
-\end{frame}
-%
-\begin{frame}
-\frametitle{Règles d'introduction et d'élimination de $\forall$}
-
-\itempoint \underline{Introduction du $\forall$ :} pour montrer
-$\forall x. Q$, on s'arrange (quitte à renommer la variable liée) pour
-que $x$ soit « frais », c'est-à-dire qu'il n'apparaisse (libre) dans
-\alert{aucune hypothèse} en cours ($\Gamma$) : si on montre $Q$ sur ce
-$x$ « arbitraire », on peut conclure $\forall x. Q$.
-
-\smallskip
-
-{\footnotesize (Rédaction : « soit $x$ arbitraire (…) on a $Q(x)$ ;
-  donc $\forall x. Q(x)$ ».)\par}
-
-\bigskip
-
-\itempoint \underline{Élimination du $\forall$ :} pour utiliser
-$\forall x. Q$, on peut l'appliquer à un $t$ quelconque (en général un
-\alert{terme}, mais ici nos seuls termes d'individus sont des
-variables), dont les variables libres \alert{doivent} apparaître dans
-$\Gamma$.
-
-\smallskip
-
-{\footnotesize (Rédaction : « on a $\forall x. Q(x)$ ; en particulier,
-  on a $Q(t)$ ».)\par}
-
-\end{frame}
-%
-\begin{frame}
-\frametitle{Règles d'introduction et d'élimination de $\exists$}
-
-\itempoint \underline{Introduction du $\exists$ :} pour montrer
-$\exists x. Q$, on peut le montrer sur un $t$ quelconque (en général
-un terme), dont les variables libres \alert{doivent} apparaître dans
-$\Gamma$.
-
-\smallskip
-
-{\footnotesize (Rédaction : « on a $Q(t)$ ; en particulier, on a
-  $\exists x. Q(x)$ ».)\par}
-
-\bigskip
-
-\itempoint \underline{Élimination du $\exists$ :} pour utiliser
-$\exists x. P$ pour montrer une conclusion $Q$, on s'arrange (quitte à
-renommer la variable liée) pour que $x$ soit « frais », c'est-à-dire
-qu'il n'apparaisse (libre) dans \alert{aucune hypothèse} en cours
-($\Gamma$) \alert{ni dans la conclusion} $Q$ : si on montre $Q$ à
-partir de $P$ sur ce $x$ « arbitraire », on peut conclure $Q$ à partir
-de $\exists x. P$.
-
-\smallskip
-
-{\footnotesize (Rédaction : « on a $\exists x. P(x)$ : soit $x$
-  arbitraire tel que $P(x)$ (…) on a $Q$ ; donc $Q$ ».)\par}
-
-\medskip
-
-Cette règle est désagréable comme celle d'élimination du $\lor$ (il
-faut démontrer la même conclusion $Q$ indépendamment du cas).  Elle
-est moins désagréable en calcul des séquents :
-\[
-\inferrule{\Gamma, x, P\vdash Q}{\Gamma, \exists x. P\vdash Q}
-\text{\quad($x$ \alert{frais})}
-\]
+\itempoint Les hypothèses en gris $\Gamma \vdash t:I$ (formation des
+termes) ne sont parfois pas écrites dans les arbres de démonstration,
+mais sont essentielles (cf. transp. \ref{caveat-inhabited-domain}).
 
 \end{frame}
 %
@@ -885,10 +842,10 @@ est moins désagréable en calcul des séquents :
 \\
 \inferrule*[Right={$\exists$Int}]{
 \inferrule*[Right={$\forall$Élim}]{
-\inferrule*[Right=Ax]{ }{x,\;\forall y.B(x,y),\;y' \vdash \forall y.B(x,y)}
-}{x,\;\forall y.B(x,y),\;y' \vdash B(x,y')}
-}{x,\;\forall y.B(x,y),\;y' \vdash \exists x'.B(x',y')}
-}{\exists x.\forall y.B(x,y),\;y' \vdash \exists x'.B(x',y')}
+\inferrule*[Right=Ax]{ }{x:I,\;\forall y.B(x,y),\;y':I \vdash \forall y.B(x,y)}
+}{x:I,\;\forall y.B(x,y),\;y':I \vdash B(x,y')}
+}{x:I,\;\forall y.B(x,y),\;y':I \vdash \exists x'.B(x',y')}
+}{\exists x.\forall y.B(x,y),\;y':I \vdash \exists x'.B(x',y')}
 }{\exists x.\forall y.B(x,y) \vdash \forall y'.\exists x'.B(x',y')}
 }{\vdash (\exists x.\forall y.B(x,y))\Rightarrow (\forall y'.\exists x'.B(x',y'))}
 \]
@@ -950,20 +907,124 @@ Présentation avec les seules conclusions :
 \end{frame}
 %
 \begin{frame}
+\frametitle{Notation des preuves par des $\lambda$-termes}
+
+On reprend la preuve donnée aux transp. précédents :
+
+\begin{center}
+\scalebox{0.8}{\footnotesize
+$
+\inferrule*[left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\forall$Int}]{
+\inferrule*[Left={$\exists$Élim}]{
+\inferrule*[Left={Ax}]{ }{\exists x.\forall y.B(x,y) \vdash \exists x.\forall y.B(x,y)}
+\\
+\inferrule*[Right={$\exists$Int}]{
+\inferrule*[Right={$\forall$Élim}]{
+\inferrule*[Right=Ax]{ }{x:I,\;\forall y.B(x,y),\;y':I \vdash \forall y.B(x,y)}
+}{x:I,\;\forall y.B(x,y),\;y':I \vdash B(x,y')}
+}{x:I,\;\forall y.B(x,y),\;y':I \vdash \exists x'.B(x',y')}
+}{\exists x.\forall y.B(x,y),\;y':I \vdash \exists x'.B(x',y')}
+}{\exists x.\forall y.B(x,y) \vdash \forall y'.\exists x'.B(x',y')}
+}{\vdash (\exists x.\forall y.B(x,y))\Rightarrow (\forall y'.\exists x'.B(x',y'))}
+$
+}
+\end{center}
+
+Avec les notations du
+transp. \ref{natural-deduction-rules-with-quantifiers-and-notations}
+elle se note :
+\[
+\lambda(u:\exists x.\forall y.B(x,y)).\;
+\lambda(y':I).\;
+(\texttt{match~}u\texttt{~with~}\langle x,v\rangle \mapsto
+\langle x,vy'\rangle)
+\]
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Exemples de preuves écrites comme $\lambda$-termes}
+
+\itempoint $(\forall x.(A(x)\Rightarrow C)) \Rightarrow ((\exists
+x. A(x)) \Rightarrow C)$
+
+\smallskip
+
+{\footnotesize Preuve :} $\lambda(f:\forall x.(A(x)\Rightarrow C)).\,
+\lambda(p:\exists x. A(x)).\, (\texttt{match~}p\texttt{~with~}\langle
+x,w\rangle \mapsto fxw)$
+
+\medskip
+
+\itempoint $((\exists x. A(x)) \Rightarrow C) \Rightarrow (\forall
+x.(A(x)\Rightarrow C))$
+
+\smallskip
+
+{\footnotesize Preuve :} $\lambda(g:(\exists x. A(x)) \Rightarrow
+C).\, \lambda(x:I).\, \lambda(u:A(x)).\, g\langle x,u\rangle$
+
+\medskip
+
+{\footnotesize
+
+\itempoint Notamment pour $C$ valant $\bot$ on a prouvé $(\forall
+x.\neg A(x)) \Leftrightarrow \neg(\exists x. A(x))$ ci-dessus.
+
+\par}
+
+\medskip
+
+\itempoint $(\exists x.(A(x)\Rightarrow C)) \Rightarrow ((\forall
+x. A(x)) \Rightarrow C)$
+
+\smallskip
+
+{\footnotesize Preuve :} $\lambda(p:\exists x.(A(x)\Rightarrow C)).\,
+\lambda(f:\forall x. A(x)).\, (\texttt{match~}\!p\!\texttt{~with~}\!\langle
+x,w\rangle \mapsto w(fx))$
+
+\medskip
+
+{\footnotesize
+
+\itempoint Notamment pour $C$ valant $\bot$ on a prouvé $(\exists
+x.\neg A(x)) \Rightarrow \neg(\forall x. A(x))$ ci-dessus.
+
+\par}
+
+\medskip
+
+\itempoint $(\forall x.A(x)) \Rightarrow (\exists x.\top) \Rightarrow
+(\exists x.A(x))$
+
+{\footnotesize Preuve :} $\lambda(f:\forall x.A(x)).\,
+\lambda(p:\exists x.\top).\, (\texttt{match~}p\texttt{~with~}\langle
+x,u\rangle \mapsto \langle x,fx\rangle)$
+
+\medskip
+
+\itempoint $\forall z.\exists x.\top$ (cf. transp. suivant)
+
+{\footnotesize Preuve :} $\lambda(z:I).\,\langle z,\bullet\rangle$
+
+\end{frame}
+%
+\begin{frame}
 \label{caveat-inhabited-domain}
 \frametitle{Pourquoi des variables d'individus avec les hypothèses ?}
 
 \itempoint L'introduction d'une variable d'individu libre porte en
 elle l'hypothèse que \alert{l'univers des individus est habité}
 ($\exists x. \top$).  Ce fait \alert{n'est pas prouvable} sans cette
-hypothèse.  On a $z \vdash \exists x.\top$ (ici $z$ variable qcque)
+hypothèse.  On a $z:I \vdash \exists x.\top$ (ici $z$ variable qcque)
 mais \alert{on n'a pas} $\vdash \exists x.\top$.
 
 \medskip
 
-\itempoint Exiger que les variables d'individus libres dans le terme
-$t$ soient déjà dans $\Gamma$ permet d'écarter la démonstration
-\alert{incorrecte} suivante :
+\itempoint Exiger que de pouvoir former $t:I$ à partir de $\Gamma$
+permet d'écarter la démonstration \alert{incorrecte} suivante :
 \[
 \inferrule*[left={$\exists$Int}]{
 \inferrule*[Left={$\top$Int}]{ }{\vdash\top}
@@ -977,8 +1038,9 @@ terme $z$ pour $t$ dans $\exists$Int) :
 \[
 \inferrule*[left={$\forall$Int}]{
 \inferrule*[Left={$\exists$Int}]{
-\inferrule*[Left={$\top$Int}]{ }{z\vdash\top}
-}{z\vdash\exists x.\top}
+{\color{gray}\inferrule*[Left={Ax}]{ }{z:I\vdash z:I}}\\
+\inferrule*[Right={$\top$Int}]{ }{z:I\vdash\top}
+}{z:I\vdash\exists x.\top}
 }{\vdash\forall z.\exists x.\top}
 \]