partie6-14.tex

%Partie 6
\chapter{La logique des prédicats}
 
\section{Introduction}

Nous allons maintenant étudier une logique beaucoup plus expressive que la
logique propositionnelle, la logique des prédicats, qui est aussi appelée
la logique de premier ordre.\footnote{Il existe des logiques d'ordres supérieures,
mais elles ne feront pas l'objet de ce cours.}
Voici un premier tableau qui montre les différences entre la logique propositionnelle vue jusqu'à présent et la logique des prédicats que nous allons étudier.
\begin{center}
\begin{tabular}{|c|c|}
\hline 
Logique Propositionnelle & Logique des prédicats \\ 
\hline
Propositions premières & Prédicats P(x,y) \\ 
P, Q, R & Quantifieurs: $\exists$x, $\forall$y \\ 
$\hookrightarrow$ Pas de Relations & $\hookrightarrow$ Relation \\ 
\hline 
\end{tabular} 
\end{center}

On note P(x,y) dans la logique des prédicats avec x,y, les arguments du prédicat P qui sont des variables.
Dans la logique propositionnelle, chaque proposition est isolée/indépendante alors que dans les prédicats on peut lier plusieurs prédicats ensemble.


\begin{center}
\begin{tabular}{|c|c|c|}
\hline 
Exemple & Logique propositionnelle & Logique des prédicats \\ 
\hline 
Socrate est un philosophe & P & Phil(Socrate) \\ 
Platon est un philosophe & Q & Phil(Platon) \\ 
\hline 
\end{tabular} 
\end{center}

En logique propositionnelle il n'y a aucune relation entre P et Q, alors qu'en logique des prédicats on peut lier Socrate et Platon avec le prédicat Philosophe qui prend en argument le nom du philosophe (Socrate ou Platon dans ce cas). Phil(Socrate) est donc vrai. On peut donc dire grâce aux prédicats que Socrate et Platon sont "la même chose", des philosophes.\\

Un autre exemple de prédicat:

\begin{center}
$\forall \alpha$ Phil($\alpha$) $\Rightarrow$ Savant($\alpha$)\\
\vspace{3mm}
$\hookrightarrow$ ... \textit{cette formulation permet de résumer un très grand nombre de faits. L'ensemble des arguments $\alpha$ peut être infini}
\end{center}
Comme Socrate est un philosophe, on peut déduire que Socrate est un savant aussi!

Dire la même chose en logique propositionnelle serait beaucoup plus compliqué: \\

"Socrate est un savant" Proposition "R"\\
\indent "Platon est un savant" Proposition "S"\\

On va donc noter en logique propositionnelle
\begin{center}
(P$\Rightarrow$R) $\cup$ (Q$\Rightarrow$S) $\cup$ ...(\textit{potentiellement infini})
\end{center}

On doit tout énumérer car il n'y a aucune relation entre les différentes propositions. S'il y a un nombre infini, ça ne marche pas. Il y a donc de grandes limitations dans la logique propositionnelle.

Néanmoins parfois la logique propositionnelle peut être utile. 
Il existe des outils informatiques qui utilisent la logique propositionnelle. On peut prendre l'exemple de ``SAT solver'' à qui on donne des équations booléennes très compliquées et qui va trouver les valeurs des propositions primitives qui rendent vraie cette proposition.
La logique propositionnelle est utile, mais si l'on veut faire du raisonnement sur plus que  "vrai" et "faux" avec des relations entre des propositions,  la logique propositionnelle ne marche pas. Si on veut faire un logiciel qui montre une certaine intelligence, il faut utiliser la logique des prédicats.\\

Autre exemple:

\begin{tabular}{|ccc|} 
\hline
Exemple & Logique propositionnelle & Logique des prédicats \\ 
\hline
Tout adulte peut voter & P & $\forall$x adulte(x) $\Rightarrow$ voter(x) \\ 
John est un adulte & Q & adulte(\textcolor{OliveGreen}{John}) \\ 
\line(1,0){50} & \line(1,0){10} & \line(1,0){45} \\ 

John peut voter & \textcolor{Red}{?R?}& voter(\textcolor{OliveGreen}{John}) \\ 
\hline
\end{tabular}\\

Ce genre de raisonnement est très difficile à faire en logique propositionnelle alors qu'en logique des prédicats c'est beaucoup plus simple.
Le John en ligne 3 et en ligne 4 correspond à la même personne, ou de manière plus général à la même variable.
Ceci montre donc bien l'utilité de la logique des prédicats pour faire des relations de ce type.

\section{Quantificateurs}

Les expressions "pour tout $x$" ($\forall x$) et "il existe $x$ tel que" ($\exists x$) sont appelés des {\em quantificateurs}.
Les quantificateurs permettent de résumer un grand nombre de formules en une formule.
La notion de {\em portée} d'un quantificateur est un concept très important auquel il faut faire très attention,
car il peut changer complètement le sens d'une formulation.
Par exemple, les deux formules suivantes:

$\forall x$ (enfants($x$) $\wedge$ intelligents($x$) $\Rightarrow$ $\exists y$ aime($x$,$y$)) \\

$\forall x$ (enfants($x$) $\wedge$ intelligents($x$)) $\Rightarrow$ $\exists y$ aime($x$,$y$) \\

Ces deux formules peuvent paraître équivalentes, mais en réalité elles ont un sens tout à fait différent.
En effet, dans le deuxième cas on remarque que le quantificateur $\forall x$ ne porte pas sur
la dernière variable $x$ qui est l'argument du prédicat aime($x$,$y$).
Il faut donc faire bien attention à quel quantificateur une variable s'identifie lorsqu'on manipule des formules.

\begin{itemize}
\item[$\bullet$] $\forall x$ P($x$) $\wedge$ $\exists x$ Q($x$) : contient deux variables différentes\\
 
\item[$\bullet$] $\forall x$ $\exists x$  P($x$) $\wedge$ Q($x$) : est une forme incorrecte, conflit des noms de variables \\
\end{itemize}

Pour résoudre ces conflits, on fait appel à une nouvelle opération, le {\em renommage}.
Cette opération permet de changer le nom des variables tout en conservant le sens de la formule. Ainsi on obtient : \\

$\forall x$ $\exists z$  P($x$) $\wedge$ Q($z$)  \textit{renommage (2)} \\
 
Le concept de variables, de leurs portées ainsi que d'opérateurs en logique des prédicats fait fortement penser au langage de programmation
 
Une comparaison peut être faite entre un code de programme et une formule.
Prenons un code tout à fait banal comprenant des variables différentes avec des portées différentes qui ont le même identificateur ainsi qu'une formule correspondante. 

\begin{verbatim}
1.  begin {
2.      var x,y: int;        
3.      x := 4;
4.      y := 2;
5.    
6.      begin {
7.          var x: int;
8.          x := 5;
9.          x := x*y;
10.     end }
11.     x := x*y;
12. end }
\end{verbatim}


\textcolor{Green}{$\forall x$} \textcolor{Red}{$\forall y$} p(\textcolor{Green}{$x$}) $\wedge$ ((\textcolor{Blue}{$\exists x$}  q(\textcolor{Blue}{$x$},\textcolor{Red}{$y$})) $\vee$ r(\textcolor{Green}{$x$},\textcolor{Red}{$y$}))  \\ 

Cet exemple illustre la hiérarchie et la portée des variables et des quantificateurs.

En analysant la formule morceau par morceau : \\

\begin{itemize}

\item[$\bullet$] " \textcolor{Green}{$\forall x$} \textcolor{Red}{$\forall y$} p(\textcolor{Green}{$x$}) $\wedge$ " correspond aux lignes $\lbrace 2,3,4 \rbrace$ du code \\

\item[$\bullet$]" \textcolor{Blue}{$\exists x$}  q(\textcolor{Blue}{$x$},\textcolor{Red}{$y$}) $\vee$ " correspond aux lignes $\lbrace 7,8,9 \rbrace$ \\
 
\item[$\bullet$]" r(\textcolor{Green}{$x$},\textcolor{Red}{$y$})) "  correspond à la ligne $\lbrace 11 \rbrace$ \\

\end{itemize}

Cet exemple montre bien la correspondance entre le concept de portée
dans le monde de la programmation et celui de la logique des prédicats.

\section{Syntaxe}

\subsection{Symboles}

Voici les différents symboles utilisés dans une formule de la logique des prédicats.
Nous appelons {\em arité} d'un prédicat ou d'une fonction son nombre d'arguments
(fonction unaire, prédicat binaire, etc.).

\begin{tabular}{|c|c|c|}
	\hline
	Symboles logiques & quantificateurs & $\forall$ $\exists$ \\
	                  & connecteurs logiques & $\wedge$ $\vee$ $\neg$ $\Rightarrow$ $\Leftrightarrow$ \\
	                  & parenthèses & ( ) \\
	                  & variables & $x, y, z$ \\
	                  & & true, false\\
	\hline
	Symboles non logiques & symboles de prédicat & $P$ $Q$ $R$ (avec arité $\geq 0$) \\
	   		      & symboles de fonction & $f$ $g$ $h$ (avec arité $\geq 0$) \\
	   		      & symboles de constante & $a$ $b$ $c$ (si arité $= 0$) \\
	\hline
\end{tabular}

\subsection{Règles de grammaire}
\begin{tabular}{rl}
$<formule>::=$ 	  &	$<formule$ $atomique>$ \\
				  & $\vert$ $\neg$ $<formule>$ \\
				  & $\vert$ $<formule>$ $<connecteur>$ $<formule>$ \\
				  & $\vert$ $\forall <var>.<formule>$ \\
				  & $\vert$ $\exists <var>.<formule>$ \\
$<formule$ $atomique>::=$ 
				  & true, false \\
				  & $\vert$ $<predicat>(<terme>*)$ \\
$<terme>::=$	  & $<constante>$ \\
				  & $\vert <var>$ \\
				  & $\vert <fonction>(<terme>*)$ \\
$<connecteur$ $binaire>::=$ 
				  & $\wedge \vert \vee \vert \Rightarrow \vert \Leftrightarrow$ \\

\end{tabular}

\section{Sémantique}

Dans la logique des prédicats, nous gardons les notions de modèle et d'interprétation déjà définies dans la logique propositionnelle. Même si la logique des prédicats est beaucoup plus puissante, sa sémantique reste similaire à la logique propositionnelle.
Comme pour la logique propositionnelle, une interprétation peut avoir une valeur (true, false).

\subsection{Exemple}
Illustrons par un exemple : 

\begin{center}
$p : P(b,f(b)) \Rightarrow \exists y   P(a,y)$  \\
\vspace{3mm}
\end{center}
On suppose que le $a$ et le $b$ sont des constantes et que le $f$ est une fonction.
Une interprétation possible de cette formule est la suivante:
\begin{itemize}
\item[$\bullet$]P : $\mathrm{val}_{I}(P) = $ $ \geq $ \hspace{3mm} (\textit{considéré comme un vrai prédicat})
\item[$\bullet$] a : $\mathrm{val}_{I}(a) = $ $ \sqrt{2} $ 
\item[$\bullet$] b : $\mathrm{val}_{I}(b) = $ $ \pi $ 
\item[$\bullet$] $f$ : $\mathrm{val}_{I}(f) = $ $ f_{i} $ \hspace{3mm} $f_{i}= \Re \rightarrow \Re : d \rightarrow \dfrac{d}{2} $ 
\end{itemize}
Avec ces éléments, on peut donc interpréter la formule $p$:
\begin{center}
\textit{Si $\pi \geq  \dfrac{\pi}{2}$, alors $\exists$ $ d \in \Re$ tel que $\sqrt2 \geq d$ }
\end{center}
Avec cette interprétation, la phrase logique donne ce sens.
Une autre interprétation donnerait un sens totalement différent à la phrase logique. Voici une autre interprétation totalement différente :
\begin{itemize}
\item[$\bullet$] a : $\mathrm{val}_{I}(a) = $ "Barack Obama"
\item[$\bullet$] b : $\mathrm{val}_{I}(b) = $ "Vladimir Putin"
\item[$\bullet$] $f$ : $\mathrm{val}_{I}(f) = $ $ f_{i} $ \hspace{3mm} $f_{i}: d \rightarrow \mathrm{père}(d)$
\item[$\bullet$] P :  $\mathrm{val}_{I}(P) = $ $P_{I}$ \hspace{3mm} $d_{1}$ est enfant de $d_{2}$\\
\end{itemize}

Avec ce nouveau sens, on trouve l'interprétation suivante : 
\begin{center}
\textit{Si Vladimir Putin est un enfant du père de Vladimir Putin alors il existe une personne telle que Barack Obama est un enfant de cette personne.}
\end{center}
La seconde interprétation est très différente de la première malgré le fait que ce soit la même formule à l'origine ! La connexion entre une formule et son sens permet de garder une certaine souplesse dans le sens où l'on peut choisir ça. C'est un peu comme dans la logique propositionnelle, mais avec encore plus de souplesse.

On peut se demander si ces deux interprétations sont des modèles de la formule ? \\
La première interprétation est un modèle de la formule, car le sens de la formule est vrai dans l'interprétation. En effet, $\pi \geq \dfrac{\pi}{2}$ et $\exists$ $ d \in \Re$ tel que $\sqrt2 \geq d$. On voit donc que le modèle est vrai.

La deuxième interprétation est aussi un modèle de la formule, car l'interprétation trouvée est vraie aussi. Cela peut paraître bizarre, mais c'est correct. 
%Partie 7

\subsection{Interprétation}

\subsubsection{Interprétation des symboles}

L'approche que nous utilisons pour définir une sémantique de la logique des prédicats est très proche 
de l'approche que nous avons utilisée pour la logique propositionnelle.
Nous allons définir une interprétation $I$ de chaque formule, qui nous permettra de calculer si la formule est vraie ou fausse.
Cependant, l'interprétation en logique des prédicats est plus générale qu'en logique propositionnelle.
En plus des propositions, nous avons des variables, des fonctions et des prédicats avec des arguments,
et des quantificateurs ($\forall$ et $\exists$).

Une {\em interprétation} $I$ en logique des prédicats est une paire $I = (D_I, \mathrm{val}_I)$,
avec un ensemble $D_I$ qui s'appelle le {\em domaine de discours} et une fonction $\mathrm{val}_I$ qui s'appelle
la {\em fonction de valuation} qui renvoie un élément de $D_I$ pour chaque symbole.
Nous avons donc pour chaque symbole $s$:
\begin{itemize}
\item Si $s$ est un symbole de prédicat,
 $\mathrm{val}_{I}(s) = P_{I}$ une fonction $P_{I}:D_{I}^{n} \rightarrow (\mathrm{true},\mathrm{false})$.
\item Si $s$ est un symbole de fonction,
 $\mathrm{val}_I(s) = f_I$ une fonction $f_{I}:D_{I}^{n} \rightarrow D_{I}$ avec $n$ le nombre d'arguments.
\item Si $s$ est une constante (une fonction avec zéro arguments),
 $\mathrm{val}_I(s) = c$ un élément de $D_I$.
\item Si $s$ est une variable,
 $\mathrm{val}_{I}(x) = x_{I}$, un élément $D_{I}$.
\end{itemize}
Cela implique chaque fonction correspond à une vraie fonction, chaque prédicat
correspond à un vrai prédicat, et chaque constante et chaque variable correspondent à une constante dans le domaine de discours.

Attention à la différence entre les variables et les constantes.
Pour les deux, l'interprétation est un élément de $D_I$,
mais on peut utiliser les variables dans les quantificateurs et pas les constantes.
Cela veut dire que dans une formule, la valeur d'une variable dépend de l'endroit où se trouve la formule,
ce qui n'est pas vrai pour une constante.

\subsubsection{Interprétation des termes et formules}

Avec la fonction $\mathrm{val}_I$ qui est définie sur tous les symboles, nous pouvons définir une fonction
$\mathrm{VAL}_I$ sur les termes et les formules:
\begin{equation}
\mathrm{VAL}_I : \mathrm{TERM} \cup \mathrm{PRED} \rightarrow D_I \cup \{T, F\}
\end{equation}
Ici, $\mathrm{TERM}$ est l'ensemble des termes et $\mathrm{PRED}$ est l'ensemble des formules.
Nous avons donc:
\begin{itemize}
\item Si $t$ est un terme, $t \rightarrow \mathrm{VAL}_I(t)$.
\item Si $p$ est une formule, $p \rightarrow \mathrm{VAL}_I(p)$.
\end{itemize}
Nous pouvons définir $\mathrm{VAL}_I$ avec $\mathrm{val}_I$, en suivant la définition de la syntaxe des formules:
\begin{itemize}
\item $\mathrm{VAL}_I ( P(t_1, \ldots, t_m) = (\mathrm{val}_I(P)) (\mathrm{VAL}_I(t_1), \ldots, \mathrm{VAL}_I(t_m))$.
\item $\mathrm{VAL}_I ( \forall x.p ) = T$ si pour chaque $d \in D_I$, $\mathrm{VAL}_{\{x \leftarrow d\} \circ I}(p) = T$.  Sinon, c'est $F$.
En clair, $d$ est l'interprétation de $x$ dans la formule $p$.  Si pour tous les $d$, l'interprétation de $p$ est vraie, alors le
quantificateur universel est vrai aussi.
\item $\mathrm{VAL}_I ( \exists x.p ) = T$ s'il existe un élément $d \in D_I$ tel que $\mathrm{VAL}_{\{x \leftarrow d\} \circ I}(p) = T$.
Sinon, c'est $F$.
\item $\mathrm{VAL}_I(p \wedge q) = T$ si $\mathrm{VAL}_I(p)=T$ et $\mathrm{VAL}_I(q)=T$.  Si au moins un des deux est $F$, c'est $F$.
\item $\mathrm{VAL}_I(p \vee q) = T$ si $\mathrm{VAL}_I(p)=T$ ou $\mathrm{VAL}_I(q)=T$.  Si tous les deux sont $F$, c'est $F$.
\item $\mathrm{VAL}_I(c) = \mathrm{val}_I(c)$ si $c$ est un symbole de constante.
\item $\mathrm{VAL}_I(x) = \mathrm{val}_I(x)$ si $x$ est un symbole de variable.
\item $\mathrm{VAL}_I(f(t_1, \ldots, t_n)) = (\mathrm{val}_I(f))(\mathrm{VAL}_I(t_1), \ldots, \mathrm{VAL}_I(t_n))$ si $f$ est un symbole de fonction.
\item $\mathrm{VAL}_I(\mathrm{true}) = T$.
\item $\mathrm{VAL}_I(\mathrm{false}) = F$.
\item Dans cette énumération, j'ai omis de mentionner l'implication $\Rightarrow$ et l'équivalence $\Leftrightarrow$.
Je vous les laisse en exercice.
\end{itemize}
En décomposant une formule $p$ en ses symboles de base, nous pouvons donc calculer $\mathrm{VAL}_I(p)$, c'est-à-dire si la formule
est vraie ou fausse, à partir de la fonction $\mathrm{val}_I$.

\subsubsection{Modèle}

Un modèle d'un ensemble de formules est une interprétation qui rend toutes les formules vraies.
Formellement, si on a un ensemble de formules $B = \{ p_1, \ldots, p_n \}$,
une interprétation $I$ pour $B$ est un {\em modèle} si et seulement si:
\begin{equation}
\forall p_i \in B: \mathrm{VAL}_I(p_i) = T
\end{equation}

%partie 3

\chapter{Preuves en logique des prédicats}
\label{preuvemanuelle}

On va généraliser l'approche de la logique propositionnelle, car comme vu précédemment le langage des prédicats est beaucoup plus riche.  Il ajoute entre autres :

\begin{itemize}
    \item Des variables
    \item Des constantes
    \item Des fonctions (détaillé plus tard)
    \item Des prédicats
    \item Des quantificateurs
\end{itemize}

Les preuves en logique des prédicats ressemblent très fort aux preuves en logique propositionnelle. Il y a encore des prémisses, des formules avec leurs justificatifs et une conclusion. On peut aussi utiliser des preuves indirectes et des preuves conditionnelles.
Une preuve est toujours un objet formel:

\begin{center}
\fbox{
\begin{tabular}{l l l}
  1. & \fbox{\ldots} &  Prémisses \\
  2. & \fbox{Formule, regle} &  Justification \\
  \ldots & \ldots &  \ldots \\
  n. & \fbox{Conclusion} &  Justification \\
\end{tabular}
}
\end{center}

Mais il est vrai que les preuves en logique des prédicats sont parfois délicates à cause des variables:
occurrences libres (pas quantifiées), occurrences liées par $\forall$ et occurrences liées par $\exists$.
Dans ce chapitre nous allons surtout étudier comment manipuler les variables et les quantificateurs
correctement dans une preuve.

\section{Exemple}

Nous allons prouver que s'il est vrai que
$\forall x \cdot P(x) \wedge Q(x)$ (prémisse)
alors il est vrai que $\forall x \cdot P(x)\wedge(\forall x \cdot Q(x))$ (conclusion).
Nous utilisons l'approche suivante pour traiter les quantificateurs~:
\begin{center}
\begin{enumerate}
	\item Enlever les quantificateurs pour avoir des variables libres\\
	\item Raisonner sur l'intérieur\\
	\item Remettre les quantificateurs\\
\end{enumerate}
\end{center}
Les étapes difficiles à réaliser correctement sont les étapes $1$ et $3$. Voici la preuve en ``français'' :

En retirant les quantificateurs des prémisses, cela donne :
``Comme $P(x) \wedge Q(x)$ est vrai pour tout $x$, alors $P(x)$ est vrai pour tout $x$''. 
De là, on peut remettre les quantificateurs pour obtenir $\forall x \cdot P(x)$. De façon similaire, on obtient $\forall x \cdot Q(x)$. Et on conclut en remettant les quantificateurs: $\forall x \cdot P(x) \wedge \forall x \cdot Q(x)$, en utilisant la conjonction.

En preuve formelle, cela donne :

\begin{center}
\fbox{
$
\begin{array}{l l l}
  1. &  \forall x \cdot P(x) \wedge Q(x) &  $Prémisses$ \\
  2. & P(x) \wedge Q(x) &  $Élimination de $\forall \\
  3. & P(x) &  $Simplification$ \\
  4. & \forall x \cdot  P(x) &  $Introduction de $ \forall \\
  5. & Q(x) &  $Simplification de 2$ \\
  6. & \forall x \cdot Q(x) &  $Introduction de $\forall \\
  7. & \forall x \cdot P(x) \wedge \forall x \cdot Q(x) &  $Conjonction$ \\
\end{array}
$
}
\end{center}

On a donc utilisé 4 règles en plus par rapport aux preuves formelles en logique propositionnelle (les règles de la logique propositionnelle restent valables en logique des prédicats):
\begin{itemize}
\item Élimination de $\forall$
\item Introduction de $\forall$
\item Élimination de $\exists$
\item Introduction de $\exists$
\end{itemize}

Certaines de ces règles sont simples d'utilisation, d'autres sont plus difficiles.
Il est également possible d'utiliser d'autres règles (certaines plus générales que d'autres\footnote{Voir "Inference logic" ou "Predicate logic"}).

\begin{framed}
\textbf{Note}

Il est possible d'utiliser les quantificateurs  dans les formules mathématiques. Typiquement, on ne les note pas, car ils sont présents de manière implicite. Par exemple :
\begin{itemize}
\item $\forall x \cdot \sin(2x) = 2 \cdot \sin(x) \cdot \cos(x)$ 
\item $\forall x \cdot x + x = 2x$
\item $\exists x \cdot \sin(x) + \cos(x) = 0,5$
\item $\exists x \cdot x + 5 = 9$
\end{itemize} 

On peut remarquer que pour les deux premiers cas, $x$ est une véritable variable, on peut donc ajouter un quantificateur universel $\forall$. 
Pour les deux cas suivants, on remarque que $x$ est une inconnue, car il y a une équation à résoudre et une solution à trouver, on peut donc ajouter un quantificateur existentiel $\exists$.

Dans certains cas, les quantificateurs existentiels et universels sont
utilisés au sein de la même formule mathématique. Se limitant à
l'univers de discours tels que $ b^{2}-4ac > 0$, on peut dire :
\begin{itemize}
\item[] $\forall a \cdot \forall b \cdot \forall c \cdot \exists x \cdot ax^{2}+bx+c = 0$
\end{itemize}
Dans l'exemple ci-dessus, nous avons 4 variables : $a,b,c,x$. Les 3 premières sont des véritables variables, on peut les affecter à n'importe quelle valeur, tandis que la dernière est une inconnue, c'est la solution à trouver. Il faut donc trouver $x$ pour toutes les valeurs possibles de $a,b,c$.
On appelle souvent $a,b,c$ des {\em paramètres}.
\end{framed}

\section{Règles en logique des prédicats}

Nous allons maintenant introduire les règles de déduction pour les quantificateurs.
D'abord, nous définissons une manipulation symbolique importante qui est utilisée
dans ces règles: la substitution.
Ensuite nous définissons les quatre règles pour les quantificateurs.

Comment savons-nous que les règles sont correctes?
On ne peut pas le prouver dans la logique des prédicats: on ne peut pas prouver l'exactitude
des règles avec les règles elles-mêmes!
Il faut faire un raisonnement en dehors de la logique des prédicats.
Nous justifions chaque règle avec un raisonnement basé sur un modèle de la formule.
Si la logique des prédicats est notre langage pour exprimer les raisonnements formels,
on peut donc dire que la justification des règles est faite en dehors de ce langage, donc en {\em meta-langage}.

\subsection{La substitution}
Une manipulation fréquente en logique des prédicats est la \textbf{substitution}. Elle consiste à prendre une formule et remplacer une partie par une autre.

Si on a une formule quelconque $p$, la notation $p[x/t]$ veut dire de remplacer toutes les occurrences libres de $x$ par $t$.
Une {\em occurrence libre} d'une variable est une occurrence qui n'est pas dans la portée d'un quantificateur.
Il faut faire attention aux variables dans $t$, pour éviter qu'une variable dans $t$ ne rentre dans la portée d'un quantificateur,
ce qui s'appelle la {\em capture de variable}.
Pour éviter la capture, il faut faire un {\em renommage} de variable, c'est-à-dire, changer les noms des variables dans $p$.
Voici un exemple de $p[x/y]$ où $p = P(x) \rightarrow \forall y \cdot (P(x) \wedge R(y))$ :
\begin{center}
\begin{tabular}{|l |l |>{\raggedright}m{6cm}|}
\hline
1. &$P(x) \rightarrow \forall y \cdot (P(x) \wedge R(y))$&$[x/y]$ veut dire qu'on va remplacer toutes les occurrences libres de $x$ par $y$.\tabularnewline
\hline
2. &$P(y) \rightarrow \forall y \cdot (P(y) \wedge R(y))$&En remplaçant $x$ par $y$, on a changé le sens de la formule, car avant, $x$ n'était pas dans la portée du quantificateur alors que maintenant il l'est. Ce changement de sens s'appelle une \textit{capture de variable}, car la variable $y$ est capturée par le quantificateur. Pour résoudre ce problème, on va effectuer un \textit{renommage}.\tabularnewline
\hline
3. &$P(y) \rightarrow \forall z \cdot (P(y) \wedge R(z))$&Résultat après renommage (pour éviter la capture de variable).
On a changé le $y$ en $z$ (renommage) et remplacé le $x$ par $y$ (substitution). \tabularnewline
\hline
\end{tabular}
\end{center}

Voici un autre exemple avec $p = \exists y . P(x,y)$.
Nous donnons plusieurs possibilités de substitution correctes:
\begin{itemize}
\item $p[x/y] = \exists z. P(y,z)$ (attention: $y$ a été renommée)
\item $p[x/f(x)] = \exists y. P(f(x),y)$
\item $p[x/c] = \exists y. P(c,y)$ ($c$ est une constante)
\item $p[x/z] = \exists y. P(z,t)$
\end{itemize}

% Ancienne partie 8

\subsection{Élimination de $\forall$}
\begin{flushleft}

Parce que $\forall x . P(x)$ veut dire pour tout $x_{I}$ $\in$ $D_{I}$ : $P_{I}$($x_{I}$) est vrai,
on peut remplacer sans contrainte:$\linebreak \linebreak$
$\forall$x$\bullet$P(x) $\rightarrow$ P(a) $\>$ a est une constante quelconque\\
$\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\rightarrow$ P(y) $\>$ y est une variable $\>$ (parce que $P_{I}$($y_{I}$) est vrai)$\linebreak$ 

\underline{Règle :}
\begin{center}
{\LARGE $\frac{\forall x : p}{p[x/t]}$}
\end{center}
\textcolor{red}{\danger\ N'oubliez pas de faire le renommage si nécessaire}

\underline{Exemple :}\\
\begin{enumerate}
\item $\forall$x $\bullet$ $\forall$y $\bullet$ P(x,y) $\>$ Pr\'emisse
\item $\forall$y $\bullet$ P(x,y) $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\forall$
\item P(x,x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\forall$
\item $\forall$x $\bullet$ P(x,x) $\>$ $\>$ $\>$ $\>$ $\>$ Introduction de $\forall$
\end{enumerate}
Le renommage n'est pas nécessaire dans la ligne (3) parce qu'il n'y a pas de capture.

\subsection{Élimination de $\exists$}

Il faut faire attention avec cette règle, parce que $\exists x. P(x)$ veut dire qu'il existe
un élément $x_I \in D_I$ pour lequel $P_I(x_I)$ est vrai.
On ne connait pas cet élément, mais on peut introduire un symbole qui le représente:$\linebreak \linebreak$
$\exists$x $\bullet$ P(x) $\rightarrow$ P(a) \\
a = nouvelle constante qui n'apparaît nulle part ailleurs ($\mathrm{val}_{I}(a) = x_{I}$) $\linebreak$ \\

$\exists$x $\bullet$ P(x) $\rightarrow$ P(z) \\
z = nouvelle variable dans la preuve ($\mathrm{val}_{I}(z) = x_{I}$) $\linebreak$\\

$\exists$x $\bullet$ P(x) $\nrightarrow$ P(y) (pas autorisé)\\
y = variable qui existe d\'ej\`a dans la preuve, elle a déjà une valeur $\linebreak$ \\

\underline{Exemple 1 :}\\
\begin{enumerate}
\item $\exists$x $\bullet$ chef(x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>\>$Pr\'emisse
\item $\exists$x $\bullet$ voleur(x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$  $\>$Pr\'emisse
\item chef(y) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$Élimination de $\exists$
\item voleur(y) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\exists$ \textcolor{red}{(y pas nouvelle)}
\item chef(y) $\wedge$ voleur(y) $\>$ $\>$ $\>$ $\>$ $\>$ Conjonction
\item $\exists$y $\bullet$ chef(y) $\wedge$ voleur(y) $\>$ Introduction de $\exists$ \textcolor{red}{(FAUSSE)}
\end{enumerate}

\underline{Exemple 2 :}\\
\begin{enumerate}
\item $\exists$x $\bullet$ chef(x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$Pr\'emisse
\item $\exists$x $\bullet$ voleur (x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$Pr\'emisse
\item chef(y) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\exists$
\item voleur (z) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\exists$
\item chef(y) $\wedge$ voleur(z) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Conjonction
\item $\exists$y $\exists$z chef(y) $\wedge$ voleur(z) $\>$ Introduction de $\exists$ (EXACTE)
\end{enumerate}

\subsection{Introduction de $\exists$}

Si $p[t]$ est vrai cela veut dire qu'il existe un élément $t_I = \mathrm{VAL}_I(t) \in D_I$ avec $(\mathrm{val}_I(p))(t_I)$.
On peut donc introduire $\exists x$ car un élément existe qui rend vrai $p[x]$.
Mais attention, on doit pouvoir trouver la formule originale à partir de $\exists x.p[x]$,
sinon l'introduction du quantificateur ``$\exists$'' a changé le sens de la formule (capture!).

\underline{R\`egle :}
\begin{center}
{\LARGE $\frac{p[t]}{\exists x \bullet p[x]}$}
\end{center}
Autorisé si la substitution $p[x/t]$ retrouve la formule originale.$\linebreak$

\underline{Exemple :}
\begin{center}
 P(y,y)\\
$\exists$x $\bullet$ P(x,x)\\[2\baselineskip]
\sout{P(y,x)}\\
\sout{$\exists$x $\bullet$ P(x,x)}
\begin{flushright}
\textcolor{red}{Ceci n'est pas correct !}
\end{flushright}
\end{center}
Le deuxième exemple ne marche pas parce que $P(x,x)[x/y]$ ne retrouve pas la formule originale.

\subsection{Introduction de $\forall$}

\underline{R\`egle :}
\begin{center}
{\LARGE $\frac{p}{\forall x \bullet p}$}
\end{center}
\begin{itemize}
\item Si $p$ n'a pas d'occurrence libre de $x$ alors c'est OK
\item Si $p$ contient une occurrence libre de $x$ : on doit s'assurer que la preuve jusqu'à cet endroit marchera pour toutes valeurs affectées à $x$\\
$\> \> \> \hookrightarrow$ Aucune formule dans la preuve jusqu'à cet endroit ne doit mettre une contrainte sur $x$ !
\end{itemize}
\underline{Deux conditions :}
\begin{itemize}
\item $x$ n'est pas libre dans une formule obtenue par élimination de $\exists$. Deux cas sont possibles~:
	\begin{itemize}
		\item $\exists x$ éliminé, donc $x$ a été choisi pour rendre vraie la formule
		\item $\exists y$ éliminé, donc $y$ a été choisi selon la valeur de $x$ ($y$ dépend de $x$)
	\end{itemize}
		Dans les deux cas, une contrainte sur $x$ empèche d'introduire $\forall x$
\item $x$ n'est pas libre dans une prémisse (dans ce cas, $x$ serait connu depuis le début donc il possède déjà une valeur)
\end{itemize}

\underline{Exemple :}\\
\begin{enumerate}
\item $\forall$x $\exists$y parent(y,x) $\>$ Prémisse
\item $\exists$y parent(y,x) $\>$ $\>$ $\>$ $\>$Élimination de $\forall$
\item parent(y,x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\exists$ \textcolor{blue}{$\rightarrow$ N'est valable que pour ce y et ce x, pas pour tous}
\item \sout{$\forall$x parent(y,x)} $\>$ $\>$ $\>$ $\>$Introduction de $\forall$ \textcolor{red}{$\rightarrow$ On ne peut pas faire ça, car il y a une contrainte sur x. Là on dit que ce y est parent de tous !}
\end{enumerate}




\end{flushleft}

% Ancienne partie 9

\section{Exemple plus conséquent}

Il est important de pouvoir faire des preuves manuellement, car cela permet de bien comprendre toutes les étapes de raisonnement
d'une preuve, même si par la suite on utilise un algorithme plutôt que de faire les preuves à la main. 
Terminons donc par un exemple un peu plus conséquent d'une preuve manuelle en logique des prédicats avant d'introduire
l'algorithme permettant d'effectuer des preuves de manière automatisée.

L'exemple suivant est inspiré de l'Empire Romain: 
\subsubsection{Prémisses}
\begin{itemize}
    \item Les maîtres et les esclaves sont tous des hommes adultes.
    \item Toutes les personnes ne sont pas des hommes adultes.
\end{itemize}
\textit{Note: on voit dans les prémisses qu'il y a des quantificateurs: tous, toutes.}

\subsubsection{A prouver} 
\begin{itemize}
    \item Il existe des personnes qui ne sont pas des maîtres.
\end{itemize}

\subsubsection{Preuve}
\begin{enumerate}
    \item $\forall{}x\ (maitre(x)\lor{}esclave(x)\implies{}adulte(x)\land{}homme(x))$ \hfill Prémisse
    \item $\lnot{}\forall{}x\ (adulte(x)\land{}homme(x))$ \hfill Prémisse
    \item $\exists{}x\ \lnot{}(adulte(x)\land{}homme(x))$ \hfill Théorème de négation\\
    \textit{S' il n'est pas vrai que toutes les personnes sont des hommes adultes alors il existe une personne qui n'est pas un homme adulte}
    \item $\lnot{}(adulte(x)\land{}homme(x))$ \hfill Élimination de $\exists$ \\
\textit{    On élimine le quantificateur existentiel:  on peut le faire, car on introduit une variable x qu'on choisit comme étant une personne rendant vraie la proposition.}
    \item $(maitre(x)\lor{}esclave(x)\implies{}adulte(x)\land{}homme(x))$ \hfill Élim. de $\forall$ \\
    \textit{On peut retirer le $\forall$  en réduisant le champ de x aux x rendant vraie la proposition.}
    \item $\lnot{}(maitre(x)\lor{}esclave(x))$ \hfill Modus Tollens
    \item $\lnot{}maitre(x)\land{}\lnot{}esclave(x)$ \hfill De Morgan
    \item $\lnot{}maitre(x)$ \hfill Simplification
    \item $\exists{}y\ \lnot{}maitre(y)$ \hfill Introduction de $\exists$ \\
    \textit{Comme dans l'interprétation, x est une personne qui rend valable cette proposition, on peut dire qu'il existe une personne rendant valable cette proposition et réintroduire le quantificateur $\exists$}
\end{enumerate}
C'était un exemple très simple ne faisant que quelques pas, mais la logique est assez expressive pour permettre des preuves plus complexes
(par exemple, formaliser les mathématiques).
Le nombre de pas serait alors beaucoup plus important. 

Les mathématiciens ont fait de grands efforts pour formaliser les mathématiques
avec la logique des prédicats.
Nous mentionnons le Principia Mathematica de Whitehead et Russell, et les ouvrages nombreux de Nicolas Bourbaki.

\section{Note historique}

\hfill {\begin{minipage}{0.90\textwidth}
\begin{small}
A la fin du 19ème siècle, début du 20ème: 
\begin{itemize}
\item Création de la logique de 1er ordre (Gottlob Frege)
\item Deux personnes ont essayé de formaliser toutes les mathématiques. Principia Mathematica (Alfred Whitehead, Bertrand Russell)
\end{itemize}
Lors que l'arrivée des ordinateurs, fin du 20ème siècle (années 50-60 et fin du siècle) on a essayé de formaliser la logique via des algorithmes:
\begin{itemize}
\item Création de l'Algorithme de Preuves (1965):
\begin{itemize}
\item Alan Robinson invente la Règle de Résolution (qui va être expliquée au chapitre suivant)
\item Création de prouveurs (assistants de preuve) par exemple Coq (1989) et Isabelle (1986)
\item Création de la logique de programmation qui aide à l'élaboration de la programmation par contraintes: Prolog (1972) 
\end{itemize}
\item Création de la sémantique Web: OWL (Web Ontology Langage)
\end{itemize}
\end{small}
\end{minipage}

\chapter{Algorithme de preuve pour la logique des prédicats}
\label{algorithmepreuve}

Dans le chapitre précédent nous avons introduit des règles pour faire des preuves manuelles.
Avec l'arrivée des ordinateurs, les logiciens ont tout de suite essayé de faire des preuves mécanisées.
Nous avons vu dans le chapitre \ref{preuveprop} (Section \ref{algorithmeprop})
un algorithme de preuve pour la logique propositionnelle qui utilise la réfutation.
La logique des prédicats est beaucoup plus expressive que la logique propositionnelle
et le raisonnement est plus délicat (voir chapitre précédent!).

Est-ce que nous pouvons faire un algorithme de preuve pour la logique des prédicats?
Cela ne semble pas évident.
Beaucoup de logiciens ont travaillé sur cette question.
La réponse affirmative à la question est un des grands résultats des mathématiques du 20ème siècle.
Dans ce chapitre nous verrons un algorithme de preuve avec une grande puissance.
On peut le faire marcher malgré la complexité des variables et des quantificateurs ce qui est assez étonnant,
car c'est une logique très expressive. 

\section{Propriétés de l'algorithme}

L'algorithme pour la logique des prédicats
ne garde pas toutes les propriétés de l'algorithme pour la logique propositionnelle,
car la logique des prédicats est beaucoup plus expressive.
En particulier, là où l'algorithme pour la logique propositionnelle est décidable,
l'algorithme pour la logique des prédicats n'est que semi-décidable.

Supposons $B$ l'ensemble des axiomes (prémisses) et $T$ le théorème que l'on veut prouver.
On a les propriétés suivantes:
\begin{itemize}
\item L'algorithme est {\em adéquat} (``{\em consistent}''): Si $B\vdash T$ alors $B \models T$\\
Si l'algorithme trouve une preuve de $T$ avec les axiomes $B$ alors $T$ sera vraie dans tous les modèles de $B$.
\item L'algorithme est {\em complet} (``{\em complete}''): Si $B \models T$ alors $B\vdash T$\\
Si $T$ est vrai dans tous les modèles de $B$ alors l'algorithme trouvera une preuve de $T$ avec les axiomes $B$.
\item L'algorithme est {\em semi-décidable}:
\begin{itemize}
\item Si $B \models T$ alors l'algorithme trouve une preuve. 
\item Si $B \not\models T$ il peut tourner en rond indéfiniment.
\end{itemize}
Si $T$ est vrai dans tous les modèles, l'algorithme trouvera une preuve, mais si $T$ n'est pas
vrai dans tous les modèles, l'algorithme peut tourner en rond et ne jamais se terminer.
Le problème est donc que quand l'algorithme prend trop de temps à trouver une preuve,
à un certain moment on doit l'arrêter et l'on n'est jamais certain du résultat.
On ne peut jamais être sûr que l'algorithme n'aurait pas trouvé une preuve si on l'avait laissé tourner plus longtemps.
Il est donc semi-décidable, car il ne s'arrête que si une preuve existe.
Si il était décidable, il s'arrêterait toujours.
\end{itemize}

\section{Concepts de base}

L'algorithme de preuve est basé sur deux idées:
\begin{itemize}
\item Simplification des prémisses.
On transforme les prémisses dans une forme uniforme et simple qui s'appelle forme clausale.
\item Simplification des règles d'inférence.
On garde une seule règle d'inférence, la résolution, qui marche sur la forme clausale.
\end{itemize}
Avec ces deux simplifications, la définition de l'algorithme se simplifie également.

\subsection{Forme normale conjonctive (forme clausale)} 

Pour transformer les prémisses en forme clausale, il y a trois étapes:
\begin{enumerate}
    \item Formule $\to$ forme prénexe: $$(\ldots{}\forall{}\ldots{}\exists{}\ldots{}\forall{} )\implies \forall{}\exists{}\forall{}(\ldots{})$$
    Tous les quantificateurs sont mis en tête de la formule. Les quantificateurs étant très compliqués à gérer, on transforme la formule pour les extraire de celle-ci. \\
    Les modèles sont préservés durant cette transformation, la formule avant la transformation a les mêmes modèles
    que la formule après la transformation.
    Cela est vrai parce que les deux formules sont équivalentes.
    \item Forme prénexe $\to$ forme Skolem (élimination des $\exists{}$): $$ \forall{}\exists{}\forall{}(\ldots{})  \implies \forall{}\forall{}\forall{}(\ldots{}) $$
    Les quantificateurs existentiels sont très embêtants, car ils sont restrictifs. Ils disent qu'il existe des éléments, mais ne précisent pas lesquels, on va donc les éliminer. \\
    Cette transformation préserve l'{\em existence} des modèles (la satisfaisabilité),
    mais pas les modèles eux-mêmes. Ils doivent être modifiés pour conserver la même signification. 
    \item Forme Skolem $\to$ forme normale conjonctive (forme clausale):  
    \[\forall \ldots \forall \land_i(\lor_j L_{ij})\]
    Cette transformation consiste à transformer la formule en
    une conjonction de disjonctions ($\land$ de $\lor$). Les règles pour cette transformation sont
    les mêmes règles qu'en logique propositionnelle. \\
    Les modèles sont préservés lors de cette transformation. 
\end{enumerate}

\subsection{Résolution}

La seule règle d'inférence gardée par l'algorithme s'appelle la résolution.
Cette règle existe déjà dans une forme plus simple dans la
logique des propositions: $$\frac{L\lor C_1, \neg L \lor C_2}{C_1\lor C_2}$$
Cette règle est simple en logique des propositions, car il n'y a pas de variables: $L$ et $\neg L$ sont directement comparables
(il y a le même $L$ dans les deux).
En logique des prédicats ce n'est plus vrai: on peut avoir $L_1 \lor C_1$ et $\neg L_2 \lor C_2$  avec $L_1$ et $L_2$ qui ont
des variables différentes.
On ne peut donc pas faire la résolution immédiatement.

Pour pouvoir faire la résolution, il va falloir en quelque sorte ``rendre $L_1$ et $L_2$ identiques''.
On va donc dire: ce ne sont peut-être pas toujours les mêmes, mais, pour certaines valeurs, ils sont identiques.
L'idée sera donc de les rendre identiques en substituant leurs variables par d'autres judicieusement choisies.
Cette opération s'appelle l'{\em unification}.
Prenons un exemple:

\begin{minipage}{0.25\textwidth}
		$L_1$ $=$ $P(x,a)$ \\
		$L_2$ $=$ $P(y,z)$
\end{minipage}

Pour que $L_1$ et $L_2$ deviennent identiques, on va restreindre leurs variables en faisant une substitution.
Nous avons les variables $x$, $y$, $z$ et une constante $a$.
Une substitution possible est de remplacer $x$ par $y$ et $z$ par $a$.
On écrit $\sigma = \{(x,y),(z,a)\}$ où $\sigma$ est la substitution.
Si on applique $\sigma$ à $L_1$ et $L_2$ on obtient:
$$L_1 \sigma = P(x,a) \sigma = P(y,a)$$
$$L_2 \sigma = P(y,z) \sigma = P(y,a)$$
Les deux formules sont maintenant identiques, et on peut donc faire la résolution.
Cette résolution marche pour toutes les valeurs qui sont limitées par la substitution.
Le résultat ne sera donc pas général.
En résumant, on peut écire la règle de résolution de façon plus générale en y mettant la substitution:
$$\frac{L_1 \lor C_1, \neg L_2 \lor C_2}{(C_1 \lor C_2)\sigma}$$
Pour faire l'inférence
on choisit le $\sigma$ le plus général possible, ce que nous appellons
l'{\em unificateur le plus général} (``{\em most general unifier}'').
On peut démontrer qu'un unificateur le plus général existe toujours.
C'est cette règle d'inférence que nous allons utiliser dans l'algorithme de preuve.

\section{Transformation en forme prénexe}

Etapes de la transformation en formule logiquement équivalente:
\begin{enumerate}
    \item Éliminer $\Leftrightarrow$ et $\Rightarrow$
    \item Renommer les variables. 
    \begin{itemize}
    \item Chaque quantificateur ne porte que sur une variable, il faudra en créer de nouvelles si besoin en prenant soin de conserver l'équivalence de la formule . 
    \item Attention: ne jamais garder le même nom de variable pour une variable libre et une variable liée. 
    \item Supprimer les quantificateurs si possible. \\
    \end{itemize}
    \item Migrer les négations ($\neg$) vers l'intérieur, vers les prédicats. On peut faire cela, car $\neg\exists$ peut être transformé en $\forall\neg$ et vice versa.  
    \item On peut mettre tous les quantificateurs de la logique des prédicats à l'avant de la formule. 
\end{enumerate}
\subsection{Exemple d'une transformation en forme prénexe}
\begin{enumerate}
\item $\forall x  [p(x) \land \neg (\exists y) \forall x ( \neg q(x,y))
    \Rightarrow\forall z \exists v \bullet p(a,x,y,v))]$\\ \textit{Expression de base}
\item $\forall x [p(x) \land \neg(\exists y) (\forall x) ($\colorbox{lightgray}{$\neg$} $\neg q(x,y) $\colorbox{lightgray}{$\lor$} $\forall z \exists v \bullet r(a,x,y,v)]$\\\textit{Suppression des $\implies{}$} 
\item $\forall x [p(x) \land \neg(\exists y) (\forall $\colorbox{lightgray}{$u$}$)(\neg\neg q($\colorbox{lightgray}{$u$}$,y) \lor $\colorbox{lightgray}{$\cancel{\forall z}$}$\exists v \bullet r(a,$\colorbox{lightgray}{$u$}$,y,v)]$\\\textit{Renommage des variables et suppression des quantificateurs inutiles}
\item $\forall x [p(x) \land$ \colorbox{lightgray}{$\forall y \neg$} $ (\forall u)($ \colorbox{lightgray}{$\cancel{\neg \neg}$} $q(u,y) \lor \exists v \bullet r(a,u,y,v)] $\\$\neg\exists y\ devient\  \forall \ y\ \neg \ et\ simplification\ des\ \neg$
\item $\forall x [p(x) \land \forall y $ \colorbox{lightgray}{$\exists u \neg$}$(q(u,y) \lor \exists v \bullet r(a,u,y,v)] $\\$\neg\forall u\ devient\  \exists \ u\ \neg$
\item $\forall x [p(x) \land \forall y \exists u $\colorbox{lightgray}{$(\neg q(u,y) \land \neg (\exists v) \bullet r(a,u,y,v))]$}\\ \textit{Distribution des $\neg$}\textit{(De Morgan)}
\item $\forall x [p(x) \land \forall y \exists u (\neg q(u,y) \land $\colorbox{lightgray}{$(\forall v) \bullet \neg$}$ r(a,u,y,v))]$\\$\neg\exists y\ devient\  \forall \ y\ \neg$
\item $\forall x$\colorbox{lightgray}{$ \forall y \exists u \forall v  \bullet$}$ [p(x) \land (\neg q(u,y) \land  \neg r(a,u,y,v))]$\\\textit{Extraction des quantificateurs.}
\end{enumerate}

% Ancienne partie 10

\section{Transformation en forme Skolem}
\subsection{Intuition}

Cette transformation consiste à éliminer toutes les occurrences de quantificateurs existentiels.
Ceux-ci correspondent au solutions des équations.
Comme l'algorithme ne résoud pas toutes les équations, la skolemisation retire le besoin de trouver une solution.
L'algorithme n'a plus qu'a trouver une solution en fonction des solutions aux équations.
\smallskip

$(\forall x)(\forall y)(\exists u)(\forall v) \big[ P(x) \wedge \neg Q(u,y) \wedge \neg R(a,u,y,v) \big]$
\smallskip 


Dans ce cas-ci, la valeur de $u$ dépend des valeurs de $x$ et $y$. Lorsqu'on a choisi $x$ et $y$, on est alors libre de choisir $u$.
On peut donc supposer qu'une fonction $g(x,y)$ fournit cet élément de façon à conserver la satisfaisabilité de la formule tout en supprimant $(\exists u)$.
\smallskip

$(\forall x)(\forall y)(\forall v) \big[ P(x) \wedge \neg Q(\textbf{g(x,y)},y) \wedge \neg R(a,\textbf{g(x,y)},y,v) \big]$
\smallskip

Après la transformation, l'existence des modèles est préservée.

\subsection{Règle}

Pour chaque élimination d'un quantificateur existentiel $(\exists x)$, on remplace sa variable quantifiée par une fonction $f(x_1,...,x_n)$ dont les arguments sont les variables des quantificateurs universels dont $x$ est dans la portée.
Cette transformation ne conserve pas les modèles parce que la formule originale n'utilise pas le symbole $f$
et la formule transformée utilise un symbole $f$.
Mais la satisfaisabilité est conservée: la première formule a un modèle si et seulement si la deuxième formule en a un.
\smallskip

\underline{Justification par un exemple:}

$p: \forall x \forall y \exists z \big[ \neg P(x,y) \vee Q(x,z) \big]$
\smallskip

$p_s: \forall x \forall y \big[ \neg P(x,y) \vee Q(x,\textbf{f(x,y)}) \big]$
\smallskip

Les modèles de $p$ ne sont les mêmes que les modèles de $p_s$.

\underline{Pour $p$}
\begin{itemize}
  \item Interprétation $I$
  \item $D_I =$ Professeur $\cup$ Université
  \item $\mathrm{val}_I(P) = P_I = $ ``a enseigné à l'université''
  \item $\mathrm{val}_I(Q) = Q_I = $ ``est diplômé de l'université''
  \item $\mathrm{val}_I(f)$ n'existe pas (le symbole $f$ n'existe pas dans $p$).
\end{itemize}

\vspace{\baselineskip}

\underline{Pour $p_s$}
\begin{itemize}
  \item Interprétation $I' = \{ f \leftarrow f_i \} \circ I$ (c'est une extension de $I$)
  \item $D_I =$ Professeur $\cup$ Université
  \item $\mathrm{val}_I(P) = P_I = $ ``a enseigné à l'université''
  \item $\mathrm{val}_I(Q) = Q_I = $ ``est diplômé de l'université''
  \item $\mathrm{val}_I(f) = f_I : \mathrm{Professeur} \times \mathrm{Université} \rightarrow \mathrm{Université}$ \\
  $f_I(a,b) = $ ``l'université ayant dû diplômer $a$ pour que $a$ puisse enseigner à $b$''
\end{itemize}

$p$ admet un modèle $(I)$ si et seulement si $p_s$ admet un modèle $(I')$.

Que ça ne soit exactement le même modèle ne pose pas de problème pour notre algorithme. L'algorithme par réfutation continue à itérer jusqu'à trouver une contradiction ({\em false}). S'il n'y a pas de modèle pour $p_s$, il n'y a pas de modèle pour $p$ et ça suffit.

\section{Transformation en forme normale conjonctive}

On fait les
mêmes manipulations qu'en logique des propositions (voir Section \ref{fnc}).
On transforme la formule en une conjonction de disjonctions.

\section{La règle de résolution}

$$ \mbox{\Large $\frac{L_1 \vee C_1, \neg L_2 \vee C_2}{(C_1 \vee C_2)\sigma}$ } $$

Cette règle de résolution ne fonctionne que si $L_1$ et $L_2$ sont identiques.

\underline{Exemple 1:}

\begin{itemize}
  \item $L_1 = P_1(a, y, z)$
  \item $L_2 = P_1(x, b, z)$
\end{itemize}

Dans un modèle de $\{L_1, L_2\}$
il y a un prédicat qui correspond au symbole $P_1$ et il y a un ensemble de triplets qui rendent vrai $P_1$.

L'unification de $L_1$ et $L_2$ donne $L$ qui représente l'intersection des deux ensembles. On écrit:
\begin{itemize}
  \item $L_1 \sigma = L$
  \item $L_2 \sigma = L$
\end{itemize}

\vspace{5 mm}
$L_1$ et $L_2$ sont {\em unifiables} s'il existe une substitution $\sigma$ telle que $L_1 \sigma = L_2 \sigma$.
\begin{itemize}
  \item $\sigma = \big\{(x,a),(y,b)\big\}$
  \item $L_1 \sigma = P(a,b,z)$
  \item $L_2 \sigma = P(a,b,z)$
\end{itemize}

\vspace{5 mm}
\underline{Exemple 2:}
\begin{itemize}
  \item $L_1 = P_1(a,x)$
  \item $L_2 = P_2(b,x)$
\end{itemize}
Il n'y pas de substitution qui existe, car on a deux constantes différentes, l'intersection des deux ensembles est vide.
$L_1$ et $L_2$ ne sont donc pas unifiables.
\smallskip

\underline{Exemple 3:}

\begin{itemize}
  \item $L_1 = P(f(x), z)$ 
  \item $L_2 = P(y, a)$
\end{itemize}

Dans ce cas-ci, il y a beaucoup de substitutions possibles telles que:
\begin{itemize}
  \item $\sigma_1 : \big\{ (y, f(a)), (x,a), (z,a) \big\}$ => $L_1 \sigma_1 = L_2 \sigma_1 = p(f(a), a)$
  \item $\sigma_2 : \big\{ (y, f(x)), (z,a) \big\}$ \hspace{11 mm}=> $L_1 \sigma_2 = L_2 \sigma_2 = p(f(x), a)$
\end{itemize}
$L_1$ et $L_2$ sont donc unifiables.
On peut démontrer que $\sigma_2$ est l'unificateur le plus général (souvent abbrévié en {\em upg},
en anglais {\em mgu}: most general unifier).
Il donne les ensembles les plus grands.\\

\begin{itemize}
  \item Pour que la démonstration soit la plus générale possible,
  on préfère toujours l'unificateur $\sigma$ \underline{le plus général}.
  \item On peut démontrer que l'unificateur le plus général est unique.
  La démonstration de ce fait est hors de portée pour ce cours.
  \item L'upg est calculable.
\end{itemize}

\vspace{5 mm}
\textbf{\underline{Règle de résolution:}}
\begin{itemize}
  \item $p_1, p_2$ clauses
  \item $p_1 = L^{+} \vee C_1$
  \item $p_2 = \neg L^{-} \vee C_2$
  \item $ L^{+}$ et $L^{-}$ ont les mêmes symboles de prédicat.
  \item $ \big\{L^{+}, L^{-}\big\}$ sont unifiables par l'upg $\sigma$.
\end{itemize}

\underline{Alors} $$ \mbox{\Large $\frac{L^{+} \vee C_1, \neg L^{-} \vee C_2}{(C_1 \vee C_2)\sigma}$ } $$

\section{Algorithme}

L'algorithme de preuve prend comme entrées un ensemble
de formules (``axiomes'') $\{ \mathrm{Ax}_1, ..., \mathrm{Ax}_n \}$
et une formule à prouver $\mathrm{Th}$.
Chaque formule est en forme normale conjonctive.
L'algorithme utilise la preuve par contradiction (réfutation):
nous allons donc ajouter $\neg \mathrm{Th}$ à l'ensemble d'axiomes
et essayer de déduire une contradiction ($\mathrm{false}$).
Les déductions utilisent la règle de résolution, qui est bien adaptée
à la forme normale conjonctive.

L'algorithme n'est pas garanti de terminer.
S'il termine avec une contradiction, cela démontre $\mathrm{Th}$.
S'il termine sans contradiction, cela démontre que l'on ne peut pas prouver $\mathrm{Th}$.
S'il ne termine pas, on est dans le cas de la semi-décidabilité.

\subsection{Définition de l'algorithme}

\begin{algorithm}
\KwIn{$S := \big\{ \mathrm{Ax}_1, ..., \mathrm{Ax}_n, \neg \mathrm{Th} \big\}$}
\While{$ \mathrm{false} \notin S$ et il existe une paire de clauses dans $S$ résolvables et non résolues.}{
	Choisir $p_i, p_j$ dans $S$ tel qu'il existe:
	\begin{itemize}
        \item $L^{+}$ dans $p_i$
        \item $L^{-}$ dans $p_j$
  	\item $\big\{ L^{+}, L^{-} \big\}$ unifiable par upg $\sigma$
	\end{itemize}

	Calculer:
	\begin{itemize}
  	\item $r:=(p_i - [L^{+}] \vee p_j - [\neg L^{-}]) \sigma$
  	\item $S_i = S \cup  \big\{ r \big\}$
	\end{itemize}
}
\eIf{$\mathrm{false} \in S$}{$S$ inconsistent, donc $\mathrm{Th}$ prouvé.}{$S$ consistent, donc $\mathrm{Th}$ non prouvé.}
\end{algorithm}

\subsection{Exemple d'exécution}
Voici un exemple avant la mise en forme clausale:
\begin{itemize}
  \item $(\forall x) \mathit{homme}(x) \wedge \mathit{fume}(x) \Rightarrow \mathit{mortel}(x)$
  \item $(\forall x) \mathit{animal}(x) \Rightarrow \mathit{mortel}(x)$
  \item $\mathit{homme}(\mathit{Ginzburg})$
  \item $\mathit{fume}(\mathit{Ginzburg})$
  \item \textbf{Candidat-théorème:} $\mathit{mortel}(\mathit{Ginzburg})$
\end{itemize}

\subsubsection{Initialisation de S}
Après la mise en forme clausale cela donne:
\begin{itemize}
  \item P1: $(\forall x) \neg \mathit{homme}(x) \vee \neg \mathit{fume}(x) \vee \mathit{mortel}(x)$
  \item P2: $(\forall x) \neg \mathit{animal}(x) \vee \mathit{mortel}(x)$
  \item P3: $\mathit{homme}(\mathit{Ginzburg})$
  \item P4: $\mathit{fume}(\mathit{Ginzburg})$
  \item P5: $\neg \mathit{mortel}(\mathit{Ginzburg})$
\end{itemize}

\subsubsection{Itérations}

\textbf{\underline{1}}
\begin{itemize}
  \item P1 + P5
  \item $\sigma = \big\{ (x, \mathit{Ginzburg}) \big\}$
  \item $r = P6 = \neg \mathit{homme}(\mathit{Ginzburg}) \vee \neg \mathit{fume}(\mathit{Ginzburg})$
\end{itemize}

\textbf{\underline{2}}
\begin{itemize}
  \item P3 + P6
  \item $\sigma = \big\{ \big\}$
  \item $r = P7 = \neg \mathit{fume}(\mathit{Ginzburg})$
\end{itemize}

\textbf{\underline{3}}
\begin{itemize}
  \item P4 + P7
  \item $\sigma = \big\{ \big\}$
  \item $r = \mathrm{false}$ 
\end{itemize}
Il y a une inconsistence donc le candidat théorème est prouvé.

\subsubsection{Non-déterminisme}

Cet algorithme a plusieures sources de non-déterminisme, c'est-à-dire
le choix des clauses et le choix des littéraux dans les clauses.
Ces choix sont faits à chaque itération.
Avec un mauvais choix, l'algorithme peut ne pas terminer ou
faire des déductions inutiles.
Par exemple, si on fait un autre choix lors de la première itération:

\textbf{\underline{1}}
\begin{itemize}
  \item P2 + P5
  \item $\sigma = \big\{ (x, Ginzburg) \big\}$
  \item $r = \neg animal(Ginzburg)$
\end{itemize}

C'est une déduction inutile qui n'aide pas pour la démonstration de $\mathrm{Th}$.

\subsection{Stratégies}

Pour que cet algorithme soit utilisable en pratique, il est très important
de concrétiser des stratégies pour les choix:
\begin{itemize}
  \item Quelles paires $p_i$ et $p_j$ choisir?
  \item Quelles $L^{+}$ et $L^{-}$ choisir?
\end{itemize}
Il y a deux possibilités pour ces stratégies qui sont utilisées en pratique,
qui donne lieu à deux sortes de programmes que l'on appelle {\em assistant de preuve}
ou {\em langage logique}.
Dans ces deux cas, cela a donné lieu a des développements signifiants.

\subsubsection{Un assistant de preuve}

Un assistant de preuve est un outil qui aide un mathématicien humain à faire des preuves formelles.
Deux exemples d'assistants de preuves sont Coq et Isabelle. C'est un
outil très sophistiqué qui a permis de prouver des choses de manière
totalement formelle, alors qu'avant des preuves prenaient des dizaines
voire des centaines de pages de preuves mathématiques. Mais cet
assistant ne fait pas tout parce que l'algorithme est moins bon.
Cependant, il aide beaucoup. C'est à l'être humain de lui donner des
coups de pouce sous forme de lemmes, hypothèses, chemins,
stratégies\ldots Ensuite, l'algorithme s'occupe de la manipulation des symboles.

Un exemple très célèbre est le théorème des quatres couleurs. La question est : est-il toujours possible de colorier chaque pays avec une couleur, de façon à ce que deux pays limitrophes n'aient pas la même couleur et en utilisant un certain nombre de couleurs différentes? Ce n'est pas évident à prouver et ça a demandé beaucoup de travail aux mathématiciens. Mais récemment, Georges Gonthier (un informaticien) a réussi à formuler ce problème avec l'assistant de preuves. Ce fut un tour de force. Désormais, il existe une preuve complètement formalisée, sans erreur pour ce théorème.

\subsubsection{Un langage logique}

Un langage logique est un langage de programmation basé sur la logique des prédicats.
Le plus célèbre de ces langages est {\em Prolog}, inventé en 1972 par Alain Colmerauer et Robert Kowalski.
Prolog utilise {\em volontairement} des stratégies naïves qui permettent de rendre l'algorithme prévisible.
Les axiomes deviennent un {\em programme}.
Cette approche donne un langage de programmation pratique.
Un exemple de stratégie naïve est la stratégie LUSH utilisée par Prolog
qui choisit de haut vers le bas les paires $p_i, p_j$,
et de gauche à droite dans chaque $p_i$.
LUSH est un acronyme qui veut dire {\em Linear resolution with Unrestricted Selection for Horn clauses}.
La programmation logique sera expliquée plus en détail dans le chapitre \ref{prolog}.

% Ancienne partie 11

\chapter{Théories logiques}

On peut utiliser la logique des prédicats pour définir et étudier des structures mathématiques.
L'avantage est qu'une définition avec la logique est complètement précise.
La définition d'une structure contiendra deux types de formules:
des {\em axiomes} et des {\em règles d'inférence}.
Quelques exemples simples des structures que l'on peut définir sont
l'ordre partiel, les treillis, les groupes, les entiers, les chaînes, les arbres,
les ensembles, les relations et les fonctions.
Il y en a beaucoup plus que cela; en fait quasi toutes les mathématiques
peuvent êtres formalisées avec la logique des prédicats.
Dans ce chapitre nous allons voir quelques exemples de ces formalisations
pour des structures discrètes.

Ces formalisations peuvent être utilisées pour la programmation (par ex. avec Prolog)
et aussi dans les assistants de preuve.
Pour ces deux utilisations, il faut faire très attention à la manière dont on définit
les axiomes et les règles: cela peut avoir une grande influence sur l'efficacité de
l'exécution.
Mais dans ce chapitre nous ne nous intéressons pas à l'efficacité, mais plutôt à
la simplicité et la compréhension.

\subsubsection{Logique du premier ordre}

La logique des prédicats est parfois appelé la logique du premier ordre.
Dans ce chapitre nous allons parfois utiliser cette terminologie.
On l'appelle premier ordre parce que le domaine des quantificateurs $\forall x$ et $\exists x$
est $D_I$: les valeurs de $\mathrm{val}_I(x)$ sont toujours dans $D_I$.
Il existe aussi des logiques d'ordres superieurs; dans ce cas le domaine des quantificateurs
peut être autre chose.
Par exemple, dans une logique du second ordre, on peut quantifier sur les prédicats et pas
simplement sur les éléments du domaine de discours.
On pourra donc dire $\forall p$ ou $\exists p$ où $p$ est un prédicat.
Cela donne une expressivité supplémentaire par rapport à la logique du premier ordre,
mais les raisonnements et les preuves deviennent beaucoup plus complexes.
Il y a aussi moins de résultats généraux sur cette logique
et la plupart des mathématiques utilisées en pratique n'ont pas besoin de cette logique
pour être formalisée.
Nous n'abordons pas les logiques d'ordres supérieurs dans ce cours.

\section{Théorie du premier ordre}

Le concept de base est la {\em théorie du premier ordre}.
Une théorie du premier ordre est un ensemble $B$ de formules
qui représente les axiomes et les règles d'inférence d'une structure mathématique.
Nous allons nous restreindre au modèles: les interprétations de $B$
où les axiomes et les règles sont valides.

\subsection{Définition d'une théorie}

Une théorie contient les parties suivantes:
\begin{itemize}
\item Un sous-langage de la logique du premier ordre:
\begin{itemize}
\item Vocabulaire : constantes, fonctions, prédicats ;
\item Règles syntaxiques et sémantiques sur ce vocabulaire ;
\end{itemize}
\item Ensemble d'axiomes
\item Ensemble de règles d'inférence
\end{itemize}
Les axiomes et les règles d'inférence sont des
formules {\em fermées}, c'est-à-dire des formules ne contenant pas de variables libres.
L'idée est que ces formules expriment des faits sur tous les éléments du domaine.

\subsection{Exemple : théorie des liens familiaux (\bsc{FAM})}

Comme premier exemple
nous définissons une théorie qui permettra de raisonner sur les liens familiaux.

\begin{enumerate}
\item Vocabulaire : 
\begin{itemize}
\item 2 symboles de fonctions à un paramètre : $p/1$, $m/1$
\item 3 symboles de prédicats à deux paramètres : $P/2$, $GM/2$, $GP/2$\\
\end{itemize}
On peut interpréter les fonctions $p$ et $m$ comme "père de" et "mère de", et les prédicats $P$, $GM$ et $GP$ comme "parent de", "grand-mère de" et "grand-père de". On donnera plus de précisions sur cette interprétation par la suite.\\

\item Axiomes :
\begin{center}
\begin{tabular}{lcr}
$(\forall x) \left(P(x,p(x))\right)$ & \hspace*{2cm}& (père)\\
$(\forall x) \left(P(x,m(x))\right)$ & \hspace*{2cm}& (mère)\\
$(\forall x)(\forall y) \left(P(x,y)\Rightarrow GP(x,p(y)) \right)$&& (grand-père)\\
$(\forall x)(\forall y) \left(P(x,y)\Rightarrow GM(x,m(y)) \right)$&& (grand-mère)\\
\end{tabular}
\end{center}
\vspace{\baselineskip}

\item Règles : \\
Les règles sont uniquement celles de la logique des prédicats.
\end{enumerate}

\subsubsection{Première interprétation}
\begin{tabular}{@{}llr}
$D_I$ : personnes&&\\
$\text{val}_I(p)=\text{"père de"}$ & &$\text{père de} : \text{Pers}\rightarrow\text{Pers} : d \rightarrow \text{"père de" }d$\\
$\text{val}_I(m)=\text{"mère de"}$ & &$\text{mère de} : \text{Pers}\rightarrow\text{Pers} : d \rightarrow \text{"mère de" }d$\\
$\text{val}_I(P)=\text{"Parent"}$ & &$\text{Parent}(d_1,d_2)=T$ ssi $d_2$ est un parent de $d_1$\\
$\text{val}_I(GP)=\text{"Grand-père"}$ & &$\text{Grand-père}(d_1,d_2)=T$ ssi $d_2$ est un grand-père de $d_1$\\
$\text{val}_I(GM)=\text{"Grand-mère"}$ & &$\text{Grand-mère}(d_1,d_2)=T$ ssi $d_2$ est une grand-mère de $d_1$\\
\end{tabular}\\

Cette interprétation est un modèle de \bsc{fam} car les axiomes sont tous vérifiés.
On remarque la ressemblance avec une théorie scientique, où les axiomes correspondent à la théorie
et l'interprétation à ce que celle-ci signifie dans le monde réel.
Une théorie peut avoir plusieurs modèles.

\subsubsection{Seconde interprétation}

\begin{tabular}{lll}
$D_J$ : $\mathbb{N}$&&\\
$\text{val}_J(p)="p_J"$ &\hspace*{1cm} &$p_J : \mathbb{N}\rightarrow\mathbb{N} : d \rightarrow 2d$\\
$\text{val}_J(m)="m_J"$ &\hspace*{1cm} &$m_J : \mathbb{N}\rightarrow\mathbb{N} : d \rightarrow 3d$\\
$\text{val}_J(P)="P_J"$ &\hspace*{1cm} &$P_J(d_1,d_2)$ ssi $d_2=2d_1$ ou $d_2=3d_1$\\
$\text{val}_J(GP)="GP_J"$ &\hspace*{1cm} &$GP_J(d_1,d_2)$ ssi $d_2=4d_1$ ou $d_2=6d_1$\\
$\text{val}_J(GM)="GM_J"$ &\hspace*{1cm} &$GM_J(d_1,d_2)$ ssi $d_2=6d_1$ ou $d_2=9d_1$\\
\end{tabular}\\

Cette interprétation est également un modèle de \bsc{fam}.

\subsubsection{Exemple de preuve}

Voici une preuve dans la théorie \bsc{fam}.
Cette preuve est un exemple de l'approche syntaxique qui est mentionnée dans la section suivante.
La propriété qui est prouvée est vraie dans les deux interprétations.
On veut montrer  : 
$$\models_{\text{\bsc{fam}}} (\forall x)(\exists z) GM(x,z)$$

\begin{tabular}{lll}
1.&$(\forall x)(\forall y) \left(P(x,y)\Rightarrow GM(x, m(y)) \right)$&(Axiome de grand-mère)\\
2.&$(\forall x) \left(P(x,p(x))\Rightarrow GM(x, m(p(x))) \right)$&(Elimination de $\forall y$ et substitution $y/p(x)$)\\
3.&$(\forall x) P(x,p(x)) \Rightarrow (\forall x) GM(x,m(p(x)))$& (Distributivité $\forall/\Rightarrow$)\\
4.&$(\forall x) P(x,p(x))$ & (Axiome de père) \\
5.&$(\forall x) GM(x,m(p(x)))$&(Modus ponens)\\
6.&$(\forall x) (\exists y) GM(x,y)$&(Introduction de $\exists$)\\
\end{tabular}

Attention, cette preuve utilise le schéma de distributivité de $\forall$ sur $\Rightarrow$
dans la ligne (3).
Ce schéma dit que pour toutes formules $p$ et $q$
l'on peut remplacer $(\forall x) (p \Rightarrow q)$
par $(\forall x) p \Rightarrow (\forall x) q$.
Je vous laisse comme exercice de prouver la validité de ce schéma.
Indice: on peut utiliser l'approche sémantique, comme définie la section suivante.

\section{Propriétés des théories}

\begin{itemize}
\item Une formule fermée $p$ est \textit{valide} dans la théorie $Th$ si elle est vraie dans chaque modèle de $Th$. On écrit : 
$$\models_{Th} p$$
Soit l'ensemble des axiomes $Ax=\{Ax_1, \hdots, Ax_n\}$. On a bien que $\models_{Th} Ax_i$.\\
\item $q$ est une \textit{conséquence logique} de $p$ dans la théorie $Th$
si $q$ est vraie dans tous les modèles de $Th$ qui rendent $p$ vraie.
On écrit :  $$p \models_{Th} q$$
\item Une théorie est \textit{consistante} si elle a au moins un modèle ($>0$ modèles).
\item Une théorie est \textit{inconsistante} si elle n'a pas de modèle ($0$ modèles).\\
\end{itemize}

\subsection{Établir la validité}

Comment peut-on faire pour établir $\models_{Th} p$? Il y a deux approches différentes :
\begin{enumerate}
\item L'approche {\em sémantique} : on prend un modèle $I$ quelconque de $Th$ et on évalue $\textrm{VAL}_I (p)$
en utilisant le fait que $\text{VAL}_I (Ax_i)=T$.
\item L'approche {\em syntaxique} : on essaye de construire une preuve de $p$ à partir des axiomes, en appliquant les règles de $Th$.
Cette approche s'appelle aussi {\em théorie de la preuve}.\\
\end{enumerate}
En pratique, la deuxième approche est beaucoup plus souvent utilisée.\\

\subsection{Qualité d'une théorie}

Une théorie peut posséder certaines qualités qui la rend
meilleure que d'autres théories qui ne les possèdent pas.
Une ``bonne'' théorie est:
\begin {enumerate}
\item {\em consistante} : il est impossible de déduire \(p\) et \(\neg p\)  de la même théorie.
\item {\em minimale} : les axiomes sont indépendants, ce qui veut dire que l'on peut faire deux modèles des autre axiomes, un dans lequel l'axiome est vrai et un autre dans lequel l'axiome est faux~: $\forall i \neq k, Ax_i \not \models Ax_k $.\\
On peut vérifier la minimalité en construisant une interprétation $J$ telle que:\\
$\text{VAL}_J (Ax_k)= \mathrm{false}$\\
$\text{VAL}_J (Ax_i)= \mathrm{true}$ pour $i \neq k$
\item {\em complète} : les axiomes suffisent pour prouver les propriétés qui nous intéressent. Sinon il faut en ajouter.
\end {enumerate}

\subsubsection{Exemple dans l'astronomie}
\begin {enumerate}
\item {\textbf{Système de Copernic}} : Chaque axiome de chaque planète est indépendant, car elles tournent toutes autour du soleil.
\item{\textbf{Système de Ptolémée}} : Les axiomes de chaque planète dépendent de ceux de la Terre, car elle représente le centre de l'univers, mais elle est également une planète et dispose donc d'axiomes. Les epicycles de chaque planète dépendent	des axiomes de la Terre. Ce sont des cycles qui viennent en fait de la révolution de la Terre autour du soleil.
\end {enumerate}

% Ancienne partie 12
\section{Opérations sur les théories}

Nous allons définir une opération, l'extension, qui permet de créer une nouvelle théorie par rapport à une théorie existante,
et deux opérations, l'inclusion et l'équivalence, qui permettent de comparer deux théories.

\subsection{Extension d'une théorie}
Lorsqu'on a une théorie déjà existante, on souhaite parfois l'étendre afin de la rendre plus complète.
On dit que $Th_2$ est une {\em extension} de $Th_1$ si:
\begin{itemize}
\item[$\bullet$] Le vocabulaire de $Th_1$ est inclus dans le vocabulaire de $Th_2$.
\item[$\bullet$] Tout axiome de $Th_1$ est axiome de $Th_2$.
\end{itemize}
On peut donc étendre le vocabulaire et ajouter des axiomes.
Voici deux exemples d'extension de théorie pour mieux comprendre comment effectuer cette opération. Ils étendent tous les deux
la théorie des liens familiaux (\bsc{fam}) décrite dans la section précédente.

\subsubsection{Exemple 1}

Considérons le nouvel axiome suivant, que nous noterons Ax:
$$ Ax \equiv (\forall x) \neg P(x,x) $$
La nouvelle théorie ainsi étendue que nous noterons \bsc{fam*} possède un axiome de plus : Ax. Cette théorie \bsc{fam*}
est {\em consistante}, c'est-à-dire qu'il existe au moins un modèle qui valide cette théorie.
Pour s'en convaincre, il suffit de considérer la première interprétation de la théorie \bsc{fam} de la section précédente,
qui utilise les liens familiaux: personne est parent de lui-même.\\

En revanche, si on considère la deuxième interprétation (deuxième modèle, noté $J$) de \bsc{fam}
qui associe les symboles $p$ et $m$ aux fonctions mathématiques $p_J : \mathbb{N} \rightarrow \mathbb{N} : d \rightarrow 2d$ et $m_J : \mathbb{N} \rightarrow \mathbb{N} : d \rightarrow 3d$, on observe une contradiction.
En effet, dans le modèle $J$ on a la définition suivante du prédicat $P$ :
$$ P_J(d_1, d_2) \textrm{ ssi } d_2 = 2d_1 \textrm{ ou } d_2 = 3d_1$$
Il suffit de choisir $x=0$ dans notre nouvel axiome Ax pour constater que le modèle $J$ ne valide pas la théorie étendue \bsc{fam*}.
De manière générale, l'extension d'une théorie peut donc {\em réduire} l'ensemble des modèles de celle-ci.

\subsubsection{Exemple 2}

Considérons le nouvel axiome suivant, que nous noterons Adam:
$$ (\forall y) \neg P(a,y) $$
où $a$ est une constante arbitraire.
Notons la théorie étendue \bsc{fam'} = \bsc{fam} + Adam. Dans cet exemple, on peut observer que \bsc{fam'}
est {\em inconsistante}, car aucun modèle ne peut valider cette théorie.
En effet, en partant du premier axiome de \bsc{fam} (appelé "père"), nous effectuons quelques étapes pour obtenir une contradiction:
\begin{align*}
& (\forall x) P(x,p(x)) && \textrm{Axiome père} \\
& P(a,p(a)) && \textrm{Elimination } \forall \\
& (\exists y) P(a,y) && \textrm{Introduction } \exists
\end{align*}
Ci-dessus, le premier axiome de \bsc{fam} reformulé (père),
qui est en contradiction avec le nouvel axiome (Adam), que nous reformulons ci-dessous.
\begin{align*}
& (\forall y) \neg P(a,y) \\
\Leftrightarrow & \ \neg (\exists y) P(a,y)
\end{align*}
Par la règle de preuve par contradiction, on démontre qu'aucun modèle n'est possible pour la théorie étendue \bsc{fam'}.
Nous avons vu que
l'extension d'une théorie peut réduire le nombre de modèles: ici on voit qu'il faut bien vérifier que ce nombre ne devienne pas 0.

\subsection{Comparaison des théories}

Dans cette section, nous abordons la comparaison de différentes théories :
inclusion, équivalence et quelques corollaires.
Dans ce qui suit, on prend $Th_1$ et $Th_2$ deux théories.

\subsubsection{Inclusion}
On dit que $Th_1$ est {\em contenue} dans $Th_2$ si
\begin{itemize}
\item[$\bullet$] Le vocabulaire de $Th_1$ est inclus dans le vocabulaire de $Th_2$.
\item[$\bullet$] Toute formule valide dans $Th_1$ l'est aussi dans $Th_2$.
\end{itemize}
Tout modèle de $Th_2$ est donc aussi un modèle de $Th_1$.
Mais pas inversément: il est possible qu'il existe des modèles de $Th_1$ qui ne sont pas des modèles de $Th_2$.
C'est parce que $Th_2$ peut contenir des formules valides qui ne le sont pas dans $Th_1$.

\subsubsection{Équivalence}
On dit que $Th_1$ et $Th_2$ sont {\em équivalentes} si elles sont inclues l'une dans l'autre.
Cela signifie que les deux théories "disent la même chose" et que tout modèle d'une des théories est également modèle de l'autre.\\


Il est important de bien faire la différence entre
l'extension d'une théorie et l'inclusion d'une théorie dans une autre.
La confusion est possible parce que dans les deux cas, le nombre de modèles peut être réduit.
Mais il ne faut pas oublier que
l'extension est définie par rapport aux axiomes et l'inclusion est définie par rapport aux modèles.
Pour l'extension on ajoute des axiomes et on ne regarde pas les modèles.
Pour l'inclusion, on compare les modèles et on ne regarde pas les axiomes.
On peut dire que l'extension est une manipulation {\em syntaxique} (on change les axiomes ce qui permet de nouvelles preuves)
et l'inclusion est une manipulation {\em sémantique} (on fait une comparaison entre ce que modélisent les deux théories).

\subsection{Corollaires}
On note respectivement $V_t$, $M_t$ et $Ax_t$ le vocabulaire, les modèles et les axiomes d'une théorie $t$. \\

\noindent \underline{Si} $V_{Th_1} \subseteq V_{Th_2}$ et $M_{Th_2} \subseteq M_{Th_1}$
(tout modèle de $Th_2$ est aussi modèle de $Th_1$) \underline{alors} $Th_1$ est contenue dans $Th_2$.
Attention à la direction: $M_{Th_2}$ est bien à gauche!
\\

\noindent \underline{Si} $V_{Th_1} \subseteq V_{Th_2}$ et $Ax_{Th_1} \subseteq Ax_{Th_2}$
(tout axiome de $Th_1$ est aussi axiome de $Th_2$) \underline{alors} $Th_1$ est contenue dans $Th_2$.
Il est donc vrai que $M_{Th_2} \subseteq M_{Th_1}$.
On peut donc dire qu'une extension donne lieu à une inclusion (mais pas inversément).\\

\noindent \underline{Si} $V_{Th_1} = V_{Th_2}$ 
et pour tout axiome $p \in Ax_{Th_1}$ nous avons $\models_{Th_2} p$
et pour tout axiome $q \in Ax_{Th_2}$ nous avons $\models_{Th_1} q$,
\underline{alors}
$Th_1$ et $Th_2$ sont équivalentes. \\

\noindent \underline{Si} $p$ une formule fermée telle que $\models_{Th_1} p$ et $Th_2 = Th_1 \bigcup \left\lbrace p \right\rbrace$ \underline{alors} $Th_1$ et $Th_2$ sont équivalentes. \\

\section{Théorie des ordres partiels stricts (OPS)}

Le concept d'ordre partiel strict est une théorie simple qui est très utile en mathématiques.
Nous allons le définir par une théorie.
Ensuite nous donnerons deux interprétations différentes de cette théorie.
\subsection*{Vocabulaire}
\begin{itemize}
\item[$\bullet$] Le symbole P/2
\end{itemize}
\subsection*{Axiomes}
\begin{itemize}
\item[$\bullet$] $ (\forall x) \neg P(x,x) $  (irréflexivité) (OPS1)
\item[$\bullet$] $ (\forall x) (\forall y) (\forall z) (P(x,y) \wedge P(y,z) \Rightarrow P(x,z))$ (transitivité) (OPS2)
\end{itemize}
\subsection*{Première interprétation}
Soit l'interprétation $I$ de cette théorie:
\begin{itemize}
\item[$\bullet$] $D_I = \mathbb{Z} $
\item[$\bullet$] $\mathrm{val}_I (P) = "<"$
\end{itemize}
Lorsque l'on écrit $\mathrm{val}_I(P) = "<"$, le premier symbole $P$ est un mot de vocabulaire dans la théorie
tandis que le deuxième est une fonction sur les entiers.
Cette fonction confère un sens au symbole. 
On remarque que cette interprétation est un modèle de notre théorie.
En effet, la fonction $<$ sur les entiers est irréflexive et transitive.
Si on a $x < y$ et $y <z$, on peut en déduire que $x<z$.

\subsection*{Deuxième interprétation}
Soit l'interprétation $J$ de cette théorie:
\begin{itemize}
\item[$\bullet$] $D_J = \mathbb{Z} $
\item[$\bullet$] $val_J (P) = "\ne"$
\end{itemize}
Ici on change le sens du symbole $P$ :
$$val_J(P) = "\ne"$$
Cette interprétation n'est pas un modèle. En effet, par exemple, pour $x=5, y=3, z=5$, on a :
$$x<y \wedge y<z \nRightarrow x<z$$
$$5 \neq 3 \wedge 3 \neq 5 \nRightarrow 5 \neq 5$$
Ceci est un contre-exemple, car $5$ n'est pas différent de $5$ (irréflexivité),
et donc cette interprétation ne vérifie pas l'axiome sur la transitivité!

% Ancienne partie 13

%document réalisé par Scott Ivinza, Florent Lejoly, Cédric Vanden Buckle et Guillaume Demaude

\section{Théorie de l'égalité (EG)}

Le concept d'égalité est omniprésent dans les mathématiques.
Nous allons définir une théorie pour le formaliser.
D'abord, il faut faire attention à la notation.
Il existe différents symboles pour représenter l'égalité : 
\begin{itemize}
	\item E(x,y)
	\item $x = y$
	\item $x == y $
\end{itemize}
Afin d'éviter la confusion, nous allons utiliser ``$==$'' dans la suite de ce cours pour représenter l'égalité.

La théorie de l'égalité est souvent {\em ajoutée} à d'autres axiomes pour être utile en pratique.
Dans cette section on ne donne que les axiomes d'égalité.  Dans la suite nous allons voir comment
ajouter l'égalité à d'autres théories.

\subsection{Axiomes} 
Pour définir ce qu'est une égalité, nous avons d'abord besoin de définir 3 axiomes et 2 schémas d'axiomes:
\begin{enumerate}
\item Réflexivité \\$\forall x, x==x$
\item Symétrie \\$\forall x, \forall y, x==y \Rightarrow y==x$
\item Transitivité \\$\forall x, \forall y, \forall z, (x==y \land y==z) \Rightarrow x==z$
\item Substituabilité dans les fonctions\\$\forall x, x_{1}, ..., x_i, ..., x_{n}\ .\ x==x_i \Rightarrow f(..., x, ...) == f(..., x_i, ...)$
\item Substituabilité dans les prédicats\\$\forall x, x_{1}, ..., x_i, ..., x_{n}\ .\ x==x_i \Rightarrow P(..., x, ...) == P(..., x_i, ...)$ 
\end{enumerate}
Les deux derniers axiomes sont des {\em schémas}: chaque schéma définit plusieurs axiomes, où on remplace $f$ par tout symbole de fonction et $P$ par tout symbole de prédicat.

\subsection{Règles d'inférence}
En plus de ces 5 axiomes, il nous faut aussi définir deux règles d'inférences.\\ \\
Substituabilité fonctionnelle 
	$$ \frac{s_{1}==t_{1} \land s_{2}==t_{2} \land ... \land s_{n}==t_{n}}{f(s_{1},s_{2},...,s_{n}) == f(t_{1},t_{2},...,t_{n})}$$ 
	Substituabilité prédicative 
	$$ \frac{s_{1}==t_{1} \land s_{2}==t_{2} \land ... \land s_{n}==t_{n}}{P(s_{1},s_{2},...,s_{n}) == P(t_{1},t_{2},...,t_{n})}$$ 

\subsection{Théorème sur la sémantique de l'égalité}

$$\mathrm{Si}\ \ \mathrm{VAL}_{I}(t_{1}) ==  \mathrm{VAL}_{I}(t_{2}) \ \ \mathrm{alors}\ \  \mathrm{VAL}_{I}(t_{1} == t_{2}) = \mathrm{true}$$

L'égalité comme elle est définie ici est une propriété syntaxique qui nous permet de faire des preuves.
Avec ce théorème, nous pouvons aussi raisonner sur un modèle (c'est-à-dire la sémantique) pour déterminer l'égalité.
C'est-à-dire, si deux termes donnent la même entité dans le domaine de discours, alors on peut dire que les
deux termes sont égaux.

\subsubsection{Preuve}

Voici la preuve étape par étape:
\begin{itemize}
\item Soit $I$ un modèle de EG et deux termes quelconques $t_{1}$ et $t_{2}$.
\item Par définition $\mathrm{VAL}_{I}(t_{1} == t_{2}) = \mathrm{VAL}_{I}(==)(\mathrm{VAL}_{I}(t_{1}), \mathrm{VAL}_{I}(t_{2}))$.
\item On pose $VAL_{I}(==) = E_{I}$ et $VAL_{I}(t_{1}) = e_1$ et $VAL_{I}(t_{2}) = e_2$.
\item La prémisse du théorème nous dit que $e_1 = e_2 = e$.
\item Donc $\mathrm{VAL}_{I}(t_{1} == t_{2}) =E_{I}(e,e)$.
\item L'axiome de réflexivité nous dit $\mathrm{VAL}_{I}(\forall x.\ x==x)= \mathrm{true}$.
\item La sémantique de $\forall$ nous dit que pour tout $d \in D_I$, il est vrai que $\mathrm{VAL}_{I}(d==d)=\mathrm{true}$.
\item On prend $d=e$ et on peut conclure que $E_{I}(e,e)=\mathrm{true}$.
\end{itemize}

\vspace{\baselineskip}
Remarquez que ceci n'est pas une preuve en logique des prédicats, mais une preuve en métalangage, c'est-à-dire
une preuve qui parle de la logique des prédicats.
On ne peut pas formaliser cette preuve comme un objet formel qui est une preuve en logique des prédicats.
Toute l'argumentation sur la sémantique de la logique des prédicats et la justification des règles de preuve
sont des raisonnements en métalangage.

\section{Théorie de l'ordre partiel (OP)}

Pour définir la théorie de l'ordre partiel, nous prenons EG \footnote{Il est intéressant de séparer EG de OP car l'égalité est intéressante en soi, et car elle peut être utile pour d'autre théories.} et nous ajoutons un symbole en
plus du symbole d'égalité:
	$$\leq$$
Les axiomes d'égalité sont déjà présents.
Il nous reste de faire les axiomes pour ce nouveau symbole.

\subsection{Axiomes} 

Aux axiomes et schémas d'axiomes de la théorie de l'égalité, on rajoute de nouveaux axiomes:
\begin{enumerate}
\item Réflexivité \\$\forall x$, $x\leq x$
\item Anti-symétrie \\$\forall x$, $\forall y$, $ x\leq y \land y\leq x\Rightarrow y==x$
\item Transitivité \\$\forall x$, $\forall y$, $\forall z$, $(x\leq y \land y\leq z) \Rightarrow x\leq z$
\item Substituabilité à gauche \footnote{Obtenu en utilisant $\leq$ comme prédicat P dans substituabilité des prédicats pour EG} \\$\forall x_{1}$, $\forall x_{2}$, $\forall x$,  $x_{1}==x \Rightarrow x_{1}\leq x_{2} \Leftrightarrow x \leq x_{2}$
\item Substituabilité à droite \\$\forall x_{1}$, $\forall x_{2}$, $\forall x$,  $x_{2}==x \Rightarrow x_{1}\leq x_{2} \Leftrightarrow x_{1} \leq x$
\end{enumerate}

\subsection{Exemple de théorème}

Nous allons prouver le théorème suivant:
$$\models \forall x.\ \forall y.\  [x==y \Leftrightarrow (x\leq y)\land (y \leq x)] $$

\subsubsection{Preuve}

\begin{itemize}
\item $\Leftrightarrow$ equivaut à $\Leftarrow \land \Rightarrow$.
\item $\Leftarrow$ est démontré immédiatement par l'axiome antisymétrique.
\item $\Rightarrow$ demande à démontrer $\models{}\ \forall x.\ \forall y.\ [x==y \Rightarrow x\leq y \land y \leq x]$.
\end{itemize}
Il nous reste de démontrer $\Rightarrow$.

\begin{enumerate}
\item $ \forall x.\ \forall y.\ \forall z.\ x==y \Rightarrow z \leq x \Leftrightarrow y \leq x$ \hfill substituabilité à gauche
\item $ \forall x.\ \forall y.\ x==y \Rightarrow x \leq x \Leftrightarrow y \leq x$ \hfill $\forall$ Élimination
\item $ x==y \Rightarrow x \leq x \Leftrightarrow y \leq x $ \hfill $\forall$ Élimination (2 fois)
\item $ \forall x.\ \forall y.\ \forall z.\ x==y \Rightarrow x \leq z \Leftrightarrow x \leq y$ \hfill substituabilité à droite
\item $ \forall x.\ \forall y.\ x==y \Rightarrow x \leq x \Leftrightarrow x \leq y$ \hfill $\forall$ Élimination
\item $ x==y \Rightarrow x \leq x \Leftrightarrow x \leq y $ \hfill $\forall$ Élimination (2 fois)
\item $ \quad \quad x==y$ \hfill Supposition (conditionnel)
\item $ \quad \quad y\leq x$ \hfill Modus ponens (3,7)
\item $ \quad \quad x\leq y$ \hfill Modus ponens (6,7)
\item $ \quad \quad y\leq x \land  x\leq y$ \hfill Conjonction (8,9)
\item $ x==y \Rightarrow y\leq x \land  x\leq y$ \hfill Conclusion
\item $ \forall x.\ \forall y.\ x==y \Rightarrow y\leq x \land  x\leq y$ \hfill $\forall$ Introduction (2 fois)
\end{enumerate}
Les lignes (8) et (9) sont légèrement simplifiés: pour la rigueur il faut utiliser la réflexivité
et la définition de l'équivalence.
Je vous laisse cela en exercice.

\subsection{Exemples de modèles d'OP}

Les ordres partiels sont omniprésents dans les mathématiques et l'informatique.
En voici quelques exemples.
\begin{itemize}
\item \underline{$I_{1}$} : $D_{I_{1}} =  \mathbb{Z}$ \\
$ val_{I_{1}}(==) = '=' :$ égalité d'entiers \\
$ val_{I_{1}}(\leq) = '\leq' :$ plus petit ou égal pour les entiers\\
Cette interprétation va satisfaire tous les entiers.
\item \underline{$I_{2}$} : $D_{I_{2}} =  P(E)$ ensemble des sous-ensembles de E\\
$ val_{I_{2}}(==) = '=' :$ égalité d'ensemble \\
$ val_{I_{2}}(\leq) = '\subseteq' :$ inclusion d'ensemble
\item \underline{$I_{3}$} : $D_{I_{3}} = ALPH^{2} = {(l_{1},l_{2}),..}$ doublons de lettres de l'alphabet\\
$ val_{I_{3}}(==) = $ égalité des paires \\
$ val_{I_{3}}(\leq) =$ suivant ordre lexicographique\\
Exemple : $(l_{i},l_{j}) \leq (l_{p},l_{q})$ si $ l_{i} < l_{p}$ ou $ l_{i} = l_{p}$ et $ l_{j} < l_{q}$ ou $ l_{j} = l_{q}$
\item \underline{$I_{3}$} : $D_{I_{4}} =$ ensemble de listes\\
$ val_{I_{4}}(==) = $ = égalité de liste (si elles possèdent les mêmes composants à la même position)\\
$ val_{I_{3}}(\leq) =$ "suffixe de" \\
Exemple : $l_{1} $ est suffixe de $l_{2}$ \\
$l_{1} $ = [d, e, f, g, h] et $l_{2} =$ [a, b, c, d, e, f, g, h, i]
\item \underline{$I_{5}$} : Soit D$_{I_{5}}$ l'ensemble des formules en logique des propositions. On commence à utiliser la logique pour parler d'elle-même:\\
VAL$_{I_{5}}$(==) = "$\Lleftarrow \Rrightarrow$" : L'égalité est synonyme d'équivalence en logique des propositions \\
VAL$_{I_{5}}$($\leq$) = "$\models$" : Le signe d'inclusion entre les ensembles de modèles.
Maintenant qu'on a défini la sémantique de l'ordre partiel en utilisant la notion de modèles, on peut prendre quelques exemples en raisonnant sur la logique :\\
p $\leq_{I_{5}}$ q   \hspace{1.5cm} p $\models_{I_{5}}$ q \hspace{1.5cm} $\models$ p $\Rightarrow$ q
\item \underline{$I_{6}$} : D$_{I_{6}}$ = l'ensemble des unificateurs d'un ensemble S de termes ou de formules
VAL$_{I_{6}}$(==) = égalité entre substitutions \{ (x$_{i}$,t$_{i}$)... \} : un ensemble de paires avec une variable et un terme VAL$_{I_{6}}$($\leq$) = "moins général que"\\
\newline
Exemple: $P(x,f(y))$ \hspace{1cm} $\underbrace{P(x,z)}_{\sigma_1}$\\
$\sigma$' = $\sigma$ $\cup$ \{(z, f(y)\} donc 
$\sigma$' $\leq$ $\sigma$\\
\end{itemize}
Ces exemples montrent qu'on peut raisonner sur tout, y compris sur la logique et les algorithmes eux-mêmes,
à partir du moment où on respecte les axiomes.
Ce qui est métalangage dans un raisonnement peut devenir langage dans un autre raisonnement apparenté.

% Ancienne partie 14

%\section*{Suite des exemples de la première heure}

\section{Théorie des ensembles}

Nous introduisons une version simple de la théorie des ensembles
comme prérequis pour la spécification des systèmes avec l'approche Z.
Informellement, il y a deux manières de définir des ensembles:
\begin{itemize}
\item Un ensemble peut être défini comme une énumération d'éléments, comme par exemple
\{0,20,40,60,80,100 \} ou \{Mercure, Vénus, Terre, ..., Neptune\}.
\item Un ensemble peut également être défini avec un prédicat d'un argument qui est vrai pour les membres.
On appelle cette définition une {\em compréhension}.
Certains langages de programmation (comme Python ou Haskell) possèdent des syntaxes particulières dédiées
à la création de listes remplies par des compréhensions.
Par exemple: \{ n | n $\in$ $\mathbb{N}$ $\wedge$ $\exists$ k, k $\in$ $\mathbb{N}$ $\wedge$ 20k = n $\wedge$ 0 $\leq$ n $\leq$ 100 \}.
\end{itemize}
Les axiomes vont en partie suivre cette intuition.
Nous introduisons maintenant les axiomes pour les ensembles.

\textbf{Axiomes}

\begin{itemize}
\item \textbf{Égalité} (première définition) \\
A = B $\Leftrightarrow$ ($\forall$ x) (x $\in$ A $\Leftrightarrow$ x $\in$ B)\\
\item \textbf{Ensemble vide} (sans éléments)\\
$\emptyset$ = \{\} = \{x $\vert$ x $\neq$ x\}\\
\item \textbf{Ensemble universel} (tous les éléments du domaine)\\
$\mathcal{U}$ (par exemple: $\mathbb{N}$, $\mathbb{R}$, $\mathbb{Z}$)\\
\item \textbf{Sous-ensemble}\\
A $\subseteq$ B $\Leftrightarrow$ ($\forall$ x) (x $\in$ A $\Rightarrow$ x $\in$ B)\\
A $\nsubseteq$ B $\Leftrightarrow$ $\neg$(A $\subseteq$ B)\\
A $\subset$ B $\Leftrightarrow$ A $\subseteq$ B $\wedge$ A $\neq$ B\\
\item \textbf{Construction de sous ensemble} \\
A $\subseteq$ B $\Leftrightarrow$ (x $\in$ A $\Leftrightarrow$ x $\in$ B $\wedge$ $\varphi$(x))\\
On va ici prendre des éléments de B tels que $\varphi$(x) est vrai, et les mettre dans A. C'est un peu une formulation de la notion de compréhension.\\ 
\item \textbf{Propriétés}\\
$\emptyset$ $\subseteq$ A\\
A $\subseteq$ A\\
A $\subseteq$ B $\wedge$ B $\subseteq$ C $\Rightarrow$ A $\subseteq$ C \\
\item \textbf{Égalité} (2e définition)\\
(A = B) $\Leftrightarrow$ (A $\subseteq$ B) $\wedge$ (B $\subseteq$ A)\\
\item \textbf{Taille d'un ensemble} 
    \begin{itemize}
    \item Prédicat à 2 arguments\\
    \#(A,n) : A contient n éléments\\
    \#$\emptyset$ = 0  $\rightarrow$ \#($\emptyset$, 0) 
    \item $\mathbb{P}$A = \{a $\vert$ a $\subseteq$ A\} (prédicat à 2 arguments) : ensemble des sous-ensembles de A\\
    \#$\mathbb{P}$A = 2$^{\#A}$ \\
    \end{itemize}
\end{itemize}

\subsection{Spécification formelle avec l'approche Z}

L'approche Z utilise la logique des prédicat et est basée sur la théorie des ensembles.
C'est une approche ``orientée modèle''': on ne donne pas que les équations, mais aussi la structure du système.
Dans cette section nous donnons une introduction à l'approche Z avec un exemple simple
de gestion de stock dans une bibliothèque.

\subsubsection{Concepts en Z}

Type:\\
\begin{itemize} 
\item {\em Types génériques} (ensembles): par exemple : Book, Location
\item {\em Types énumérés}: par exemple : \\
Status := $\underbrace{\mathit{In}}_{Dans \hspace{0.1cm} la \hspace{0.1cm} bibliothèque, \hspace{0.1cm} disponible}$ $\vert$ $\overbrace{\mathit{Out}}^{Prêté}$ $\vert$ $\underbrace{\mathit{Ref}}_{Livre \hspace{0.1cm} de \hspace{0.1cm} référence}$ \\
\end{itemize}

Schéma d'un état:\\
\begin{itemize}
\item {\em Nom}: le nom d'un état du système
\item {\em Signature}: une énumération des variables utilisées avec leurs types
\item {\em Prédicat}: formule en logique des prédicats qui décrit l'état du système\\
\end{itemize}

Schéma d'un comportement:\\
\begin{itemize}
\item {\em Nom}: le nom d'un comportement du système
\item {\em Signature}: une description de la transformation faite par le comportement
\item {\em Précondition}: formule en logique des prédicats, ce qui doit être vrai avant pour que le composant soit applicable
\item {\em Postcondition}: formule en logique des prédicats, ce qui est vrai après l'application du composant
\end{itemize}
La définition d'un comportement utilise une sémantique et une syntaxe particulière pour décrire les transformations d'état.
Une exécution est une séquence d'états et chaque application d'un composant avant l'exécution d'un pas avec
un avant et un après:
\begin{center}
\includegraphics[scale=0.5]{images/14_sequence.png} 
\end{center}
Les variables avant sont écrites normalement (Lib\_Stock) et les variables après sont écrites avec un apostrophe
(Lib\_Stock').
Il y a une syntaxe particulière pour décrire ce qui se passe avec les états avant et après:
\begin{itemize}
\item $\Delta$ Lib\_Stock: état avant (Lib\_Stock) et après (Lib\_Stock')
\item $\Xi$ Lib\_Stock: état avant et après s'ils sont identiques
\end{itemize}
Les définitions de ces deux symboles sont:
\begin{itemize}
\item $\Delta$ Lib\_Stock $\triangleq$ Lib\_Stock $\wedge$ Lib\_Stock'
\item $\Xi$ Lib\_Stock $\triangleq$ Lib\_Stock $\wedge$ Lib\_Stock' $\mid$ Lib\_Stock=Lib\_Stock'
\end{itemize}

\subsubsection{Exemple d'un état}

\begin{center}
\newcolumntype{M}[1]{>{\raggedright}m{#1}}
	\begin{tabular}{|l|M{7cm}|}
    	\hline
    	nom & \hspace{2cm} LIB\_STOCK \tabularnewline
    	\hline
    	signature & stock\\ on\_loan\\ on\_shelf\\ ref\_coll : $\mathbb{F}$ Book  \tabularnewline
    	\hline
    	prédicat & stock = on\_loan $\cup$ on\_shelf\\ on\_loan $\cap$ on\_shelf = $\emptyset$\\ ret\_call $\subseteq$ on\_shelf \tabularnewline
    	\hline
 	\end{tabular}
\end{center}
La notation $\mathbb{F}$ Book représente un sous-ensemble {\em fini} de l'ensemble Book.\\

\subsubsection{Exemple d'un comportement}

\begin{center}
\newcolumntype{M}[1]{>{\raggedright}m{#1}}
	\begin{tabular}{|l|M{7cm}|}
    	\hline
    	nom & \hspace{2cm} ADD\_STOCKo \tabularnewline
    	\hline
    	signature & $\Delta$ Lib\_Stock\\ new ? : $\mathbb{F}$  Book \tabularnewline
    	\hline
    	prédicat & new ? $\neq$ $\emptyset$ \hfill $\rightarrow$ précondition\\ new ? $\wedge$ stock = $\emptyset$ \hfill $\rightarrow$ précondition\\ stock' = stock $\cup$ new ? \hfill $\rightarrow$ postcondition\\ on\_loan' = on\_loan \hfill $\rightarrow$ postcondition\tabularnewline
    	\hline
 	\end{tabular}

\end{center}
Le "?" signifie qu'il s'agit d'une entrée.
On peut déduire de ces prédicats que new? sera dans on\_shelf.
Si la ou les préconditions ne sont pas satisfaites, on aura des erreurs que l'on devra corriger via la gestion d'erreurs.
Si les préconditions n'échouent jamais, on a affaire à une opération totale.

\subsubsection{Exemple d'opération totale}

On peut définir une operation totale en ajoutant un traitement d'erreur:

ADD\_STOCK = ADD\_STOCK${}_0$ $\cup$ ERRONEOUS\_NEW\_STOCK

\begin{center}
\newcolumntype{M}[1]{>{\raggedright}m{#1}}
	\begin{tabular}{|l|M{8.5cm}|}
    	\hline
    	nom & \hspace{1cm}ERRONEOUS\_NEW\_STOCK \tabularnewline
    	\hline
    	signature & $\Xi$ Lib\_Stock\\ new ? : \# Book\\ rep! : Report \tabularnewline
    	\hline
    	prédicat & (new ? = $\emptyset$ $\vee$ new ? $\cap$ stock $\neq$ $\emptyset$) \hfill $\rightarrow$ préconditions\\ rep ! = "Attention stock problem" \tabularnewline
    	\hline
 	\end{tabular}

\end{center}
Le "!" signifie qu'il s'agit d'une sortie.