diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 268 |
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} \] |