Try to improve explanations of what sort of quantifications are allowed.

1 files changed, 92 insertions, 23 deletions

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index beaac0b..d2d9bd0 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -234,7 +234,7 @@ $t_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
 {\footnotesize\textcolor{orange}{Les règles ci-dessous (et
     transp. suivants) 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}
+    peut en former des « termes d'individus ».}\par}
 
 \medskip
 
@@ -397,8 +397,8 @@ 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.
 
-{\footnotesize (\textbf{N.B.} on n'explique pas comment le « terme »
-  $t$ est formé.)}
+{\footnotesize (\textbf{N.B.} on n'explique pas comment le « terme
+  d'individu » $t$ est formé.)}
 \[
 \inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}
 \]
@@ -488,43 +488,74 @@ $\exists$
 \\
 \end{tabular}
 
+\medskip
+
+\itempoint Les séquents en gris sont des formations de termes
+d'individus (cf. transp. suivant).
+
 \end{frame}
 %
 \begin{frame}
-\frametitle{Que peut-on quantifier au juste ?}
+\frametitle{Monde des termes et monde logique}
 
 \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 » :
+séquents en gris (formation des termes).
+
+\medskip
+
+\itempoint Selon le système logique, on peut distinguer deux
+« mondes » \alert{plus ou moins séparés ou confondus} :
 \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 ?)
+\item le monde des termes (individus) et types (d'individus),
+\item le monde logique, avec preuves et propositions.
 \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).
+\itempoint Les règles données aux transp. précédents sont les règles
+de construction des \alert{démonstrations} ($\rightarrow$ monde
+logique), où se placent tous les séquents sauf ceux marqués en gris.
 
 \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 ».
+\itempoint Les règles du monde des termes peuvent être calquées sur le
+monde des démonstrations, plus simples, ou différentes.
 
 \medskip
 
-\itempoint Évoquons néanmoins auparavant deux problèmes généraux :
+\itempoint En Coq, les deux mondes sont \alert{séparés mais
+  parallèles} : $\mathit{Prop}$ pour le type des propositions et
+$\mathit{Type}$ pour le type des types d'individus.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Que peut-on quantifier au juste ?}
+
+\itempoint Outre la question des termes d'individus et leur séparation
+du monde logique, il manque les explications sur ce qu'on a le droit
+de quantifier et d'abstraire ; notamment :
 \begin{itemize}
-\item l'extraction d'informations du $\exists$,
-\item l'imprédicativité dans la quantification.
+\item peut-on former des propositions comme
+  $\forall(A:*).\,(A\Rightarrow A)$ {\footnotesize (où « $*$ » est le
+  type des propositions)} avec preuve $\lambda(A:*).\,\lambda(h:A).h$,
+  i.e., quantifier sur les propositions (et abstraire dessus dans les
+  termes) ?
+\item peut-on former des objets comme $\lambda(A:*).\,A$ de type
+  $*\rightarrow *$, i.e., abstraire sur les propositions ?
+\item peut-on former des propositions comme $\forall(x:I).\,A(x)$ où
+  $A$ a pour type $I \rightarrow *$, i.e., quantifier et abstraire sur
+  des individus ?
 \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 (jusqu'à mélanger complètement preuves et individus).
+
 \end{frame}
 %
 \begin{frame}
@@ -644,9 +675,9 @@ imprédicatif) :
 \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}.
+  prédicats} (du 1\textsuperscript{er} ordre) est la plus simple qui
+ajoute les quantificateurs.  Les « choses » sur lesquelles on a le
+droit de quantifier s'appellent des \textbf{individus}.
 
 \medskip
 
@@ -793,7 +824,8 @@ correctement :
 \end{frame}
 %
 \begin{frame}
-\frametitle{Logique du premier ordre : reprise des règles}
+\label{first-order-logic-rules}
+\frametitle{Logique du premier ordre : reprise des règles logiques}
 
 \begin{tabular}{c|c|c}
 &Intro&Élim\\\hline
@@ -1060,4 +1092,41 @@ intuitionniste, ils sont identiques en logique classique.  On
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Monde des individus et monde logique}
+
+\itempoint En logique du premier ordre, on a
+\alert{deux « mondes » complètement séparés} :
+\begin{itemize}
+\item le monde des individus, avec un seul type ($I$) et des variables
+  sur lesquelles on peut quantifier,
+\item le monde logique, avec propositions et preuves.
+\end{itemize}
+
+\medskip
+
+\itempoint Les propositions ont « moralement » un type (qu'on pourrait
+appeler « $*$ » ou « $\mathit{Prop}$ »), mais on ne l'écrit pas.  Les
+relations $n$-aires ont « moralement » le type $I^n \to
+\mathit{Prop}$, pas non plus écrit.
+
+\medskip
+
+\itempoint Dans le transparent \ref{first-order-logic-rules}, tous les
+séquents concernent le monde logique (= construction des
+démonstrations), sauf ceux marqués en gris.
+
+\medskip
+
+\itempoint Dans la version la plus simple de la logique du premier
+ordre (pas de \emph{fonctions} d'individus, seulement des
+\emph{relations}), la seule règle du monde des individus est :
+\[
+\inferrule{ }{\Gamma,\; x:I\vdash x:I}
+\]
+(on ne peut former un terme d'individu qu'en invoquant une variable du
+contexte).
+
+\end{frame}
+%
 \end{document}