%% 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(v)$ dépendant d'une variable $v$ libre
  {\footnotesize (de type $I$)},
\item lient cette variable, pour former une nouvelle formule :
  $\forall (v:I). P(v)$ ou $\exists (v:I). P(v)$
  {\footnotesize (parfois juste $\forall v. P(v)$ et $\exists v. P(v)$)}.
\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 v.P(v)$, parfois noté $\bigwedge_v P(v)$ est à $P\land
  Q$ ce que $\prod_i p_i$ est à $p\times q$,
\item $\exists v.P(v)$, parfois noté $\bigvee_v P(v)$ 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
$v$ ici ? quel est leur domaine $I$ ?).

\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 v.P(v)$ est un moyen
  de transformer un $x$ quelconque en un témoignage de $P(x)$,
\item un témoignage de $\exists v.P(v)$ est la donnée d'un certain
  $t_0$ et d'un témoignage de $P(t_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 v. P(v)$ {\footnotesize (« une façon de transformer $v$ en un
  témoignage de $P(v)$ »)}, qui est une sorte de \emph{conjonction en
famille} $\bigwedge_v P(v)$, correspondra au \alert{type produit en
  famille} $\prod_v \sigma(v)$ {\footnotesize (« fonction renvoyant
  une valeur de $\sigma(v)$ pour chaque $v$ »)}.

\medskip

\itempoint Ceci présuppose l'existence de \alert{familles de types} $v
\mapsto \sigma(v)$ (= types dépendant de quelque chose) dont on puisse
prendre le produit.

\medskip

\itempoint Une preuve de $\forall (v:I).P(v)$ correspondra à un terme
de forme $\lambda(v:I).\,(\cdots)$, où le type de $(\cdots)$
correspond à $P(v)$.

\medskip

\itempoint Remarquer que $\forall (v:I).P$, si $P$ ne dépend pas de
$v$, « ressemble » à $I \Rightarrow P$ de la même manière que
$\prod_{i\in I} S = S^I$ (ensemblistement ou numériquement).
           {\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{disjonction 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 v. P(v)$ {\footnotesize (« la donnée d'un $t_0$ et d'un
  témoignage de $P(t_0)$ »)}, qui est une sorte de \emph{disjonction
en famille} $\bigvee_v P(v)$, correspondra au \alert{type somme en
  famille} $\sum_v \sigma(v)$ {\footnotesize (« donnée d'un $t_0$ et
  d'une valeur de type $\sigma(t_0)$ »)}.

\medskip

\itempoint Une preuve de $\exists (v:I).P(v)$ correspondra à un terme de
forme $\langle t_0, \cdots\rangle$, où le type de $(\cdots)$
correspond à $P(t_0)$.  {\footnotesize (De nouveau, il faut des
  « familles de types ».)}

\medskip

\itempoint Remarquer que $\exists (v:I).P$, si $P$ ne dépend pas de $v$,
« ressemble » à $I \times P$ de la même manière que $\sum_{i\in I} S =
I\times S$.  {\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 v.P(v)$ on \alert{puisse extraire} le
$t_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{Règles d'introduction et d'élimination de $\forall$}

{\footnotesize\textcolor{orange}{Les règles ci-dessous (et
    transp. suivant) sont \alert{incomplètes} : il manque des
    explications sur le type $I$ sur lequel on quantifie et comment on
    peut en former des « termes ».}\par}

\medskip

\itempoint \underline{Introduction du $\forall$ :} pour montrer
$\forall (v:I).\, Q$, on s'arrange (quitte à renommer la variable
liée) pour que $v:I$ soit « frais », c'est-à-dire qu'il n'apparaisse
(libre) dans \alert{aucune hypothèse} en cours : si on montre $Q$ sur
ce $v$ « arbitraire », on peut conclure $\forall (v:I).\, Q$.

\smallskip

{\footnotesize (Rédaction : « soit $v$ arbitraire (…) on a $Q(v)$ ;
  donc $\forall (v:I).\, Q(v)$ ».)\par}

\medskip

\textcolor{teal}{Ceci donnera un $\lambda$-terme noté
  $\lambda(v:I).(\cdots)$ comme l'ouverture d'une hypothèse.}

\bigskip

\itempoint \underline{Élimination du $\forall$ :} pour utiliser
$\forall (v:I). Q$, on peut l'appliquer à un $t$ quelconque (un
\alert{terme} de type $I$).

\smallskip

{\footnotesize (Rédaction : « on a $\forall (v:I). Q(v)$ et $t$ de
  type $I$ ; en particulier, on a $Q(t)$ ».)\par}

\medskip

\textcolor{teal}{Ceci donnera un $\lambda$-terme noté $ft$ comme
  l'application d'une implication.}

\end{frame}
%
\begin{frame}
\frametitle{Règles d'introduction et d'élimination de $\exists$}

\itempoint \underline{Introduction du $\exists$ :} pour montrer
$\exists (v:I). Q$, on peut le montrer sur un terme $t$ quelconque de
type $I$.

\smallskip

{\footnotesize (Rédaction : « pour ce $t$ de type $I$ on a $Q(t)$ ; en
  particulier, on a $\exists (v:I). Q(v)$ ».)\par}

\medskip

\textcolor{teal}{Ceci donnera un $\lambda$-terme noté $\langle
  t,\cdots\rangle$ comme pour une conjonction.}

\bigskip

\itempoint \underline{Élimination du $\exists$ :} pour utiliser
$\exists (v:I). P(v)$ pour montrer une conclusion $Q$, on s'arrange
(quitte à renommer la variable liée) pour que $v$ soit « frais »,
c'est-à-dire qu'il n'apparaisse (libre) dans \alert{aucune hypothèse}
en cours \alert{ni dans la conclusion} $Q$ : si on montre $Q$ à partir
de $P$ sur ce $v$ « arbitraire », on peut conclure $Q$ à partir de
$\exists v. P$.

\smallskip

{\footnotesize (Rédaction : « on a $\exists (v:I). P(v)$ : soit $v$
  arbitraire tel que $P(v)$ : (…) on a $Q$ ; donc $Q$ ».)\par}

\medskip

\textcolor{teal}{Ceci donnera un $\lambda$-terme noté
  $(\texttt{match~}\cdots\texttt{~with~}\langle v,h\rangle \mapsto
  \cdots)$.}

\end{frame}
%
\begin{frame}
\label{natural-deduction-rules-with-quantifiers}
\frametitle{Aperçu d'ensemble des règles de la déduction naturelle}

\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}v:I}\vdash Q}{\Gamma\vdash \forall (v:I).\, Q}$ ($v$ \alert{frais})
&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall (v:I).\, Q}{\Gamma\vdash Q[v\backslash t]}$
\\\hline
$\exists$
&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[v\backslash t]}{\Gamma\vdash \exists (v:I).\, Q}$
&$\inferrule{\Gamma\vdash \exists (v:I).\, P\\\Gamma, {\color{mydarkgreen}v:I}, {\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash Q}$
($v$ \alert{frais})
\\
\end{tabular}

\smallskip

\itempoint « $v$ frais » = « $v$ n'apparaît nulle part ailleurs »
(cf. transp. précédents).

\smallskip

\itempoint Le contexte $\Gamma$ peut contenir des formules
(hypothèses) et des variables d'« individus » (avec leur type,
p.ex. $v:I$).

