modif algo euclide

[cours-maths-dis.git] / logique / Propositions2.tex

\section{Présentation de la théorie de la démonstration}


Il s'agit ici d'explorer les mécanismes du raisonnement humain, 
c'est-à-dire les schémas de pensée qui nous permettent de décider 
d'agir d'une certaine manière, dans le but d'obtenir un certain 
résultat.

% Nous disposons en fait d'une \og base de connaissances\fg{} qui fait 
% que nous savons que, dans telles ou telles circonstances, certaines 
% causes produisent certains effets. Pour obtenir ces effets, nous 
% essayons de nous replacer dans les conditions de leur réalisation.

% \subsection{Système formel et règles d'inférences}

% Un système formel qui est chargé de reproduire mécaniquement ce 
% fonctionnement est constitué d'{\sl axiomes logiques\/}, qui jouent 
% le rôle de \og connaissances de base\fg{} ; il s'agit de formules de 
% logique qui servent de \og points de départ\fg{}  aux déductions 
% ultérieures.

% Puis, le système est muni de \og règles d'inférence\fg{}, qui sont 
% chargées de simuler les divers modes de raisonnement que nous 
% utilisons.

En théorie de la démonstration, une preuve est un objet mathématique.
Elle est classiquement représentée comme une structure de donnée 
(liste, arbre,\ldots). Elle est construite à l'aide d'axiomes logiques 
et de règles d'inférence.  Plus formellement:

\begin{Def}[Axiome Logique]\index{axiome logique}  
Un \emph{axiome logique} est une tautologie qui sert 
de \og point de départ\fg{} aux déductions du système formel.
\end{Def}

\begin{Def}[Règle d'inférence]\index{règle d'inférence}
Une \emph{règle d'inférence} est une règle qui, à partir de 
formule(s) \emph{prémisses}, produit une formule \emph{conclusion}. 
\end{Def}


%\subsection{Statut des axiomes logiques}

% Il convient de distinguer les axiomes logiques des autres axiomes qui
% peuvent être posés dans divers domaines (par exemple, en géométrie,
% l'axiome d'Euclide); ces axiomes n'appartiennent pas à la logique et
% autorisent la construction d'une théorie (la géométrie euclidienne en
% l'occurrence). 

% Il faut aussi les distinguer des axiomes posés au sujet de la logique
% elle-même, comme, par exemple, celui que nous avons appelé le principe
% de non-contradiction% . 
% Ces axiomes énoncés {\sl au sujet de\/} la logique, ne sont pas non
% plus des axiomes logiques. 

% Ils jouent le même rôle, pour la logique, que l'axiome d'Euclide pour
% la géométrie : ils conduisent à la 
% construction d'une certaine logique, étant bien entendu que d'autres
% axiomes peuvent conduire à la construction d'autres logiques que celle
% qui est l'objet du présent chapitre.  Plus précisément :

%\paragraph{Théorème logique}

\begin{Def}[Théorème logique]
Un résultat obtenu par une déduction correcte ou une suite de
déductions correctes (c'est-à-dire qui utilisent explicitement les
règles d'inférence autorisées) à partir des axiomes logiques et, 
éventuellement, d'autres résultats du même type déjà établis par
ailleurs s'appelle un \emph{théorème
  logique}\index{théorème!logique}. 
\end{Def}

On exprime que la formule  $F$ est un théorème par la notation :
$\theor F$, qui se lit \og $F$ est un théorème \fg{}. 




\begin{Def}[Démonstration] 
La chaîne de déductions qui conduit à un théorème logique est appelée
\emph{démonstration} \index{démonstration} de ce résultat. 
\end{Def}




Il est possible d'utiliser des formules logiques supplémentaires 
(autres que des axiomes ou des théorèmes) et de mener un raisonnement 
correct à partir de ces formules (et des axiomes et des théorèmes 
déjà connus). On parle alors de \emph{démonstration sous hypothèses}.
L'affirmation \og la formule logique $H$ est démontrée
sous les hypothèses $G_1,G_2,\ldots,G_n$\fg{}  est notée 
$\{G_1,G_2,\ldots,G_n\}\theor H$. 



\section{Axiomes logiques et règles d'inférence du système formel \og PR  \fg{}} Il existe plusieurs systèmes d'axiomes qui permettent de 
définir la logique propositionnelle. Nous nous en tiendrons à 
l'ensemble des axiomes suivants, qui n'est ni minimal, ni 
contradictoire.


\paragraph{Axiomes relatifs à l'implication logique : }

\begin{itemize}

\item Axiome 1 : $P\imp (Q\imp P)$
\item Axiome 2 : $(P\imp Q)\imp((P\imp(Q
\imp R))\imp (P\imp R))$

\end{itemize}

\paragraph{Axiomes relatifs à la conjonction logique : }

\begin{itemize}

\item Axiome 3 : $P\imp(Q\imp P\et Q)$
\item Axiome 4 : $P\et Q\imp P$
\item Axiome 5 : $P\et Q\imp Q$

\end{itemize}

\paragraph{Axiomes relatifs à la disjonction logique : }

\begin{itemize}

\item Axiome 6 : $P\imp P\ou Q$
\item Axiome 7 : $Q\imp P\ou Q$
\item Axiome 8: $(P\imp R)\imp((Q\imp R) \imp(P\ou Q\imp R))$
\end{itemize}



\paragraph{Axiomes relatifs à la négation logique : }

\begin{itemize}

\item Axiome 9: $\non\non P\imp P$
\item Axiome 10: $(P\imp Q)\imp((P\imp\non Q)
\imp\non P)$

\end{itemize}

\paragraph{Axiomes relatifs à l'équivalence logique : }

\begin{itemize}

\item Axiome 11 : $(P\imp Q)\imp((Q\imp P)\imp(P\eqv Q))$
\item Axiome 12 : $(P\eqv Q)\imp(P\imp Q)$
\item Axiome 13 : $(P\eqv Q)\imp(Q\imp P)$

\end{itemize}


On définit la règle d'inférence 
du \emph{modus ponens} (le mode \og en posant, on
  pose\fg{}) : 
$$\{P,P\imp Q\}\theor Q$$

% \og Des formules $P$ et $P \imp Q$, on peut déduire par modus ponens
% la formule Q \fg{}. 

% \paragraph{\og modus tollendo tollens\fg{}} 
%   (le mode \og en niant, on nie\fg{}):\\ 
% $\{P\imp Q,\non Q\}\theor\non P$.

% % \paragraph{\og modus ponendo tollens\fg{}}  (le mode \og en posant, on
% %   supprime\fg{}): \\ 
% % $\{\non(P\et Q),P\}\theor\non Q$.

% % \paragraph{\og modus tollendo ponens\fg{}}  (le mode \og en
% % supprimant,  on pose\fg{}) : \\
% % $\{P\ou Q,\non P\}\theor Q$. 


% \begin{Rem}
%  Les noms sont traditionnellement des noms latins, utilisés depuis les
%  philosophes du XVI\up{ème} siècle. 
% \end{Rem}


% Une brève étude montrerait que ces deux  règles sont équivalentes.
% Il est donc possible de n'en conserver qu'une seule, qu'on appelle le
% \og modus (sous-entendu : ponendo) ponens\fg{}, ou {\sl règle 
% de détachement\/} et qui est la première.


\begin{Def}[Système formel \og PR \fg{}]
Le système formel composé des 13 axiomes précédents et du modus ponens
est nommé \og \emph{PR} \fg{}.
\end{Def}


% \begin{Rem}
% Sinon, il serait possible de supprimer quelques axiomes. Mais il
% vaut mieux, dans un but ultime de programmation, diminuer le nombre
% de règles d'inférence que celui d'axiomes. 
% \end{Rem}



% Cependant, dans le but de raccourcir au maximum les démonstrations
% ou déductions à faire à la main, nous nous conformerons à l'usage et
% conserverons les quatre règles classiques. 



\section{Démonstrations avec ou sans hypothèses}

Un raisonnement logique peut être rédigé sous forme de démonstration, 
soit d'un théorème, soit d'une conséquence de certaines hypothèses.

\subsection{Démonstration d'un théorème}

La démonstration d'un théorème est constituée :

\begin{enumerate}
\item d'un en-tête, portant l'indication \og  \sou{Démonstration}\fg{}; 
%(de  manière à l'isoler totalement du contexte), 
\item puis d'un certain nombre de lignes, numérotées (pour pouvoir
  être référencées dans la suite); Chacune   comporte deux champs : 
\begin{enumerate}
\item une formule, qui est le \og résultat\fg{}
  de la ligne courante;
 \item la justification du résultat;
 \end{enumerate}
\item une dernière ligne, non numérotée, qui
  porte l'en-tête \og \sou{Conclusion}\fg{}. 
\end{enumerate}



Dans une ligne, on peut avancer :
\begin{itemize}
\item un axiome en remplaçant éventuellement une variable par une formule;
\item un théorème considéré comme connu 
  (dont la démonstration a été vue par ailleurs),
  en remplaçant éventuellement une variable par une formule;
\item un résultat de l'application d'une règle d'inférence
  sur des formules écrites dans les lignes précédentes.
\end{itemize}


\begin{Ex}[Théorème de réflexivité de l'implication]$ $ 
Soit $P$ une formule propositionnelle.
On souhaite démontrer le 
\emph{théorème de réflexivité de l'implication}:
$$
\theor(P\imp P).
$$

\sou{Démonstration} :\par
\begin{tabular}{l l l}
  \x{1} & $(P\imp(P\imp P))\imp((P\imp((P\imp P)\imp  P))\imp(P\imp P))$ 
  & Axiome 2 ($P\imp P/Q$, $P/R$ ) \\ 
  \x{2} & $P\imp(P\imp P)$ 
  & Axiome 1 ($P/Q$)\\
  \x{3} & $(P\imp((P\imp P)\imp P))\imp(P\imp P)$
  & m.p. sur \x{2} et \x{1} \\ 
  \x{4} & $P\imp((P\imp P)\imp P)$ 
  & Axiome 1 ($P \imp P /Q$) \\
  \x{5} & $(P\imp P)$ 
  & m.p. sur \x{4} et \x{3} \\
\end{tabular}

\sou{Conclusion} :  $\theor(P\imp P)$
\end{Ex}



\subsection{Démonstration sous hypothèses}

Une démonstration sous hypothèses \ldots 
\begin{enumerate}
\item commence par une première ligne qui comporte les mots \og
  \sou{Démonstration sous les hypothèses}\fg{} suivie de l'écriture de l'ensemble des
  hypothèses utilisées;
\item puis, comme dans une démonstration de théorème, de lignes numérotées \ldots 
dans lesquelles peuvent figurer les mêmes éléments, auxquels il faut
 ajouter les hypothèses, dont on a le droit de se servir comme s'il 
s'agissait de résultats établis ;
\item une ligne de  conclusion qui rappelle les hypothèses. 
\end{enumerate}

% Dans la pratique, dans un but d'économie de place (la moindre
% démonstration peut très vite prendre de nombreuses lignes), on
% s'autorisera d'autres éléments (par exemple, l'utilisation de la 
% technique de l'hypothèse supplémentaire), qui seront vus dans la suite.


\begin{Ex}[Modus (tollendo) tollens]$ $ \\
L'objectif est d'obtenir 
$\{P\imp Q\vir\non Q\}\theor \non P$
qui est plus connu sous le nom 
\og modus (tollendo) 
tollens\fg{}.

Soit $P$ et $Q$ des formules propositionnelles quelconques, 
montrons $\non P$ sous les hypothèses $P\imp Q$ et $\non
Q$: 

\sou{Démonstration sous les hypothèses} $\{P\imp Q\vir\non Q\}$

\begin{tabular}{l l l}
  \x{1} & $(P\imp Q)\imp((P\imp\non Q)\imp\non P)$ 
  & Axiome 10 \\
  \x{2} & $P\imp Q$ 
  & Hypothèse 1 \\
  \x{3} & $(P\imp\non Q)\imp\non P$ 
  & m.p. sur \x{2} et \x{1}  \\
  \x{4} & $\non Q\imp(P\imp\non Q)$ 
  & Axiome 1 \\
  \x{5} & $\non Q$ 
  & Hypothèse 2 \\
  \x{6} & $(P \imp\non Q)$ 
  & m.p. sur \x{5} et \x{4} \\
  \x{7} & $\non P$ 
  & m.p. sur \x{6} et \x{3}\\ 
\end{tabular}

\sou{Conclusion} : $\{P\imp Q\vir\non Q\}\theor \non P$.

\end{Ex}






% AG : Ce qui suit n'est pas un théorème, démontrable dans le système
% PR, mais un méta-théorème, prouvé informellement, à propos du système
% PR, dont il exprime une propriété utile. Le discours doit être revu
% jusqu'à la fin de la partie IV.

%, mais la
%démonstration de ce dernier utilise le théorème d'idempotence. 



\section{Théorème de la déduction}

Les démonstrations sont souvent considérablement simplifiées par
l'utilisation du théorème de la déduction donné ci-après.
%Il s'agit du résultat qui équivaut, en théorie de la démonstration,
%au théorème de la validité en théorie des valeurs de vérité.

\begin{Th}[Théorème de la déduction]
 \index{théorème!de la déduction}
Ce théorème s'énonce par :
$$ 
\{G_1,G_2,\ldots,G_n\}\theor H  \textrm{ si et seulement si }
\{G_1,G_2,\ldots,G_{n-1} \}\theor G_n\imp H$$
\end{Th}


\begin{Proof}
La démonstration s'effectue par récurrence sur la longueur de la
déduction. 
\paragraph{Seulement si.}
Hypothèse : $\{G_1,G_2,\ldots,G_n\}\theor H$.
Soit $p$ la longueur de la déduction qui amène à $H$.
\begin{itemize}
\item Si $p=1$ : une \og déduction de longueur 1\fg{}  n'autorise
  l'écriture que d'une seule ligne. Cela signifie donc que l'on peut
  directement écrire $H$ dans 
celle-ci. Ce n'est possible que si $H$ est un axiome ou une hypothèse. 
\begin{itemize}
\item Si $H$ est un axiome :\psaut
\sou{Démonstration sous les hypothèses} 
$\{G_1,G_2,\ldots,G_{n-1}\} :$

\begin{tabular}{l l l} 
  \x{1}  & $H\imp (G_n\imp H)$ 
  & Axiome 1 \\
  \x{2}  & $H$ 
  & Axiome j \\
  \x{3}  & $G_n\imp H$ 
  & m.p. sur \x{2} et \x{1} \\
\end{tabular}\par

\sou{Conclusion} :   $\{G_1,G_2,\ldots,G_{n-1}\}\theor G_n\imp H$

\psaut
Dans ce premier cas : $\{G_1,G_2,\ldots,G_n\}\theor H$ implique
$\{G_1,G_2,\ldots,G_{n-1}\}\theor G_n\imp H$ (Les hypothèses
ne sont en fait pas utilisées, donc elles n'interviennent pas).
\item Si $H$ est l'une des hypothèses $\{G_1,G_2,\ldots,G_{n-1}\}$,
  posons 
$H=G_i\ (0<i<n)$ :
\sou{Démonstration sous les hypothèses} 
$\{G_1,G_2,\ldots,G_{n-1}\} :$

\begin{tabular}{l l l}
  \x{1}  & $G_i\imp(G_n\imp G_i)$ 
  & Axiome 1 \\
  \x{2}  & $G_i$
  & Hypothèse \\
  \x{3}  & $G_n\imp G_i$
  & m.p. sur \x{2} et \x{1} \\
\end{tabular}\par
\sou{Conclusion} : $\{G_1,G_2,\ldots,G_{n-1}\}\theor G_n\imp H$
\psaut
Dans ce deuxième cas : $\{G_1,G_2,\ldots,G_n\}\theor H$ implique
$\{G_1,G_2,\ldots,G_{n-1}\}\theor G_n\imp H$ (Seule
l'hypothèse $G_i$ a été utilisée, les autres ne sont en fait pas
utilisées, elles n'interviennent pas).
\item Si $H$ est l'hypothèse $G_n$ : Alors on sait que :
$\theor G_n\imp G_n$ (voir paragraphe précédent).\par
Dans ce troisième cas : $\{G_1,G_2,\ldots,G_n\}\theor H$ implique
$\{G_1,G_2,\ldots,G_{n-1}\}\theor  G_n\imp H$.
\end{itemize}
Conclusion : la propriété est vraie pour $p=1$.
\item Hypothèse de récurrence : Soit $p$ un entier tel que la propriété
soit vraie pour tous les entiers $i$ de 1 à $p$ (récurrence
généralisée); on suppose que la longueur de la déduction qui mène
à $H$ est $(p+1)$.
\begin{itemize}
\item Si $H$ est un axiome ou l'une des hypothèses, le cas se traite comme
ci-dessus.
\item Dans le cas contraire, $H$ ne peut avoir été obtenu que par un
\og modus ponens\fg{}  sur des formules $P$ et $P\imp H$. Ces formules
ont elles-mêmes été obtenues par des déductions de longueur
inférieure ou égale à $p$, donc on peut dire que

$\{G_1,G_2,\ldots,G_n\}\theor P$ implique
$\{G_1,G_2,\ldots,G_{n-1}\}\theor G_n\imp P$ et que

$\{G_1,G_2,\ldots,G_n\}\theor P\imp H$ implique
$\{G_1,G_2,\ldots,G_{n-1}\}\theor G_n\imp(P\imp H)$.

\sou{Démonstration sous les hypothèses} $\{G_1,G_2,\ldots,G_{n-1}\}$ :

\begin{tabular}{l l l}
  \x{1}  & $G_n\imp P$ 
  & Résultat intermédiaire 1 \\
  \x{2} & $G_n\imp(P\imp H)$ 
  & Résultat intermédiaire 2 \\
  \x{3} & $(G_n\imp P)\imp((G_n\imp(P\imp H))\imp(G_n\imp H))$ 
  & Axiome 2  \\
  \x{4} & $(G_n\imp(P\imp H))\imp(G_n\imp H)$
  & m.p. sur \x{1} et \x{3} \\
  \x{5} & $G_n\imp H$ 
  & m.p. sur \x{2} 4 \x{4}  \\
\end{tabular}\par
\sou{Conclusion} $\{G_1,G_2,\ldots,G_{n-1}\}\theor G_n\imp H$,\psaut et donc :
$\{G_1,G_2,\ldots,G_n\}\theor H$ implique
$\{G_1,G_2,\ldots,G_{n-1}\}\theor G_n\imp H$, lorsque la
déduction est de longueur $p+1$.
\end{itemize}
\end{itemize}
%Le résultat est établi.
\paragraph{Si.} Réciproquement, supposons $\{G_1,G_2,\ldots,G_{n-1}\}\theor 
(G_n\imp H)$. Alors, \psaut
\sou{Démonstration sous les hypothèses} $\{G_1,G_2,\ldots,G_n\}$\par
\begin{tabular}{l l l}
  \x{1}  & $G_n\imp H$ 
  & Résultat obtenu sous les hyp. $\{G_1,G_2,\ldots,G_{n-1}\}$\\
  \x{2} & $G_n$
  & Hypothèse $n$  \\
  \x{3} & H 
  & m.p. sur \x{2} et \x{1} \\
\end{tabular}\par
\sou{Conclusion} $\{G_1,G_2,\ldots,G_n\}\theor H$\psaut 
\psaut Donc : $\{G_1,G_2,\ldots,G_{n-1}\}\theor 
G_n\imp H$ entraîne $\{G_1,G_2,\ldots,G_n\}\theor H$.
\end{Proof}


%\subsubsection{Exemples d'utilisation du théorème de la déduction}

% \begin{Ex}
% Le \og modus tollens \fg{} $\{ P \imp Q, \non Q \} \theor \non P$
% \end{Ex}


\begin{Ex}
On cherche à  montrer  le \emph{théorème d'échange des prémisses}:
$$\theor (P\imp(Q\imp R))\imp(Q\imp(P\imp R))$$


La démonstration de ce théorème équivaut à la démonstration sous hypothèses
$$\{P\imp(Q\imp R)\}\theor(Q\imp(P\imp R)),$$
\noindent équivalente à la démonstration sous hypothèses
$$\{P\imp(Q\imp R),Q\}\theor(P\imp R),$$
elle-même équivalente à la démonstration sous hypothèses
$$\{P\imp(Q\imp R),Q,P\}\theor R$$
qui est obtenu comme suit:

\psaut
\sou{Démonstration sous les hypothèses} $\{P\imp(Q\imp R),Q,P\}$\par
\begin{tabular}{l l l}
  \x{1} & $P$ 
  & Hypothèse  \\
  \x{2} & $P\imp(Q\imp R)$
  & Hypothèse  \\
  \x{3} & $Q\imp R$ 
  & m.p. sur \x{1} et \x{2}  \\
  \x{4} & $Q$
  & Hypothèse  \\
  \x{5} & $R$
  & m.p. sur \x{4} et \x{3} \\
\end{tabular}\par
\sou{Conclusion} $\{P\imp(Q\imp R),Q,P\}\theor R$.\psaut

\end{Ex}

\begin{Rem}
 Cette méthode est beaucoup plus rapide que celle qui consisterait à
essayer de démontrer ce théorème à partir des axiomes et de la
règle d'inférence. 
\end{Rem}


% \begin{Ex}
% On a démontré la règle d'inférence du \og modus (tollendo) tollens\fg{}  :

% \hfil $\{P\imp Q,\non Q\}\theor\non P$.\hfil

% D'après le théorème de la déduction, ce dernier résultat est
% équivalent à :

% \hfil $\{P\imp Q\}\theor(\non Q\imp\non P)$.\hfil

% Une nouvelle application de ce même théorème donne :

% \hfil $\theor(P\imp Q)\imp(\non Q\imp\non P)$.\hfil
% \end{Ex}


\begin{Rem}
L'utilisation principale du théorème de la déduction consiste à remplacer la démonstration d'implication par des déductions sous hypothèses.
\end{Rem}


\section{Quelques théorèmes classiques et 
  quelques règles d'inférence annexes} 
Au théorème de réflexivité de l'implication 
($\theor\ P\imp P$) et au  théorème d'échange des prémisses 
($\theor (P\imp(Q\imp R))\imp(Q\imp(P\imp R))$) on 
ajoute ceux qui suivent.



\begin{Th}[Théorème de transitivité de l'implication]
Soit $P$ et $Q$ deux formules propositionnelles quelconques\index{théorème!de la transitivité 
de l'implication}.
$$\theor\ (P\imp Q)\imp((Q\imp R)\imp(P\imp R))$$
\end{Th}

\begin{Exo}
Effectuer la démonstration du théorème.
\end{Exo}

\begin{Def}[Contraposée]
L'implication $\non Q\imp\non P$ est appelée \emph{contraposée} \index{contraposée} de l'implication $P\imp Q$.
\end{Def}

\begin{Th}[Théorème de la contraposée]
Soit $P$ et $Q$ deux formules propositionnelles quelconques\index{théorème!de la contraposée}.
$$\theor(P\imp Q)\imp(\non Q\imp\non P)$$

\end{Th}

\begin{Exo}
Effectuer la démonstration du théorème.
\end{Exo}


% \begin{Proof}
% $\theor\ (P\imp Q)\imp((Q\imp R)\imp(P\imp R))$

% équivalent $ \{P\imp Q\} \theor (Q\imp R)\imp(P\imp R)$

% équivalent $ \{P\imp Q, Q\imp R \} \theor P\imp R$

% équivalent $ \{P\imp Q, Q\imp R, P \} \theor R$

% Cette déduction est évidente avec le modus ponens, avec :

% \begin{enumerate}
% \item $P \imp Q$ et $Q$,
% \item $Q \imp R$ et $Q$ obtenu en 1,
% \item on obtient $R$ en 2.
% \end{enumerate}
% \end{Proof}



\begin{Th}[Théorème de la contradiction]
\index{théorème!de la contradiction}
Soit $P$ et $Q$ deux formules propositionnelles quelconques\index{théorème!de la contradiction}. 
$$\theor \non P\imp(P\imp Q)$$
\end{Th}
Intuitivement, cela signifie que si $\non P$ et $P$ sont établies, 
alors on peut en déduire n'importe quoi ($Q$).


\begin{Exo}
Effectuer la démonstration.
\end{Exo}
% \sou{Démonstration sous les hypothèses} $\{P\vir\non P\}$\par
% \begin{tabular}{l l l}
% \x{1} & Hypothèse 1 & $P$ \\
% \x{2} & Axiome 1 & $P\imp(\non Q\imp P)$ \\
% \x{3} & m.p. sur \x{1},\x{2} & $\non Q\imp P$ \\
% \x{4} & Hypothèse 2 & $\non P$ \\
% \x{5} & Axiome 1 & $\non P\imp(\non Q\imp\non P)$ \\
% \x{6} & m.p. sur \x{4},\x{5} & $\non Q\imp\non P$ \\
%    \x{7} & Axiome 10 & $(\non Q\imp P)\imp((\non Q\imp \non P)\imp \non\non Q)$\cr
%    \x{8} & m.p. sur \x{4}, \x{7} & $(\non Q\imp \non P)\imp \non\non Q$ \cr
%    \x{9} & m.p. sur \x{6}, \x{8} & $\non\non Q$ \cr
%    \x{10} & Axiome 9 & $\non\non Q\imp Q$ \cr
%    \x{11} & m.p. sur \x{9}, \x{10} & $Q$ \cr
% \end{tabular}\par
% \sou{Conclusion} $\{P\vir\non P\}\theor Q$.\psaut



On introduit une règle permettant de s'abstraire de l'application de deux 
modus ponens sur l'axiome 8.
En effet, considérons l'axiome 8:
$$\theor (P\imp R)\imp((Q\imp R)\imp(P\ou Q\imp R))$$
En appliquant deux fois de suite le théorème de la déduction, il est équivalent à la déduction:
$$\{P\imp R\vir Q\imp R\}\ \theor\ P\ou Q\imp R$$
que l'on peut utiliser sous cette forme comme règle d'inférence annexe : elle s'appelle {\sl règle de disjonction des cas\/}.\psaut

\begin{Th}[Règle de disjonction des cas]
\index{règle!de disjonction des cas}
On a
$$\{P\imp R\vir Q\imp R\}\ \theor\ P\ou Q\imp R$$
\end{Th}


Pour finir, en appliquant deux fois de suite le théorème de la 
déduction à l'axiome 10:
$$\theor (P\imp Q)\imp((P\imp\non Q)\imp \non P)$$
il est équivalent à la déduction\par
$$\{P\imp Q\vir P\imp\non Q\}\theor\ \non P$$
que l'on peut utiliser sous cette forme comme règle
d'inférence annexe : elle s'appelle {\sl règle de réduction à
  l'absurde\/}.\psaut 

\begin{Th}[Règle de réduction à l'absurde]
\index{règle!de réduction à l'absurde}
On a
$$\{P\imp Q\vir P\imp\non Q\}\theor\ \non P$$
\end{Th}


% \begin{Exo}
% Démontrer les règles d'inférence suivantes :

% \begin{enumerate}
% \item \og modus tollendo ponens\fg{}: $\{\non P, P\ou Q\}\theor Q$  
% \item \og modus ponendo tollens \fg{}: $\{P, \non(P\et Q)\}\theor\non
%   Q$. 
% \end{enumerate}

% Pour la première, on pourra utiliser le théorème de la contradiction
% et, pour la seconde, le théorème de la contraposée.
% \end{Exo}




\begin{Exo}[Démonstrations avec ou sans hypothèses]
Démontrer les théorèmes logiques suivants (seuls les axiomes, règles
d'inférence, règles d'inférence annexes et théorèmes du cours sont
autorisés). 


\begin{enumerate}
%\item $\theor (P\imp Q)\imp((Q\imp R)\imp(P\imp R))$ 
%\item $\theor(P\imp(Q\imp R))\eqv(Q\imp(P\imp R))$
\item $\theor(P\imp(Q\imp R))\eqv(P\et Q\imp R)$
\item $\theor (P\imp Q)\eqv(\non Q\imp\non P)$
\item $\theor P\eqv\non\non P$ 
%\item $\theor (P\eqv Q)\et(Q\eqv R)\imp(P\eqv R)$
\item $\theor P\et (Q\ou R)\eqv(P\et Q)\ou(P\et R)$ 
\item $\theor P\ou(Q\et R)\eqv(P\ou Q)\et(P\ou R)$ 
%\item $\theor \non(P\et\non P)$
%\item $\theor \non(P\ou Q)\eqv\non P\et\non Q$
%\item $\theor \non(P\et Q)\eqv\non P\ou\non Q$ 
% \item $\theor P\ou Q\eqv\non(\non P\et\non Q)$
% \item $\theor P\et Q\eqv\non(\non P\ou\non Q)$ 
%\item $\theor (P\imp Q)\eqv\non P\ou Q$
%\item $\theor (P\imp Q)\eqv\non(P\et\non Q)$
%\item $\theor \non(P\imp Q)\eqv P\et\nonQ$

\item $\{P \lor R, P \imp Q, R \eqv S\} \theor Q \lor S$
\item $\{P \land \neg S, Q \lor  \neg R, S \imp R\} \theor 
  ( P \imp Q)  \lor (R \imp S)$
\end{enumerate}
\end{Exo}

% \section {Technique de l'hypothèse supplémentaire}

% \subsection{Introduction et suppression d'une hypothèse supplémentaire}

% Supposons qu'au cours d'une démonstration, il arrive que l'on ne 
% sache plus quoi écrire pour progresser en direction du résultat 
% recherché, mais que l'utilisation d'une hypothèse qui ne figure pas 
% dans l'ensemble déclaré au départ semble pouvoir débloquer la 
% situation.

% On admettra alors l'écriture d'une ligne contenant la déclaration de 
% cette hypothèse, appelons-la $H$, avec la justification \og Hypothèse 
% supplémentaire\fg{}. Cette hypothèse pourra alors être utilisée pour 
% progresser, et pour atteindre, quelques lignes plus loin, un certain 
% résultat, disons $R$.  La démonstration a alors l'allure suivante :\par

% \sou{Démonstration sous les hypothèses} $\{H_{1}\vir H_{2}\vir\ldots\vir
% H_{n}\}$

% \begin{tabular}{c c c}
% \x{1} & $\cdots$ & $\cdots$ \\
%  $\vdots$ & $\vdots$ & $\vdots$ \\
% \x{i} & Hypothèse supplémentaire & $H$ \\
% $\vdots$ & $\vdots$ & $\vdots$ \\
% \x{j} & $\cdots$ & $R$ \\
% \end{tabular}\par



% Dans une telle démonstration, le résultat obtenu est celui qui est écrit
% sur la dernière ligne écrite (même si ce n'est pas le résultat
% recherché!). 
% Autrement dit, si la démonstration s'arrêtait à cet endroit, le résultat
% obtenu serait $R$ mais, pour l'obtenir, une hypothèse non prévue au
% départ a été utilisée. Le véritable résultat obtenu est en fait

% \sou{Conclusion} $\{H_{1}\vir H_{2}\vir\ldots\vir H_{n}\vir H\}\theor 
% R$.

% %\noindent (en rajoutant $H$ à l'ensemble des hypothèses de départ).


% Mais on sait que ce résultat est équivalent à :

% \sou{Conclusion} $\{H_{1}\vir H_{2}\vir\ldots\vir H_{n}\}\theor H\imp
% R$.\psaut 

% \noindent R'est-à-dire un résultat établi en utilisant les seules
% hypothèses de départ. 


% On pourra donc rajouter une ligne contenant la justification : \og
% Suppression de l'hypothèse supplémentaire\fg{}  et comme résultat
% $H\imp R$ et, comme ce résultat est obtenu avec les seules hypothèses
% de départ, il est utilisable dans la suite (à la différence de ceux
% qui sont écrits dans les lignes $i$ à $j$ incluses). 


% \noindent On obtient
 
%  \sou{Démonstration sous les hypothèses} $\{H_{1}\vir H_{2}\vir\ldots\vir
%  H_{n}\}$

% \begin{tabular}{c c c}
% \x{1} & $\cdots$ & $\cdots$ \\
%  $\vdots$ & $\vdots$ & $\vdots$ \\
% \x{i} & Hypothèse supplémentaire & $H$ \\
% $\vdots$ & $\vdots$ & $\vdots$ \\
% \x{j} & $\cdots$ & $R$ \\
% \x{j+1} & Suppression hyp. suppl. $H$ & $H\imp R$ \\
%  $\vdots$ & $\vdots$ & $\vdots$ \\
% \end{tabular}

% On espère évidemment que ce dernier résultat a rendu le résultat
% recherché plus accessible.\psaut 

% Cependant, les lignes écrites dans le domaine de validité de
% l'hypothèse supplémentaire (de $i+1$ à $j$) ne peuvent pas être
% utilisées dans la suite de la démonstration. 



% Dans certains cas complexes, il est possible de faire successivement
% plusieurs hypothèses supplémentaires. 

% Il faut dans ce cas respecter la règle selon laquelle, lorsque
% plusieurs hypothèses supplémentaires coexistent, elles doivent être
% supprimées dans l'ordre inverse de leur introduction. 


% \subsection{Utilisation de cette technique dans une disjonction des cas}

% Lorsque le résultat à établir a la forme $\{P\ou Q\}\theor R$, o\`u $R$
% est une formule quelconque, le raisonnement \og par  disjonction des
% cas\fg{} prend la forme suivante, lorsque le résultat n'est pas
% immédiat. 



%  \sou{Démonstration sous l'hypothèse} $\{P\ou Q\}$

% \begin{tabular}{c c c}
% \x{1} & Hypothèse supplémentaire & $P$ \\
%  $\vdots$ & $\vdots$ & $\vdots$ \\
% \x{i} & $\cdots$ & $R$ \\
% \x{i+1} & Suppression hyp. suppl. $P$ & $P\imp R$ \\
% \x{i+2} & Hypothèse supplémentaire & $Q$ \\
%  $\vdots$ & $\vdots$ & $\vdots$ \\
% \x{j} & $\cdots$ & $R$ \\
% \x{j+1} & Suppression hyp. suppl. $Q$ & $Q\imp R$ \\
% \x{j+2} & Disjonction des cas sur \x{i+1},\x{j+1} & $P\ou Q\imp R$ \\
% \x{j+3} & Hypothèse & $P\ou Q$ \\
% \x{j+4} & m.p. sur \x{j+2}, \x{j+3} & $R$ \\
% \end{tabular}

% \sou{Conclusion} $\{P\ou Q\}\ \theor\ R$.


% \begin{Rem}
% Il faut veiller que ce soit bien le résultat final attendu qui soit
% obtenu avant la suppression des hypothèses supplémentaires. 
% \end{Rem}



% \section{Méthodes de démonstration}
% Il peut sembler {\sl a priori\/} difficile de trouver les idées qui
% permettent de mener à bien une démonstration sous hypothèses. 

% On pourra s'inspirer des principes suivants qui sont souvent d'une 
% aide précieuse bien qu'on ne puisse affirmer qu'ils fournissent dans 
% tous les cas la solution la plus courte, ni même ne suffisent 
% toujours pour trouver une solution.



% La première chose à faire est de faire intervenir au maximum le
% théorème de la déduction. 
% On conseille ensuite d'observer...
% \begin{description}
% \item[Les hypothèses.] Une hypothèse (ou un résultat intermédiaire)
%   qui se présente sous la forme d'une 
% \begin{description}
% \item[conjonction :] s'utilise par application des axiomes 4 et 5 
% \item[disjonction :] s'utilise par une disjonction des cas (voir
%   paragraphe précédent) 
% \item[négation :] s'utilise par application du théorème de la
%   contraposée  
% \item[implication logique :] souvent la technique de l'hypothèse
%   supplémentaire (utilisée aussi 
% dans le cas précédent) permet de l'utiliser. 
% \item[équivalence logique :] s'utilise par application des axiomes 12 et 13
% \end{description}

% L'application de ces quelques principes permet en général de bien
% démarrer les démonstrations, par leurs premières lignes. On observe
% ensuite... 

% \item[La conclusion.] Si elle se présente sous la forme d'une 
% \begin{description}
% \item[conjonction :] elle peut s'obtenir par application de l'axiome
%   3. 
% \item[disjonction :] elle peut s'obtenir par application de l'axiome 6
%   ou de l'axiome 7. 
% \item[négation :] elle peut s'obtenir par une réduction à l'absurde. 
% \item[implication :] vous n'avez pas suivi les conseils d'utiliser le
%   théorème de la déduction au maximum ! 
% \item[équivalence logique :] elle peut s'obtenir par application de
%   l'axiome 11 (concrètement, on effectue en général séparément les
%   démonstrations des deux implications et on peut s'abstenir de \og
%   reconstruire\fg{}  l'équivalence logique à partir des deux
%   implications, de l'axiome 11 et de deux \og modus ponens\fg{}). 
% \end{description}
% L'application de ces quelques principes permet en général de découvrir
% un bon chemin vers le résultat, c'est-à-dire les dernières lignes de
% la démonstration. 
% \end{description}

% Au total, sauf dans des cas très compliqués, on devrait avoir ainsi
% l'intégralité de la démonstration. 

% \section{Exercices}


% \begin{Exo}[Validité de raisonnements] Formaliser, puis étudier la
%   validité des raisonnements suivants : 

% \begin{enumerate}

% \item Un étudiant ne peut résoudre un exercice si on ne lui dit pas
%   comment faire. On  ne lui dit pas comment faire s'il ne pose pas de
%   questions. Il a trouvé, donc  il a  posé des questions. 

% \item Ce qui est compréhensible ne m'intrigue jamais; la logique
%   m'intrigue. Donc, la logique est incompréhensible. 

% \item Aucun professeur n'est ignorant; les gens ignorants sont
%   ennuyeux. Donc, 
% aucun professeur n'est ennuyeux.

% \item Tout professeur de mathématiques est logique; un homme illogique
%   est 
% toujours têtu. Donc, aucun professeur de mathématiques n'est têtu. 

% \item Un parapluie est utile en voyage; toute chose inutile en voyage
%   doit être 
% laissée à la maison. Il faut donc emporter son parapluie en voyage.

% \item Aucun problème ne m'intéresse s'il est possible de le résoudre;
%   tous ces 
% problèmes m'intéressent. Ils sont donc impossibles à résoudre.

% \end{enumerate}
% \end{Exo}





% \begin{Exo}
% \'Etude de raisonnements concrets :

% \begin{enumerate}

% \item Peut-on conclure quelque chose au sujet de la réussite de
%   l'attaque envisagée dans les conditions suivantes? 

% \og
% L'attaque réussira seulement si l'ennemi est surpris ou si la position
% est peu défendue. L'ennemi ne sera pas surpris, à moins qu'il ne soit
% téméraire. L'ennemi n'est pas téméraire 
% lorsque la position est peu défendue.
% \fg{}

% \item Peut-on conclure quelque chose au sujet de la culpabilité du
%   suspect décrit dans les propositions suivantes? 

% \og
% Si le suspect a commis le vol, celui-ci a été minutieusement préparé
% ou le suspect disposait d'un complice dans la place. Si le vol a été
% minutieusement préparé, alors, si le suspect avait un complice dans la
% place, le butin aurait été beaucoup plus important. 
% \fg{}

% \item La conclusion du raisonnement suivant est-elle valide? 

% \og
% \`P moins que nous ne continuions la politique de soutien des prix,
% nous perdrons les voix des agriculteurs. Si nous continuons cette
% politique, la surproduction se poursuivra, sauf si nous contingentons
% la production. Sans les voix des agriculteurs, nous ne serons pas
% réélus. Donc, si nous sommes réélus et que nous ne contingentons pas
% la production, la surproduction continuera. 
% \fg{}

% \item Quelles sont les conclusions que l'on peut tirer des
%   renseignements suivants: 

% \og
% J'aime les tomates à la provençale, ou je suis né un 29 février, ou je
% sais jouer du cornet à pistons. Si je sais jouer du cornet à pistons,
% alors je suis né un 29 février ou j'aime les tomates à la
% provençale. Si je n'aime pas les tomates à la provençale et si je suis
% né un 29 février, alors je ne sais pas jouer du cornet à pistons. Je
% n'aime pas les tomates à la provençale ou je ne sais pas jouer du
% conet à pistons. 
% \fg{}
% \end{enumerate} 
% \end{Exo}


% \begin{Exo}[Un problème de logique]
% Trois artisans coiffeurs (Aristide, Barnabé et Clotaire) tiennent un
% salon de coiffure. Celui-ci ne peut rester sans surveillance pendant
% les heures d'ouverture, donc l'un au moins des trois artisans est
% obligatoirement présent. On sait, de plus, qu'Aristide ne peut sortir
% seul; lorsqu'il s'absente, il se fait obligatoirement accompagner par
% Barnabé.

% Oncle Jim et oncle Joe, deux sympathiques logiciens, se dirigent vers
% le salon, en échangeant les propos suivants:\psaut 

% -- J'espère bien que Clotaire est là. Barnabé est très maladroit, et
% la main d'Aristide tremble constamment depuis qu'il a eu cet accès de
% fièvre qui le handicape, dit oncle Jim. 

% -- Clotaire est sûrement là, affirme oncle Joe.

% -- Qu'en sais-tu\,? Je te parie cent sous que non, reprend oncle Jim.

% -- Je peux te le prouver logiquement, rétorque oncle Joe, qui poursuit
% : Prenons comme hypothèse de travail que Clotaire est {\sl absent\/},
% et voyons ce qu'il résulte de cette supposition. Pour cela, je vais
% utiliser le principe de {\sl réduction à l'absurde\/}. 

% -- Je m'en doutais, grommelle oncle Jim. Je ne t'ai encore jamais
% entendu discuter quelque chose sans que cela se termine par quelque
% absurdité\,! 

% -- Sans me laisser démonter par tes propos venimeux, dit noblement
% oncle Joe, je continue; Clotaire étant absent, tu m'accordes que, si
% Aristide est également absent, Barnabé est obligatoirement présent ? 

% -- \'Evidemment, dit oncle Jim en haussant les épaules, sinon il n'y
% aurait plus personne pour garder le salon. 

% -- Nous voyons par conséquent que l'absence de Clotaire fait
% intervenir une implication logique, \og {\it si Aristide est absent,
%   Barnabé est présent\/} \fg{}, et que cette implication reste vraie
% tant que Clotaire est absent. 

% -- Admettons, fait Oncle Jim, et après ?

% -- Il nous faut à présent tenir compte d'une autre hypothétique, que
% je formule par \og {\it Si Aristide est absent, alors Barnabé est
%   absent\/} \fg{}, laquelle est {\tt toujours\/} vraie, indépendamment
% de la présence de Clotaire, n'est-ce pas\,? 

% --  Sans doute, dit oncle Jim, qui semble gagné par l'inquiétude, je
% confirme qu'Aristide, s'il s'absente, se fait obligatoirement
% accompagner par Barnabé. 

% -- Nous somme donc placés en présence de deux implications. La
% première est vraie tant que Clotaire est absent. La seconde, qui est
% toujours vraie, l'est en particulier lorsque Clotaire est absent. Or
% ces deux implications me paraissent parfaitement incompatibles. Donc,
% par une très belle réduction à l'absurde, je conclus qu'il est
% impossible que Clotaire soit absent, tu vas donc le voir tout de
% suite. 

% -- Il y a quand même quelque chose qui me paraît douteux, dans ton \og
% {\it incompatibilité\/} \fg{}, dit oncle Jim, qui semble totalement
% décontenancé. Il réfléchit, puis reprend : Pourquoi, en effet,
% seraient-elles contradictoires\,? Tu ne prouves en fait qu'une seule
% chose : c'est que c'est Aristide qui est présent\,! 

% -- Très cher et très illogique frère, fait oncle Joe, ne vois-tu pas
% que tu es en train de décomposer une implication logique en prémisse
% et conclusion\,? Qui te permet d'affirmer que l'implication \og {\it
%   si Aristide est absent, Barnabé est présent\/} \fg{} est vraie\,?
% N'as-tu jamais appris que, de la valeur de vérité d'une implication,
% on ne peut rien déduire sur celles de ses éléments\,? 
% \psaut

% \`P l'aide des variables propositionnelles $P$ (pour : \og Aristide
% est présent \fg{}), $Q$ (pour: \og Barnabé 
% est présent \fg{}) et $R$ (pour: \og Clotaire est présent \fg{}),
% formaliser les raisonnements d'oncle Joe (dont la conclusion est $R$)
% et d'oncle Jim (dont la conclusion est $P$). Qui a raison et qui a
% tort ?  
% \end{Exo}




\section{Théorèmes de complétude du calcul propositionnel}

On a jusqu'à maintenant deux points de vue :

\begin{enumerate}
\item La théorie des valeurs de vérité, avec ses
\begin{itemize}
\item tables de vérités,
\item fonctions de vérités,
\item tautologie, conséquence, hypothèse.
\end{itemize}
\item La théorie de la démonstration, avec ses
\begin{itemize}
\item axiomes,
\item règles d'inférence,
\item démonstrations (ou démonstrations sous hypothèses).
\end{itemize} 
\end{enumerate}

On peut se demander si les résultats obtenus dans chacune des deux
théories sont identiques:
une formule propositionnelle est-elle démontrable si et seulement 
si elle est une tautologie?


Un sens est immédiat, c'est le \og seulement si\fg{}:
toute proposition démontrée résulte d'un axiome ou 
de l'application d'une règle sur des propositions déjà démontrées.
On peut facilement de vérifier que les axiomes fournissent 
des tautologies et que les règles conservent les tautologies. 
Toute proposition démontrée est donc une tautologie. 
On dit que le système déductif PR est \emph{correct}.
L'autre sens la démonstration  qui consiste à vérifier que toute tautologie 
admet une démonstration dans PR est un peu plus complexe et admise.
Pour ce sens on dit que PR est \emph{complet}. 

On retiendra les théorèmes suivants 
(abusivement nommés théorèmes de complétude).

% Le théorème de complétude du calcul des propositions énonce que le système de déduction PR est complet

% \subsection{Théorème de complétude}
% %\subsubsection{Théorème}

% Le théorème de complétude du calcul propositionnel s'énonce ainsi :


\begin{Th}[Théorème de complétude]
 \index{théorème!de complétude}
tout théorème est une tautologie et réciproquement, soit :
$$\theor F  \textrm{ si et seulement si } \tauto F$$.
\end{Th}

% Autrement dit, les deux points de vue (théorie des valeurs de vérité,
% théorie de la démonstration) sont équivalents pour les théorèmes et
% les tautologies.

% \begin{Proof} 
% $ $ 

% \paragraph{Seulement si.} 
% Hypothèse : $\theor F$ (c'est-à-dire : $F$ est un théorème). La
% démonstration utilise les résultats suivants :

% \begin{itemize}
% \item Tous les axiomes du calcul propositionnel sont des tautologies
%   (simple 
% calcul sur leurs fonctions de vérité, qui ne sera pas développé ici). 
% \item Le modus ponens est valide: $\{P,P\imp Q\}\tauto Q$.
% \end{itemize}

% Il résulte de ces considérations que, lorsqu'on effectue une 
% démonstration, cette
% démonstration utilise des axiomes, qui sont des tautologies,
% c'est-à-dire des formules propositionnelles \og toujours vraies\fg{}, et
% en déduit d'autres formules propositionnelles; d'après la validité du
% \og modus ponens\fg{}, les formules propositionnelles qui ont été
% déduites sont \og vraies\fg{} chaque fois que les formules d'origine le
% sont aussi; or, ces dernières le sont toujours, donc les formules
% déduites le sont aussi toujours; autrement dit, les formules déduites
% en théorie de la démonstration sont des tautologies.  
% Conclusion : $\tauto F$.

% \paragraph{Si.} Hypothèse : $\tauto F$ (c'est-à-dire : $F$ est une
% tautologie) :  Plus compliqué : il faut exhiber une démonstration
% d'une tautologie. La démonstration se fait en trois étapes : 

% \begin{itemize}

% \item étape 1 : On montre que, si $\tauto F$, alors $\{P_1\ou\non P_1,
% P_2\ou\non P_2,\ldots,P_n\ou\non P_n\}\theor F$ [Dans cette expression,
% $P_1,P_2,\ldots,P_n$ sont les variables propositionnelles qui interviennent
% dans l'expression de $F$, à l'exclusion de toute autre].

% \item étape 2 : On montre que $\theor P\ou\non P$.

% \item étape 3 : On montre que, si, $\forall i\in\{1,2,...,p\},\
% \Gamma\theor Q_i$ et si $\{Q_1,Q_2,\ldots,Q_p\}\theor R$ , alors 
% $\Gamma\theor R$ ou transitivité de la déductibilité [$\Gamma$ est un ensemble, éventuellement vide,
% d'hypothèses].

% \item Conclusion : L'étape 3, appliquée à $\theor P_1\ou\non P_1,
% \theor P_2\ou\non P_2,\ldots,\theor P_n\ou\non P_n$ [l'ensemble
% d'hypothèses $\Gamma$ est ici vide] permet d'obtenir : $\theor F$.

% \end{itemize}

% Voici le détail de la démonstration des trois étapes :

% \begin{itemize}

% \item étape 1 : Toute ligne d'une table de vérité concernant une formule
% propositionnelle peut être interprétée comme introduisant une \og règle
% de déductibilité\fg{}. Exemple : la ligne
% \begin{tabular}{|c|c|c|} \hline
% $P$ & $Q$ & $P\ou Q$ \\ \hline
% V & F & V \\ \hline
% \end{tabular}  de la table de vérité de la disjonction logique peut être interprétée comme
% représentant une déduction : $\{P,\non Q\}\theor(P\ou Q)$. Cette \og règle de
% déductibilité\fg{}  résulte immédiatement des considérations suivantes :\psaut
% \sou{Démonstration sous les hypothèses} $\{P\vir\non Q\}$\par
% \begin{tabular}{l l l}
% \x{1} & Hypothèse 1 & $P$ \\
% \x{2} & Axiome 6 & $P\imp P\ou Q$ \\
% \x{3} & m.p. sur \x{2},\x{3} & $P\ou Q$ \\
% \end{tabular}\par
% \sou{Conclusion} $(P,\non Q)\theor P\ou Q$.\psaut
% [remarque : l'hypothèse $\non Q$ ne
% sert en fait pas, mais peu importe]. Il suffit alors d'établir ces
% \og règles de déductibilité\fg{}  pour toutes les lignes des tables de
% vérité des connecteurs logique (ce qui est un peu long -il y en a 18 - mais ne
% présente pas de véritable caractère de difficulté, elles sont
% proposées en TD); comme la 
% table de vérité de $F$  est obtenue à partir de celles des connecteurs
% logiques, chacune de ses lignes 
% peut aussi être considérée comme une règle de déductibilité; comme $F$
% est une tautologie, 
% sa dernière colonne est uniquement composée de \og V\fg{}, autrement dit, les
% règles de déductibilité qui la concernent pourront s'écrire : 

% \begin{tabular}{c c c c c c c c c c c c c}
% \{ & $\non P_1$ & , & $\non P_2$ & , & $\ldots$ & , & $\non P_{n-1}$ & , &
% $\non P_n$ & \} & $\theor$ & $F$ \\
% \{ & $\non P_1$ & , & $\non P_2$ & , & $\ldots$ & , & $\non P_{n-1}$ & , &
% $P_n$ & \} & $\theor$ & $F$ \\

% \dotfill & \dotfill & \dotfill & \dotfill & \dotfill & \dotfill & \dotfill &
% \dotfill & \dotfill & \dotfill & \dotfill & \dotfill & \dotfill \\
% \{ & $P_1$ & , & $P_2$ & , & $\ldots$ & , & $P_{n-1}$ & , &
% $\non P_n$ & \} & $\theor$ & $F$ \\
% \{ & $P_1$ & , & $P_2$ & , & $\ldots$ & , & $P_{n-1}$ & , &
% $P_n$ & \} & $\theor$ & $F$ \\
% \end{tabular}

% [Le tableau comporte $2^n$  lignes]. Il ne reste plus qu'à établir
% que, si 
% $\Gamma$ est un ensemble quelconque de formules propositionnelles, et si on a
% $\Gamma\union\{P\}\theor R$ et $\Gamma\union\{Q\}\theor R$, alors on a
% $\Gamma\union\{P\ou 
% Q\}\theor R$, ce qui se fait de la manière suivante (il s'agit en fait
% d'une disjonction des 
% cas) :

% \begin{itemize}

% \item $\Gamma\union\{P\}\theor R$ est équivalent à $\Gamma\theor
% P\imp R$ [d'après le théorème de la déduction].

% \item $\Gamma\union\{ Q\}\theor R$ est équivalent à
% $\Gamma\theor Q\imp R$ [d'après le théorème de la déduction].

% \end{itemize}

% Donc, dans une\psaut

% \sou{Démonstration sous les hypothèses} $\Gamma$ :\par
% \begin{tabular}{l l l}
% \x{1} & Résultat intermédiaire 1 & $P\imp R$ \\
% \x{2} & Résultat intermédiaire 2 & $Q\imp R$ \\
% \x{3} & Axiome 8 & $(P\imp R)\imp ((Q\imp R)\imp(P\ou Q\imp R))$ \\
% \x{4} & m.p. sur \x{1},\x{3} & $(Q\imp R)\imp(P\ou Q\imp R)$ \\
% \x{5} & m.p. sur \x{2},\x{4} & $P\ou Q\imp R$ \\
% \end{tabular}\par
% \sou{Conclusion} $\Gamma\theor P\ou Q\imp R$\psaut
% Donc, si on suppose $\Gamma\union\{P\}\theor R$ et
% $\Gamma\union\{Q\}\theor R$, il existe 
% une démonstration sous les hypothèses $\Gamma$ dont la conclusion est
% $P\ou 
% Q\imp R$. R'est à dire : $\Gamma\theor P\ou Q\imp R$. D'après le
% théorème de la déduction, ce dernier résultat est équivalent à :
% $\Gamma\union\{P\ou Q\}\theor R$. R'est la conclusion qui était
% recherchée. 

% Ce résultat est à présent appliqué $n$ fois de suite aux $2^n$
% \og règles de déductibilité\fg{}, que l'on prend deux par deux, pour obtenir
% enfin : $\{P_1\ou\non P_1,P_2\ou\non P_2,\ldots,P_n\ou\non P_n\}\theor F$.

% \item étape 2 : Il faut montrer que : $\theor P\ou\non P$ ({\sl
%     théorème du tiers-exclu}).\psaut 

% \sou{Démonstration} :\par
% \begin{tabular}{l l l}
% \x{1} & Axiome 6 & $P\imp P\ou\non P$ \\
% \x{2} & Th. de la contrap. & $(P\imp P\ou\non
% P)\imp(\non(P\ou\non P)\imp\non P)$ \\
% \x{3} & m.p. sur \x{1},\x{2} & $\non(P\ou\non P)\imp\non P$ \\
% \x{4} & Axiome 7 & $\non P\imp P\ou\non P$ \\
% \x{5} & Th. de la contrap. & $(\non P\imp P\ou\non
% P)\imp(\non(P\ou\non P)\imp\non\non P)$ \\
% \x{6} & m.p. sur \x{4},\x{5} & $\non(P\ou\non P)\imp\non\non P$ \\
% \x{7} & Axiome 10 & $(\non(P\ou\non P)\imp\non P)\imp((\non(P\ou\non
% P)\imp\non\non P)\imp\non\non(P\ou\non P))$ \\
% \x{8} & m.p. sur \x{3},\x{7} & $(\non(P\ou\non P)\imp\non\non
% P)\imp\non\non(P\ou\non P)$ \\
% \x{9} & m.p. sur \x{6},\x{8} & $\non\non(P\ou\non P)$ \\
% \x{10} & Axiome 9 & $\non\non(P\ou\non P)\imp P\ou\non P$ \\
% \x{11} & m.p. sur \x{9},\x{10} & $P\ou\non P$ \\
% \end{tabular}\par
% \sou{Conclusion} : $\theor P\ou\non P$.

% \item étape 3 : Il faut montrer que, si, $\forall i\in\{1,2,...,p\}$, 
% $\Gamma\theor Q_i$ et si $\{Q_1,Q_2,\ldots,Q_p\}\theor R$, alors
% $\Gamma\theor R$.
% Pour cela, il suffit de remarquer qu'une \og conclusion
% partielle\fg{}, c'est à 
% dire une formule obtenue au cours d'une démonstration, est d\^ument établie,
% et peut donc servir pour des inférences dans la suite (cette remarque a
% déjà été utilisée dans plusieurs des démonstrations de ce cours).
% Ainsi, il suffit de regrouper au sein d'une même démonstration (sous les
% hypothèses de $\Gamma$), les démonstrations qui mènent aux $Q_i$ (pour
% $1\infeg i\infeg p$). Ceux-ci seront considérés, dans la suite, comme
% \og conclusions partielles\fg{}  ou \og résultats
% intermédiaires\fg{}. Et ils seront 
% donc réutilisés en tant que tels dans la suite de la démonstration, qui
% consistera à recopier la démonstration de $R$ (sous les hypothèses $Q_i$).
% Dans cette démonstration, les références aux $Q_i$, en tant
% qu'hypothèses, seront remplacées par les références aux lignes qui
% précèdent dans lesquelles les $Q_i$ ont été obtenus comme
% \og conclusions partielles\fg{}. Cette nouvelle démonstration sera bien une
% démonstration de $R$ sous les hypothèses de $\Gamma$.
% \end{itemize}
% \end{Proof}



% \subsection{Théorème de complétude généralisé}

% Le résultat énoncé dans le théorème de complétude au sujet des 
% théorèmes (donc des démonstrations sans hypothèses) et des tautologies 
% est étendu aux démonstrations sous hypothèses et aux conséquences 
% logiques; c'est-à-dire :

\begin{Th}[Théorème de complétude généralisé]
On a
$$\{P_1,P_2,\ldots,P_n\}\theor Q \textrm{ si et seulement si }
\{P_1,P_2,\ldots,P_n\}\tauto Q$$
\end{Th}


% La démonstration de ce théorème est obtenue aisément en appliquant,
% pour la partie \og théorie de la démonstration\fg{}, le théorème de la déduction, et, pour la partie \og théorie des valeurs de vérité\fg{}, le théorème de validité. Il ne reste plus alors qu'à appliquer le théorème de complétude.

% Ainsi, $\{P_1,P_2,\ldots,P_n\}\theor Q$ est remplacé par 
% $\theor(P_1\imp (P_2\imp \ldots (P_n\imp Q)\ldots))$

% et $\{P_1,P_2,\ldots,P_n\}\tauto Q$ est remplacé par 
% $\tauto(P_1\imp (P_2\imp\ldots(P_n\imp Q)\ldots))$.



\gsaut
\centerline{\x{Fin du Chapitre}}