The problem of the inhabitedness of the domain.

1 files changed, 57 insertions, 6 deletions

diff --git a/transp-inf110-03-super.tex b/transp-inf110-03-super.tex
index b255e1a..45d1e7c 100644
--- a/transp-inf110-03-super.tex
+++ b/transp-inf110-03-super.tex
@@ -369,9 +369,11 @@ $\bot$
 $\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$)
 \\\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}$
 ($x$ \alert{frais})
 \\
@@ -379,12 +381,19 @@ $\exists$
 
 \smallskip
 
-« $x$ frais » = « $x$ n'apparaît nulle part ailleurs »,
-cf. transp. suivant
+\itempoint « $x$ frais » = « $x$ n'apparaît nulle part ailleurs »,
+cf. transp. suivants.
 
 \smallskip
 
-$\Gamma$ peut contenir des formules et des variables d'individus « introduites libres ».
+\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}
 %
@@ -407,7 +416,8 @@ $x$ « arbitraire », on peut conclure $\forall x. Q$.
 \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.
+variables), dont les variables libres \alert{doivent} apparaître dans
+$\Gamma$.
 
 \smallskip
 
@@ -421,7 +431,8 @@ variables), qui \alert{peut} apparaître dans les hypothèses.
 
 \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.
+un terme), dont les variables libres \alert{doivent} apparaître dans
+$\Gamma$.
 
 \smallskip
 
@@ -473,7 +484,7 @@ est moins désagréable en calcul des séquents :
 }{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'))}
+}{\vdash (\exists x.\forall y.B(x,y))\Rightarrow (\forall y'.\exists x'.B(x',y'))}
 \]
 
 }
@@ -532,4 +543,44 @@ Présentation avec les seules conclusions :
 
 \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.  Autrement dit : $z \vdash \exists x.\top$ (pour $z$ une
+variable quelconque) 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 :
+\[
+\inferrule*[left={$\exists$Int}]{
+\inferrule*[Left={$\top$Int}]{ }{\vdash\top}
+}{\vdash\exists x.\top}
+\]
+
+\medskip
+
+\itempoint En revanche, celle-ci \alert{est correcte} (en utilisant le
+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}
+}{\vdash\forall z.\exists x.\top}
+\]
+
+\medskip
+
+\textbf{N.B.} Ces problèmes n'ont rien à voir avec la logique
+intuitionniste, ils sont identiques en logique classique.
+
+\end{frame}
+%
 \end{document}