%% 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)))
\]
{\footnotesize
\[
\begin{aligned}
\text{« preuve(?) » :~}
\lambda(h:\cdots).\,
\langle
&\lambda(x:U).\,
(\texttt{match~}hx\texttt{~with~}\langle v,z\rangle \mapsto v),\\
&\lambda(x:U).\,
(\texttt{match~}hx\texttt{~with~}\langle v,z\rangle \mapsto z)
\rangle
\end{aligned}
\]
\par}

\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

{\footnotesize

\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 comme indiqué).

\par}

\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 $I$ 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$
  {\footnotesize (pour $\forall (x:I).P$ ou $\exists (x:I).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{Remarques sur la logique du premier ordre}

\itempoint Le type $I$ (non écrit) des « individus », le seul sur
lequel on peut quantifier, est \alert{complètement spécial} en logique
du premier ordre : on ne l'écrit même pas, on ne peut pas former
$I\times I$ ni $I\to I$ ni rien d'autre.

\medskip

\itempoint Ce type $I$ ne se « mélange » pas aux relations
$A,B,C,\ldots$ : les individus vivent dans un monde hermétiquement
séparé des preuves.

\medskip

\itempoint Dans la variante la plus simple, les seuls termes
d'individus sont les variables d'individus (i.e., la seule façon
d'obtenir $t:I$ est d'avoir $t:I$ dans le contexte !).

\medskip

\itempoint On ne suppose pas $I$ habité, i.e. $\exists x.\top$ n'est
pas démontrable (pas plus que $\forall x. A(x) \Rightarrow \exists
x. A(x)$).  Cf. transp. \ref{caveat-inhabited-domain}.

\medskip

\itempoint Pour avoir le droit d'écrire $A(x)$, la variable $x$ doit
avoir été introduite : la règle d'axiome devrait s'écrire
correctement :
\[
\inferrule{ }{\Gamma,\; x:I\vdash x:I}
\quad\text{~et~}\quad
\inferrule{\Gamma\vdash x_1:I\\\cdots\\\Gamma\vdash x_n:I}{\Gamma,\;A(x_1,\ldots,x_n)\vdash A(x_1,\ldots,x_n)}
\]

\end{frame}
%
\begin{frame}
\frametitle{Logique du premier ordre : reprise 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:I}\vdash Q}{\Gamma\vdash \forall x.\, Q}$ ($x$ \alert{frais})
&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall x.\, Q}{\Gamma\vdash Q[x\backslash t]}$
\\\hline
$\exists$
&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[x\backslash t]}{\Gamma\vdash \exists x.\, Q}$
&$\inferrule{\Gamma\vdash \exists x.\, P\\\Gamma, {\color{mydarkgreen}x:I}, {\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash Q}$
($x$ \alert{frais})
\\
\end{tabular}

\itempoint Les hypothèses en gris $\Gamma \vdash t:I$ (formation des
termes) ne sont parfois pas écrites dans les arbres de démonstration,
mais sont essentielles (cf. transp. \ref{caveat-inhabited-domain}).

\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:I,\;\forall y.B(x,y),\;y':I \vdash \forall y.B(x,y)}
}{x:I,\;\forall y.B(x,y),\;y':I \vdash B(x,y')}
}{x:I,\;\forall y.B(x,y),\;y':I \vdash \exists x'.B(x',y')}
}{\exists x.\forall y.B(x,y),\;y':I \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}
\frametitle{Notation des preuves par des $\lambda$-termes}

On reprend la preuve donnée aux transp. précédents :

\begin{center}
\scalebox{0.8}{\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:I,\;\forall y.B(x,y),\;y':I \vdash \forall y.B(x,y)}
}{x:I,\;\forall y.B(x,y),\;y':I \vdash B(x,y')}
}{x:I,\;\forall y.B(x,y),\;y':I \vdash \exists x'.B(x',y')}
}{\exists x.\forall y.B(x,y),\;y':I \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'))}
$
}
\end{center}

Avec les notations du
transp. \ref{natural-deduction-rules-with-quantifiers-and-notations}
elle se note :
\[
\lambda(u:\exists x.\forall y.B(x,y)).\;
\lambda(y':I).\;
(\texttt{match~}u\texttt{~with~}\langle x,v\rangle \mapsto
\langle x,vy'\rangle)
\]

\end{frame}
%
\begin{frame}
\frametitle{Exemples de preuves écrites comme $\lambda$-termes}

\itempoint $(\forall x.(A(x)\Rightarrow C)) \Rightarrow ((\exists
x. A(x)) \Rightarrow C)$

\smallskip

{\footnotesize Preuve :} $\lambda(f:\forall x.(A(x)\Rightarrow C)).\,
\lambda(p:\exists x. A(x)).\, (\texttt{match~}p\texttt{~with~}\langle
x,w\rangle \mapsto fxw)$

\medskip

\itempoint $((\exists x. A(x)) \Rightarrow C) \Rightarrow (\forall
x.(A(x)\Rightarrow C))$

\smallskip

{\footnotesize Preuve :} $\lambda(g:(\exists x. A(x)) \Rightarrow
C).\, \lambda(x:I).\, \lambda(u:A(x)).\, g\langle x,u\rangle$

\medskip

{\footnotesize

\itempoint Notamment pour $C$ valant $\bot$ on a prouvé $(\forall
x.\neg A(x)) \Leftrightarrow \neg(\exists x. A(x))$ ci-dessus.

\par}

\medskip

\itempoint $(\exists x.(A(x)\Rightarrow C)) \Rightarrow ((\forall
x. A(x)) \Rightarrow C)$

\smallskip

{\footnotesize Preuve :} $\lambda(p:\exists x.(A(x)\Rightarrow C)).\,
\lambda(f:\forall x. A(x)).\, (\texttt{match~}\!p\!\texttt{~with~}\!\langle
x,w\rangle \mapsto w(fx))$

\medskip

{\footnotesize

\itempoint Notamment pour $C$ valant $\bot$ on a prouvé $(\exists
x.\neg A(x)) \Rightarrow \neg(\forall x. A(x))$ ci-dessus.

\par}

\medskip

\itempoint $(\forall x.A(x)) \Rightarrow (\exists x.\top) \Rightarrow
(\exists x.A(x))$

{\footnotesize Preuve :} $\lambda(f:\forall x.A(x)).\,
\lambda(p:\exists x.\top).\, (\texttt{match~}p\texttt{~with~}\langle
x,u\rangle \mapsto \langle x,fx\rangle)$

\medskip

\itempoint $\forall z.\exists x.\top$ (cf. transp. suivant)

{\footnotesize Preuve :} $\lambda(z:I).\,\langle z,\bullet\rangle$

\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:I \vdash \exists x.\top$ (ici $z$ variable qcque)
mais \alert{on n'a pas} $\vdash \exists x.\top$.

\medskip

\itempoint Exiger que de pouvoir former $t:I$ à partir de $\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}]{
{\color{gray}\inferrule*[Left={Ax}]{ }{z:I\vdash z:I}}\\
\inferrule*[Right={$\top$Int}]{ }{z:I\vdash\top}
}{z:I\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}