From e58127820b750b17cdaab6674b1430dbd90adcb7 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
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(-)

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