partie6et7.tex

%Packages à ajouter pour la compilation
%\usepackage{amsmath}
%\usepackage{lmodern}
%\usepackage{vmargin}
%\usepackage{tabularx}
%\usepackage[usenames,dvipsnames]{color}
%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 : $val_{I}(P) = $ $ \geq $ \hspace{3mm} (\textit{considéré comme un vrai prédicat})
\item[$\bullet$] a : $val_{I}(a) = $ $ \sqrt{2} $ 
\item[$\bullet$] b : $val_{I}(b) = $ $ \pi $ 
\item[$\bullet$] $f$ : $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 : $val_{I}(a) = $ "Barack Obama"
\item[$\bullet$] b : $val_{I}(b) = $ "Vladimir Putin"
\item[$\bullet$] $f$ : $val_{I}(f) = $ $ f_{i} $ \hspace{3mm} $f_{i}: d \rightarrow \mathrm{père}(d)$
\item[$\bullet$] P :  $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}

% \section{Différence avec la logique des propositions}
% Les trois différences entre les deux logiques sont:
% \begin{enumerate}
% \item les variables,
% \item les quantificateurs,
% \item les symboles de fonction (moins important).
% \end{enumerate}  
% Imaginons un modèle $B:
% \{
%   \begin{array}{rcr}
%     P_{1},...P_{n}
%   \end{array}
% \}
% $
% Si nous utilisons une interprétation I pour B cela donne:
% $\forall P_{I} \in B : VAL_{I} (P_{I}) = True$ qui est très générale, car $P_{I}$ peut avoir des variables, des quantificateurs ...

% partie 1 (15 à 30 min) Thomas)

\section{Preuves avec règles}

Comme pour la logique propositionnelle, il est important de pouvoir faire des preuves avec la logique des prédicats.
Il y a deux approches principales: la preuve manuelle et la preuve automatisée.
Pour les deux approches, la preuve est toujours un objet mathématique, une séquence de déductions avec ses formules et
ses justifications, qui sont une application des règles de preuve.

\subsection{Preuves manuelles}

Les preuves manuelles sont le sujet du chapitre \ref{preuvemanuelle}.

\subsection{Preuves automatisées}

Les preuves automatisées sont le sujet du chapitre \ref{algorithmepreuve}.
L'algorithme de preuve que nous allons définir est une généralisation de l'algorithme pour la logique propositionnelle.
Il y a toujours :
\begin{itemize}
  \item Une règle de résolution pour les preuves automatisées, mais celle-ci est plus générale. Elle va utiliser un concept appelé
``unification''. Ce nouveau concept est nécessaire à cause des variables.
En effet, celles-ci peuvent être différentes, il faut donc trouver un nouveau moyen de les fusionner.
  \item Une forme normale, qui  est plus compliquée à cause des quantificateurs et des symboles de fonctions, mais qu'il est encore possible de l'obtenir.
  \item Un algorithme avec ses propriétés. Mais il est moins fort/complet que l'algorithme développé pour la logique des propositions. Il ne sera plus décidable, mais seulement semi-décidable. C'est-à-dire que parfois il tournera en boucle. Cela est dû aux variables et aux quantificateurs. La logique des prédicats est beaucoup plus riche que la logique des propositions, mais en contrepartie l'algorithme arrive à prouver moins de choses. Cependant, l'algorithme sera toujours adéquat, mais pas forcément complet. Il ne sera pas toujours possible de trouver une preuve, même quand elle existe parce qu'elle sera trop compliquée.
\end{itemize}
Qu'est il possible de faire avec ce genre d'algorithme moins fort?

\subsubsection{L'utilisation de l'algorithme de preuve}

Il y a deux possibilités : 
\begin{itemize}
\item {\em Un assistant de preuve}
C'est un outil qui aide les gens à faire des preuves formelles. Deux exemples d'assistants de preuves sont Coq et Isabelle. C'est un outil très sophistiqué, mais 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 ... Ensuite, l'algorithme s'occupe de la manipulation des symboles.\\
Un exemple très célèbre est le théorème de la coloration d'une carte. 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.
\item {\em Un langage de programmation}
L'algorithme peut être considéré comme le moteur d'un programme. C'est ce qu'on appelle maintenant la programmation logique. Elle consiste à utiliser la logique dans un programme. Le langage le plus célèbre qui a suivi cette approche est Prolog. Ce fut un énorme succès, car les gens ne croyaient pas que c'était possible de faire un programme en logique qui pouvait tourner. Cela a donné naissance à la programmation par contraintes (une contrainte est une relation logique). Cette discipline est très utile pour les optimisations, par exemple dans le cas du "voyageur de commerce".
\end{itemize}

La logique des prédicats n'est donc pas quelque chose de seulement théorique, destiné uniquement aux mathématiciens.
Elle a été utilisée avec succès dans les programmes.

%partie 3 de 30 à 45 min (Guillaume)

\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. Cela reste un objet formel.

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

La méthode pour passer de $\forall x \cdot P(x) \wedge Q(x)$ (prémisse) à $\forall x \cdot P(x)\wedge(\forall x \cdot Q(x))$ (conclusion) est la suivante:
\begin{center}
$
\begin{array}{l l}
  1. & $Enlever les quantificateurs pour avoir des variables libres$ \\
  2. & $Raisonner sur l'intérieur$\\
  3. & $Remettre les quantificateurs$\\
\end{array}
$
\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 $ \forall \\
  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.
\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$.
\end{framed}

\section{Règles en logique des prédicats}
En logique des prédicats, pour trouver une preuve, on va faire des manipulations de formules.

\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 $p[x/t]$ (où $p$ veut dire "toutes les formules"). On va remplacer toutes les occurrences libres de $x$ par $t$.\\
On peut aussi écrire cela de la manière suivante :\\
$p[x/t]$ possède deux portées :
\begin{itemize}
\item[] La première se note $p[x]$ et correspond à une partie de la règle.
\item[] La seconde se note $p[t]$ et correspond à l'autre partie de la règle.\\
\end{itemize}

Exemple :
\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 \textbf{capture de variable}, car la variable $y$ est capturée par le quantificateur. Pour résoudre ce problème, on va effectuer un \textbf{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).\tabularnewline
\hline
\end{tabular}
\end{center}