diff options
| -rw-r--r-- | transp-inf110-03-super.tex | 113 |
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} % |