Fix various mistakes and make some improvements noted during lecture on 2023-12-19.

1 files changed, 33 insertions, 33 deletions

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 0626337..0ef600c 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -93,9 +93,9 @@ connecteurs propositionnels $\Rightarrow,\land,\lor,\top,\bot$.
 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 prennent une formule $P(v)$ dépendant d'une variable $v$ libre,
 \item lient cette variable pour former une nouvelle formule $\forall
-  x. P(x)$ ou $\exists x. P(x)$.
+  v. P(v)$ ou $\exists v. P(v)$.
 \end{itemize}
 
 \medskip
@@ -103,9 +103,9 @@ mathématiques au-delà de ces connecteurs : les
 \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
+\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 x.P(x)$, parfois noté $\bigvee_x P(x)$ est à $P\lor 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}
 
@@ -113,7 +113,7 @@ comme des « $\land$ et $\lor$ en famille », c'est-à-dire que :
 
 \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 ?).
+$v$ ici ? quel est leur domaine ?).
 
 \smallskip
 
@@ -156,30 +156,30 @@ maintenant les quantificateurs :
 \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$ »)}.
+$\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} $x
-\mapsto \sigma(x)$ (= types dépendant de quelque chose) dont on puisse
+\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 x.P(x)$ correspondra à un terme de
-forme $\lambda(x:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
-à $P(x)$.
+\itempoint Une preuve de $\forall v.P(v)$ correspondra à un terme de
+forme $\lambda(v:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
+à $P(v)$.
 
 \medskip
 
-\itempoint Remarquer que $\forall x.P$, si $P$ ne dépend pas de $x$,
+\itempoint Remarquer que $\forall v.P$, si $P$ ne dépend pas de $v$,
 « 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.)}
+  I} S = S^I$ (ensemblistement ou numériquement).  {\footnotesize (Les
+  détails dépendent de la nature de la quantification.)}
 
 \end{frame}
 %
@@ -187,7 +187,7 @@ forme $\lambda(x:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
 \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
+\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 »)}.
@@ -195,31 +195,31 @@ forme $\lambda(x:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
 \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)$ »)}.
+$\exists v. P(v)$ {\footnotesize (« la donnée d'un $v_0$ et d'un
+  témoignage de $P(v_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 $v_0$ et
+  d'une valeur de type $\sigma(v_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
+\itempoint Une preuve de $\exists v.P(v)$ correspondra à un terme de
+forme $\langle v_0, \cdots\rangle$, où le type de $(\cdots)$
+correspond à $P(v_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
+\itempoint Remarquer que $\exists v.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 x.P(x)$ on \alert{puisse extraire} le
-$x_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
+que d'une preuve de $\exists v.P(v)$ on \alert{puisse extraire} le
+$v_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}.)}
 
@@ -263,7 +263,7 @@ fonction.
 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).
+uniquement logique, et cet énoncé est prouvable).
 
 \end{frame}
 %