From e58127820b750b17cdaab6674b1430dbd90adcb7 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Mon, 18 Dec 2023 18:51:38 +0100 Subject: Example proof in first-order logic. --- transp-inf110-03-super.tex | 94 ++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 86 insertions(+), 8 deletions(-) (limited to 'transp-inf110-03-super.tex') diff --git a/transp-inf110-03-super.tex b/transp-inf110-03-super.tex index f0f136a..b255e1a 100644 --- a/transp-inf110-03-super.tex +++ b/transp-inf110-03-super.tex @@ -21,7 +21,7 @@ % \usepackage{mathrsfs} \usepackage{mathpartir} -%\usepackage{flagderiv} +\usepackage{flagderiv} % \usepackage{graphicx} \usepackage{tikz} @@ -363,7 +363,8 @@ $\top$ \\\hline $\bot$ &\scalebox{0.65}{(néant)} -&\scalebox{0.65}{$\inferrule{\Gamma\vdash \bot}{\Gamma\vdash Q}$} +&\scalebox{0.65}{$\inferrule{\Gamma\vdash \bot}{\Gamma\vdash Q}$ +(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}) @@ -383,7 +384,7 @@ cf. transp. suivant \smallskip -$\Gamma$ peut contenir des formules et des variables d'individus. +$\Gamma$ peut contenir des formules et des variables d'individus « introduites libres ». \end{frame} % @@ -394,11 +395,11 @@ $\Gamma$ peut contenir des formules et des variables d'individus. $\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$. +$x$ « arbitraire », on peut conclure $\forall x. Q$. \smallskip -{\footnotesize (Rédaction : « soit $x$ quelconque (…) on a $Q(x)$ ; +{\footnotesize (Rédaction : « soit $x$ arbitraire (…) on a $Q(x)$ ; donc $\forall x. Q(x)$ ».)\par} \bigskip @@ -434,13 +435,13 @@ $\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 +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$ tel - que $P(x)$ (…) on a $Q$ ; donc $Q$ ».)\par} +{\footnotesize (Rédaction : « on a $\exists x. P(x)$ : soit $x$ + arbitraire tel que $P(x)$ (…) on a $Q$ ; donc $Q$ ».)\par} \medskip @@ -452,6 +453,83 @@ est moins désagréable en calcul des séquents : \text{\quad($x$ \alert{frais})} \] +\end{frame} +% +\begin{frame} +\frametitle{Exemple de preuve en logique du premier ordre} + +{\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,\;\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')} +}{\exists x.\forall y.B(x,y) \vdash \forall y'.\exists x'.B(x',y')} +}{(\exists x.\forall y.B(x,y))\Rightarrow (\forall y'.\exists x'.B(x',y'))} +\] + +} + +Présentation avec les seules conclusions : + +{\footnotesize + +\[ +\inferrule*[left={$\Rightarrow$Int(\textcolor{mydarkgreen}{$u$})}]{ +\inferrule*[Left={$\forall$Int(\textcolor{mydarkgreen}{$y'$})}]{ +\inferrule*[Left={$\exists$Élim(\textcolor{mydarkgreen}{$x$},\textcolor{mydarkgreen}{$v$})}]{ +\inferrule*[Left={\textcolor{mydarkgreen}{$u$}}]{ }{\exists x.\forall y.B(x,y)} +\\ +\inferrule*[Right={$\exists$Int}]{ +\inferrule*[Right={$\forall$Élim}]{ +\inferrule*[Right={\textcolor{mydarkgreen}{$v$}}]{ }{\forall y.B(x,y)} +}{B(x,y')} +}{\exists x'.B(x',y')} +}{\exists x'.B(x',y')} +}{\forall y'.\exists x'.B(x',y')} +}{(\exists x.\forall y.B(x,y))\Rightarrow (\forall y'.\exists x'.B(x',y'))} +\] + +} + +\end{frame} +% +\begin{frame} +\frametitle{Exemple de preuve : présentation drapeau} + +{\footnotesize +\begin{flagderiv}[example-1st-order-proof] +\assume{mainhyp}{\exists x.\forall y.B(x,y)}{} +\assume{vary}{y'}{} +\assume{exhyp}{x,\;\forall y.B(x,y)}{} +\step{bare}{B(x,y')}{$\forall$Élim sur \ref{exhyp} et $y$} +\step{exbare}{\exists x'.B(x',y')}{$\exists$Int sur $x$ et \ref{bare}} +\conclude{extrude}{\exists x'.B(x',y')}{$\exists$Elim sur \ref{mainhyp} de \ref{exhyp} dans \ref{exbare}} +\conclude{mainconc}{\forall y'.\exists x'.B(x',y')}{$\forall$Intro de \ref{vary} dans \ref{extrude}} +\conclude{}{(\exists x.\forall y.B(x,y))\Rightarrow(\forall y'.\exists x'.B(x',y'))}{$\Rightarrow$Intro de \ref{mainhyp} dans \ref{mainconc}} +\end{flagderiv} +\par} + +\smallskip + +{\footnotesize « Supposons $\exists x.\forall y.B(x,y)$. Considérons + un $y'$ arbitraire. Considérons un $x$ tel que $\forall y.B(x,y)$. + En particulier, on a $B(x,y')$. En particulier, $\exists + x'.B(x',y')$. Or on pouvait trouver un tel $x$ car $\exists + x.\forall y.B(x,y)$, donc on a bien la conclusion $\exists + x'.B(x',y')$. Le choix de $y'$ étant arbitraire, $\forall + y'. \exists x'. B(x',y')$. Finalement, on a prouvé $(\exists + x.\forall y.B(x,y))\Rightarrow(\forall y'.\exists + x'.B(x',y'))$. »\par\strut\par} + \end{frame} % \end{document} -- cgit v1.2.3