diff options
| -rw-r--r-- | transp-inf110-03-super.tex | 121 |
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} |