Change my mind about name of third part.

1 files changed, 681 insertions, 0 deletions

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
new file mode 100644
index 0000000..0626337
--- /dev/null
+++ b/transp-inf110-03-quantif.tex
@@ -0,0 +1,681 @@
+%% This is a LaTeX document.  Hey, Emacs, -*- latex -*- , get it?
+\documentclass[mathserif,a4paper,aspectratio=169]{beamer}
+%\documentclass[a4paper]{article}
+%\usepackage[envcountsect,noxcolor]{beamerarticle}
+\usepackage[shorthands=off,french]{babel}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{lmodern}
+\DeclareUnicodeCharacter{00A0}{~}
+\DeclareUnicodeCharacter{2026}{...}
+% Beamer theme:
+\usetheme{Goettingen}
+%\usecolortheme{albatross}
+%\usecolortheme{lily}
+%\setbeamercovered{transparent}
+% A tribute to the worthy AMS:
+\usepackage{amsmath}
+\usepackage{amsfonts}
+\usepackage{amssymb}
+\usepackage{amsthm}
+%
+\usepackage{mathrsfs}
+\usepackage{mathpartir}
+\usepackage{flagderiv}
+%
+\usepackage{graphicx}
+\usepackage{tikz}
+\usetikzlibrary{arrows,automata,calc}
+%
+\newcommand{\itempoint}{\strut\hbox{\color{beamerstructure}\donotcoloroutermaths$\blacktriangleright$}\nobreak\hskip.5em plus.5em\relax}
+\renewcommand{\thefootnote}{\textdagger}
+\newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
+\newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}}
+%\newcommand{\dottedlimp}{\mathbin{\dot\Rightarrow}}
+%\newcommand{\dottedland}{\mathbin{\dot\land}}
+%\newcommand{\dottedlor}{\mathbin{\dot\lor}}
+%\newcommand{\dottedtop}{\mathord{\dot\top}}
+%\newcommand{\dottedbot}{\mathord{\dot\bot}}
+%\newcommand{\dottedneg}{\mathop{\dot\neg}}
+\mathchardef\emdash="07C\relax
+\newcommand{\mpdotsabove}[1]{\inferrule*{\vdots}{#1}}
+%\setlength{\derivskip}{4pt}
+%
+%
+%
+\title{Introduction aux quantificateurs}
+\subtitle{INF110 (Logique et Fondements de l'Informatique)}
+\author[David Madore]{David A. Madore\\
+{\footnotesize Télécom Paris}\\
+\texttt{david.madore@enst.fr}}
+\date{2023–2024}
+\mode<presentation>{%
+\beamertemplatenavigationsymbolsempty
+\usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize\hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}}
+}
+\setbeamercolor{myhighlight}{fg=black,bg=white!90!green}
+\colorlet{mydarkgreen}{green!50!black}
+\begin{document}
+\mode<article>{\maketitle}
+%
+\setlength\abovedisplayskip{2pt plus 2pt minus 2pt}
+\setlength\belowdisplayskip{2pt plus 2pt minus 2pt}
+%
+\begin{frame}
+\titlepage
+{\footnotesize\center{\url{http://perso.enst.fr/madore/inf110/transp-inf110.pdf}}\par}
+{\tiny
+\immediate\write18{sh ./vc > vcline.tex}
+\begin{center}
+Git: \input{vcline.tex}
+\end{center}
+\immediate\write18{echo ' (stale)' >> vcline.tex}
+\par}
+\end{frame}
+%
+\section*{Plan}
+\begin{frame}
+\frametitle{Plan}
+\tableofcontents
+\end{frame}
+%
+\section{Les quantificateurs : discussion informelle}
+\begin{frame}
+\frametitle{Limitations du calcul propositionnel}
+
+\itempoint On a parlé pour l'instant de \textbf{calcul
+  propositionnel}, qui ne connaît que les affirmations logiques et les
+connecteurs propositionnels $\Rightarrow,\land,\lor,\top,\bot$.
+
+\medskip
+
+\itempoint Mais il y a deux notations logiques essentielles en
+mathématiques au-delà de ces connecteurs : les
+\textbf{quantificateurs} $\forall,\exists$, qui :
+\begin{itemize}
+\item prennent une formule $P(x)$ dépendant d'une variable $x$ libre,
+\item lient cette variable pour former une nouvelle formule $\forall
+  x. P(x)$ ou $\exists x. P(x)$.
+\end{itemize}
+
+\medskip
+
+\itempoint Intuitivement, il faut penser à $\forall$ et $\exists$
+comme des « $\land$ et $\lor$ en famille », c'est-à-dire que :
+\begin{itemize}
+\item $\forall x.P(x)$, parfois noté $\bigwedge_x P(x)$ est à $P\land
+  Q$ ce que $\prod_i p_i$ est à $p\times q$,
+\item $\exists x.P(x)$, parfois noté $\bigvee_x P(x)$ est à $P\lor Q$
+  ce que $\sum_i p_i$ est à $p + q$.
+\end{itemize}
+
+\medskip
+
+\itempoint Il existe de \alert{nombreux systèmes logiques} différant
+notamment en \alert{ce qu'on a le droit de quantifier} (qui sont les
+$x$ ici ?).
+
+\smallskip
+
+\textcolor{brown}{Commençons par une discussion informelle de
+  $\forall$ et $\exists$.}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{L'interprétation BHK des quantificateurs}
+
+On a déjà vu l'interprétation informelle des connecteurs, on introduit
+maintenant les quantificateurs :
+
+\begin{itemize}
+\item {\color{darkgray} un témoignage de $P\land Q$, est un témoignage
+  de $P$ et un de $Q$,}
+\item {\color{darkgray} un témoignage de $P\lor Q$, est un témoignage
+  de $P$ ou un de $Q$, et la donnée duquel des deux on a choisi,}
+\item {\color{darkgray} un témoignage de $P\Rightarrow Q$ est un moyen
+  de transformer un témoignage de $P$ en un témoignage de $Q$,}
+\item {\color{darkgray} un témoignage de $\top$ est trivial,} \quad
+  \itempoint {\color{darkgray} un témoignage de $\bot$ n'existe pas,}
+\item un témoignage de $\forall x.P(x)$ est un moyen
+  de transformer un $x$ quelconque en un témoignage de $P(x)$,
+\item un témoignage de $\exists x.P(x)$ est la donnée d'un certain
+  $x_0$ et d'un témoignage de $P(x_0)$.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Curry-Howard pour le $\forall$}
+
+\itempoint On a vu que Curry-Howard fait correspondre
+\alert{conjonction logique} $P\land Q$ {\footnotesize (« un témoignage
+  de $P$ et un de $Q$ »)} avec \alert{type produit} $\sigma\times\tau$
+      {\footnotesize (« une valeur de $\sigma$ et une de $\tau$ »)}.
+
+\medskip
+
+\itempoint De façon analogue, la \alert{quantification universelle}
+$\forall x. P(x)$ {\footnotesize (« une façon de transformer $x$ en un
+  témoignage de $P(x)$ »)}, qui est une sorte de \emph{conjonction en
+famille} $\bigwedge_x P(x)$, correspondra au \alert{type produit en
+  famille} $\prod_x \sigma(x)$ {\footnotesize (« fonction renvoyant
+  une valeur de $\sigma(x)$ pour chaque $x$ »)}.
+
+\medskip
+
+\itempoint Ceci présuppose l'existence de \alert{familles de types} $x
+\mapsto \sigma(x)$ (= types dépendant de quelque chose) dont on puisse
+prendre le produit.
+
+\medskip
+
+\itempoint Une preuve de $\forall x.P(x)$ correspondra à un terme de
+forme $\lambda(x:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
+à $P(x)$.
+
+\medskip
+
+\itempoint Remarquer que $\forall x.P$, si $P$ ne dépend pas de $x$,
+« ressemble » à $I \Rightarrow P$ de la même manière que $\prod_{i\in
+  I} X = X^I$.  {\footnotesize (Les détails dépendent de la nature de
+  la quantification.)}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Curry-Howard pour le $\exists$}
+
+\itempoint On a vu que Curry-Howard fait correspondre
+\alert{conjonction logique} $P\lor Q$ {\footnotesize (« un témoignage
+  de $P$ ou un de $Q$, avec la donnée duquel on a choisi »)} avec
+\alert{type somme} $\sigma+\tau$ {\footnotesize (« une valeur de
+  $\sigma$ ou une de $\tau$, avec un sélecteur entre les deux »)}.
+
+\medskip
+
+\itempoint De façon analogue, la \alert{quantification existentielle}
+$\exists x. P(x)$ {\footnotesize (« la donnée d'un $x_0$ et d'un
+  témoignage de $P(x_0)$ »)}, qui est une sorte de \emph{disjonction
+en famille} $\bigvee_x P(x)$, correspondra au \alert{type somme en
+  famille} $\sum_x \sigma(x)$ {\footnotesize (« donnée d'un $x_0$ et
+  d'une valeur de type $\sigma(x_0)$ »)}.
+
+\medskip
+
+\itempoint Une preuve de $\exists x.P(x)$ correspondra à un terme de
+forme $\langle x_0, \cdots\rangle$, où le type de $(\cdots)$
+correspond à $P(x_0)$.  {\footnotesize (De nouveau, il faut des
+  « familles de types ».)}
+
+\medskip
+
+\itempoint Remarquer que $\exists x.P$, si $P$ ne dépend pas de $x$,
+« ressemble » à $I \times P$ de la même manière que $\sum_{i\in I} X =
+I\times X$.  {\footnotesize (Les détails dépendent de la nature de la
+  quantification.)}
+
+\medskip
+
+\itempoint Mais Curry-Howard atteint ses limites : il n'est pas dit
+que d'une preuve de $\exists x.P(x)$ on \alert{puisse extraire} le
+$x_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
+  (Les détails dépendent du système logique précis considéré {\tiny et
+    si Martin-Löf est dans la salle}.)}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Le problème du $\exists$ et des types sommes}
+
+Doit-on croire à ceci (pour $U$ et $V$ deux types) ?
+\[
+(\forall(x:U).\,\exists(y:V).\,P(x,y))
+\Rightarrow
+(\exists(f:U\Rightarrow V).\,\forall(x:U).\,P(x,f(x)))
+\]
+
+\medskip
+
+{\footnotesize (Cet énoncé porte le nom d'\alert{axiome du choix} :
+  c'est un analogue pour la théorie des types de l'axiome du choix (de
+  Zermelo) en théorie des ensembles.)\par}
+
+\medskip
+
+\itempoint Si on voit $\forall$ et $\exists$ comme des types produit
+et \alert{somme} en famille respectivement, \alert{oui} :
+$\forall(x:U).\,\exists(y:V).\,P(x,y)$ représente une fonction qui
+prend un $x$ de type $U$ et renvoie un $y$ de type $V$ ainsi qu'un
+$P(x,y)$ correspondant : on peut collecter tous ces $y$ en une
+fonction $f : U \Rightarrow V$.
+
+\medskip
+
+\itempoint Si on voit $\exists$ comme un quantificateur
+\alert{logique}, alors \alert{non} : le $y$ renvoyé par $\exists$ ne
+peut servir qu'à l'intérieur d'une preuve, pas être collecté en une
+fonction.
+
+\medskip
+
+\itempoint C'est ici la différence principale entre des systèmes comme
+Coq (où l'énoncé ci-dessus ne sera pas prouvable pour $P : U\times V
+\to \mathit{Prop}$) et les systèmes à la Martin-Löf comme Agda (où
+Curry-Howard est suivi « jusqu'au bout » : il n'y a pas de $\exists$
+uniquement logique).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Imprédicativité}
+
+\itempoint On appelle \textbf{imprédicativité} la possibilité de
+définir une proposition ou un type en quantifiant sur toutes les
+propositions ou types \alert{y compris celui qu'on définit} : c'est
+une forme de circularité.
+
+\medskip
+
+\itempoint P.ex., $\forall (Z:*).\, (Z \Rightarrow A)$ représente le
+type des fonctions capables de renvoyer un type $A$ à partir d'un type
+$Z$ quelconque, y compris celui qu'on définit.
+
+\smallskip
+
+Cette imprédicativité est utile pour définir des constructions sur les
+types.
+
+\medskip
+
+{\footnotesize
+
+Exemples (informellement, et en notant « $*$ » le « type des types »
+imprédicatif) :
+\begin{itemize}
+\item $A \; \cong \; \forall (Z:*).\, (Z \Rightarrow A)$ : donné une
+  valeur $x$ de type $A$ on peut en fabriquer une de type
+  $Z\Rightarrow A$ comme $\lambda(z:Z).\, x$ pour tout type $Z$, mais
+  réciproquement, donné une valeur de type $\forall (Z:*).\, (Z
+  \Rightarrow A)$ on peut l'appliquer à $Z = \top$ pour obtenir une
+  valeur de type $A$.
+\item $A \; \cong \; \forall (Z:*).\, ((A \Rightarrow Z) \Rightarrow
+  Z)$ : dans un sens on fabrique $\lambda(k:A \Rightarrow Z).\, kx$
+  comme pour le CPS, dans l'autre sens, appliquer à $Z = A$ et
+  l'identité.
+\item $\bot \; \cong \; \forall (Z:*).\, Z$
+\quad\itempoint $A\land B \; \cong \; \forall (Z:*).\, ((A \Rightarrow B
+  \Rightarrow Z) \Rightarrow Z)$
+\item $A\lor B \; \cong \; \forall (Z:*).\, ((A \Rightarrow Z)
+  \Rightarrow (B\Rightarrow Z) \Rightarrow Z)$
+\end{itemize}
+
+\par}
+
+\medskip
+
+\itempoint Cela \alert{peut} donner des incohérences logiques
+(paradoxe de Girard).
+
+\end{frame}
+%
+\section{Logique du premier ordre}
+\begin{frame}
+\frametitle{Logique du premier ordre : principe}
+
+\itempoint La \textbf{logique du premier ordre} ou \textbf{calcul des
+  prédicats} est la plus simple qui ajoute les quantificateurs.  Les
+« choses » sur lesquelles on a le droit de quantifier s'appellent des
+\textbf{individus}.
+
+\medskip
+
+\itempoint Côté typage, elle n'est pas très heureuse : les
+« individus » apparaissent comme un type unique, \textit{ad hoc},
+qu'on ne peut presque pas manipuler (la logique ne permet pas de faire
+des couples, fonctions, etc., des individus).
+
+\medskip
+
+\itempoint Néanmoins, elle a une \alert{grande importance
+  mathématique} car le dogme « orthodoxe » est que :
+\begin{center}
+Les mathématiques se font dans la « théorie des ensembles\\de
+Zermelo-Fraenkel en logique du premier ordre » ($\mathsf{ZFC}$).
+\end{center}
+
+Le manque d'expressivité de la logique (pas de couples, fonctions,
+etc.) est \alert{compensé par la théorie elle-même} (constructions
+ensemblistes des couples, fonctions, etc.).
+
+\medskip
+
+{\footnotesize\itempoint La \alert{sémantique} (Tarskienne) de la
+  logique du premier ordre a aussi des propriétés agréables (théorème
+  de complétude de Gödel).\par}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Logique du premier ordre : sortes de variables et syntaxe}
+
+\itempoint En (pure) logique du premier ordre, on a diverses sortes de
+variables :
+\begin{itemize}
+\item les \textbf{variables d'individus} ($x$, $y$, $z$...) en nombre
+  illimité,
+\item les \textbf{variables de prédicats} $n$-aires, ou de
+  \textbf{relations} $n$-aires [entre individus] ($A^{(n)}$,
+  $B^{(n)}$, $C^{(n)}$...), pour chaque entier naturel $n$.
+\end{itemize}
+
+\medskip
+
+\itempoint L'indication d'arité des variables de prédicats est
+généralement omise (elle peut se lire sur la formule).
+
+\medskip
+
+\itempoint Une \textbf{formule} (logique) est (inductivement) :
+\begin{itemize}
+\item l'application $A^{(n)}(x_1,\ldots,x_n)$ d'une variable
+  propositionnelle à $n$ variables d'individus,
+\item l'application d'un connecteur : $(P\Rightarrow Q)$, $(P\land
+  Q)$, $(P\lor Q)$ où $P,Q$ sont deux formules, ou encore $\top$,
+  $\bot$,
+\item une quantification : $\forall x.P$ ou $\exists x.P$, qui
+  \alert{lie} la variable d'individu $x$ dans $P$.
+\end{itemize}
+
+\medskip
+
+\itempoint\alert{On ne peut quantifier que sur les individus
+  (« premier ordre »).}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Exemples de formules du premier ordre}
+
+\itempoint Les \textbf{formules propositionnelles} sont encore des
+formules du premier ordre, en interprétant chaque variable
+propositionnelle comme une variable de prédicat $0$-aire
+(« nullaire ») : $A\land B \Rightarrow B\land A$ par exemple.
+
+\bigskip
+
+Autres exemples (qui seront par ailleurs tous démontrables) :
+\begin{itemize}
+\item $(\forall x.A(x)) \land (\exists x.\top) \Rightarrow (\exists
+  x.A(x))$ (ici, $A$ est un prédicat unaire)
+\item $(\forall x.\neg A(x)) \Leftrightarrow (\neg\exists x.A(x))$ (idem)
+\item $(\exists x.\neg A(x)) \Rightarrow (\neg\forall x.A(x))$ (idem)
+\item $(\exists x.A) \Leftrightarrow (\exists x.\top) \land A$ (ici,
+  $A$ est un prédicat \alert{nullaire})
+\item $(\forall x.A) \Leftrightarrow ((\exists x.\top) \Rightarrow A)$
+  (idem)
+\item $(\exists x.\forall y.B(x,y))\Rightarrow (\forall y.\exists
+  x.B(x,y))$ (ici, $B$ est un prédicat binaire)
+\end{itemize}
+
+\bigskip
+
+\textbf{N.B.} On a suivi la convention que $\forall,\exists$ ont une
+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}$
+(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})
+&$\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})
+\\
+\end{tabular}
+
+\smallskip
+
+\itempoint « $x$ frais » = « $x$ n'apparaît nulle part ailleurs »,
+cf. transp. suivants.
+
+\smallskip
+
+\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}
+%
+\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$ « arbitraire », on peut conclure $\forall x. Q$.
+
+\smallskip
+
+{\footnotesize (Rédaction : « soit $x$ arbitraire (…) 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), dont les variables libres \alert{doivent} apparaître dans
+$\Gamma$.
+
+\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), dont les variables libres \alert{doivent} apparaître dans
+$\Gamma$.
+
+\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$ « arbitraire », on peut conclure $Q$ à partir
+de $\exists x. P$.
+
+\smallskip
+
+{\footnotesize (Rédaction : « on a $\exists x. P(x)$ : soit $x$
+  arbitraire 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}
+%
+\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')}
+}{\vdash (\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}
+%
+\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.  On a $z \vdash \exists x.\top$ (ici $z$ variable qcque)
+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.  On
+\alert{n'a pas} non plus $\forall x.A(x) \Rightarrow \exists x.A(x)$.
+
+\end{frame}
+%
+\end{document}