1 files changed, 111 insertions, 2 deletions

diff --git a/transp-inf110-03-super.tex b/transp-inf110-03-super.tex
index 36485c6..db76f2c 100644
--- a/transp-inf110-03-super.tex
+++ b/transp-inf110-03-super.tex
@@ -219,8 +219,117 @@ I\times X$.  {\footnotesize (Les détails dépendent de la nature de la
 
 \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.  {\footnotesize (Les détails dépendent du système
-  logique précis considéré.)}
+$x_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}
+%
+\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 !
 
 \end{frame}
 %