\end{frame}
%
\begin{frame}
\frametitle{Notations des $\lambda$-termes pour $\forall$}

{\footnotesize

\itempoint On a vu en calcul propositionnel qu'on peut noter les
démonstrations par des « $\lambda$-termes » qui peuvent ensuite être
réinterprétés comme des programmes (c'est Curry-Howard).  Complétons
ces notations pour $\forall, \exists$ :

\par}

\medskip

\itempoint \textcolor{blue}{\underline{Introduction du $\forall$ :}}
si $s$ désigne une preuve de $Q$ faisant intervenir $v$ variable libre
de type $I$, on notera $\lambda(v:I).\,s$ la preuve de
$\forall(v:I).\,Q$ obtenue par introduction du $\forall$.
\[
\inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q}
\]

\medskip

\itempoint \textcolor{blue}{\underline{Élimination du $\forall$ :}} si
$f$ désigne une preuve de $\forall(v:I).\,Q$ et $t$ un terme de
type $I$, on notera $ft$ la preuve de $Q[v\backslash t]$ {\footnotesize
  (c'est-à-dire $Q$ avec $v$ remplacé par $t$)} obtenue par
élimination du $\forall$ sur ce terme.
\[
\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}
\]

\medskip

\itempoint Ceci est conforme à l'idée de BHK : une preuve de
$\forall(v:I).\, Q(v)$ prend un $t$ de type $I$ et renvoie une preuve
de $Q(t)$.

\end{frame}
%
\begin{frame}
\frametitle{Notations des $\lambda$-termes pour $\exists$}

\itempoint \textcolor{blue}{\underline{Introduction du $\exists$ :}}
si $t$ désigne un terme de type type $I$ et $z$ une preuve de
$Q[v\backslash t]$ (pour ce $t$-là, donc), on notera $\langle
t,z\rangle$ la preuve de $\exists(v:I).\,Q$ obtenue par introduction
du $\exists$.
\[
\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash z \;:\; Q[v\backslash t]}{\Gamma\vdash \langle t,z\rangle \;:\; \exists (v:I).\, Q}
\]

\medskip

