The rules of first-order logic.

1 files changed, 121 insertions, 0 deletions

diff --git a/transp-inf110-03-super.tex b/transp-inf110-03-super.tex
index db76f2c..f0f136a 100644
--- a/transp-inf110-03-super.tex
+++ b/transp-inf110-03-super.tex
@@ -331,6 +331,127 @@ priorité plus faible que les connecteurs
 $\Rightarrow,\lor,\land,\neg$.  Tout le monde n'est pas d'accord avec
 cette convention !
 
+\smallskip
+
+\textbf{N.B.2 :} Il serait peut-être préférable de noter $Bxy$ que
+$B(x,y)$.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Logique du premier ordre : aperçu des règles}
+
+\begin{tabular}{c|c|c}
+&Intro&Élim\\\hline
+$\Rightarrow$
+&\scalebox{0.65}{$\inferrule{\Gamma,{\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash P\Rightarrow Q}$}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash P\Rightarrow Q\\\Gamma\vdash P}{\Gamma\vdash Q}$}
+\\\hline
+$\land$
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\\\Gamma\vdash Q_2}{\Gamma\vdash Q_1\land Q_2}$}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_1}$}
+\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_2}$}
+\\\hline
+$\lor$
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1}{\Gamma\vdash Q_1\lor Q_2}$}
+\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_2}{\Gamma\vdash Q_1\lor Q_2}$}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash P_1\lor P_2\\\Gamma,{\color{mydarkgreen}P_1}\vdash Q\\\Gamma,{\color{mydarkgreen}P_2}\vdash Q}{\Gamma\vdash Q}$}
+\\\hline
+$\top$
+&\scalebox{0.65}{$\inferrule{\strut}{\Gamma\vdash \top}$}
+&\scalebox{0.65}{(néant)}
+\\\hline
+$\bot$
+&\scalebox{0.65}{(néant)}
+&\scalebox{0.65}{$\inferrule{\Gamma\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]}$
+\\\hline
+$\exists$
+&$\inferrule{\Gamma\vdash Q[x\backslash t]}{\Gamma\vdash \exists x. Q}$
+&$\inferrule{\Gamma\vdash \exists x. P\\\Gamma, {\color{mydarkgreen}x}, {\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash Q}$
+($x$ \alert{frais})
+\\
+\end{tabular}
+
+\smallskip
+
+« $x$ frais » = « $x$ n'apparaît nulle part ailleurs »,
+cf. transp. suivant
+
+\smallskip
+
+$\Gamma$ peut contenir des formules et des variables d'individus.
+
+\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$ « quelconque », on peut conclure $\forall x. Q$.
+
+\smallskip
+
+{\footnotesize (Rédaction : « soit $x$ quelconque (…) 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), qui \alert{peut} apparaître dans les hypothèses.
+
+\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), qui \alert{peut} apparaître dans les hypothèses.
+
+\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$ « quelconque », on peut conclure $Q$ à partir
+de $\exists x. P$.
+
+\smallskip
+
+{\footnotesize (Rédaction : « on a $\exists x. P(x)$ : soit $x$ 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})}
+\]
+
 \end{frame}
 %
 \end{document}