diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 115 |
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} |