\itempoint \textcolor{blue}{\underline{Élimination du $\exists$ :}} si
$z$ désigne une preuve de $\exists(v:I).\,P$ et $s$ une preuve de $Q$
faisant intervenir $v$ variable libre de type $I$ et $h$ hypothèse
supposant $P$ (pour ce $v$-là, donc), on notera
$(\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s)$ la
preuve de $Q$ obtenue par élimination du $\exists$.
\[
\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}
\]

\medskip

\itempoint Ceci est conforme à l'idée de BHK : une preuve de
$\exists(v:I).\, P(v)$ est la donnée d'un $t$ de type $I$ d'une preuve
de $Q(t)$.

\end{frame}
%
\begin{frame}
\label{natural-deduction-rules-with-quantifiers-and-notations}
\frametitle{Récapitulatif des notations}

{\footnotesize(À comparer au
  transp. \ref{natural-deduction-rules-with-quantifiers}.)\par}

\medskip

\begin{tabular}{c|c|c}
&Intro&Élim\\\hline
$\Rightarrow$
&\scalebox{0.65}{$\inferrule{\Gamma,v:P\vdash s:Q}{\Gamma\vdash \lambda(v:P).\,s : P\Rightarrow Q}$}
&\scalebox{0.65}{$\inferrule{\Gamma\vdash f:P\Rightarrow Q\\\Gamma\vdash z:P}{\Gamma\vdash fz:Q}$}
\\\hline
$\land$
&\scalebox{0.65}{$\inferrule{\Gamma\vdash z_1:Q_1\\\Gamma\vdash z_2:Q_2}{\Gamma\vdash \langle z_1,z_2\rangle : Q_1\land Q_2}$}
&\scalebox{0.65}{$\inferrule{\Gamma\vdash z:Q_1\land Q_2}{\Gamma\vdash \pi_1 z:Q_1}$}
\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash z:Q_1\land Q_2}{\Gamma\vdash \pi_2 z:Q_2}$}
\\\hline
$\lor$
&\scalebox{0.65}{$\inferrule{\Gamma\vdash z:Q_i}{\Gamma\vdash \iota_i^{(Q_1,Q_2)}z : Q_1\lor Q_2}$} {\footnotesize ($i\in\{1,2\}$)}
&\scalebox{0.65}{$\inferrule{\Gamma\vdash r:P_1\lor P_2\\\Gamma,h_1:P_1\vdash s_1:Q\\\Gamma,h_2:P_2\vdash s_2:Q}{\Gamma\vdash (\texttt{match~}r\texttt{~with~}\iota_1 h_1 \mapsto s_1,\; \iota_2 h_2 \mapsto s_2):Q}$}
\\\hline
$\top$
&\scalebox{0.65}{$\inferrule{\strut}{\Gamma\vdash \bullet:\top}$}
&\scalebox{0.65}{(néant)}
\\\hline
$\bot$
&\scalebox{0.65}{(néant)}
&\scalebox{0.65}{$\inferrule{\Gamma\vdash r:\bot}{\Gamma\vdash \texttt{exfalso}^{(Q)} r:Q}$}
\\\hline
$\forall$
&\scalebox{0.80}{$\inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q}$}
&\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}$}
\\\hline
$\exists$
&\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash z \;:\; Q[v\backslash t]}{\Gamma\vdash \langle t,z\rangle \;:\; \exists (v:I).\, Q}$}
&\scalebox{0.80}{$\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}$}
\\
\end{tabular}

\end{frame}
%
\begin{frame}
\frametitle{Que peut-on quantifier au juste ?}

\itempoint Les règles pour les démonstrations écrites notamment
transp. \ref{natural-deduction-rules-with-quantifiers} à \ref{natural-deduction-rules-with-quantifiers-and-notations}
\alert{ne sont pas complètes}, il manque les explications sur les
« individus » :
\begin{itemize}
\item qu'est-ce que c'est que ce « type » $I$ sur lequel on a le droit
  de quantifier ?
\item comment forme-t-on des « termes » de type $I$ ?  (d'où sortent
  ces $\Gamma \vdash t:I$ écrits en gris ?)
\end{itemize}

\medskip

\itempoint Différents systèmes logiques diffèrent dans la réponse à
ces questions, notamment, les $8$ systèmes du « $\lambda$-cube » de
Barendregt (certains mélangent complètement preuves et individus).

\medskip

\itempoint On ne va décrire plus loin que le cas le plus simple, la
\alert{logique du 1\textsuperscript{er} ordre}, où on ne peut
quantifier que sur \alert{un seul type} très spécial, l'« univers des
individus ».

\medskip

\itempoint Évoquons néanmoins auparavant deux problèmes généraux :
\begin{itemize}
\item l'extraction d'informations du $\exists$,
\item l'imprédicativité dans la quantification.
\end{itemize}

\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, et cet énoncé est prouvable).

\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}