\begin{frame}
 \frametitle{Déductions et démonstrations}
 \framesubtitle{Conséquence logique}
\begin{itemize}
\item Principe de causalité
\item Relation binaire ``\ldots a pour conséquence logique \ldots''
\item \pause ``$F$ a pour conséquence logique $G$'' est noté $F
\vdash G$
\item \pause On veut axiomatiser cette relation par des
``règles de déduction''
\item \pause Extension à $n$ ``hypothèses'' $H_1, \ldots, H_n$
\item $H_1, \ldots, H_n \vdash C$
\end{itemize} 
\end{frame}

\begin{frame}
 \frametitle{Déductions et démonstrations}
 \framesubtitle{Démonstration d'un théorème}
\begin{itemize}
\item Une démonstration est une suite de déductions correctes
\item Chaque déduction respecte une règle donnée
\item \pause A partir d'axiomes (formules admises)
\item \pause Produit des formules à partir d'autres formules
\item La dernière formule de la suite est le théorème ainsi
démontré
\end{itemize} 
\end{frame}


\begin{frame}
 \frametitle{Exemple de système déductif propositionnel}
 \framesubtitle{Variante du système de Hilbert et Ackermann}
\begin{itemize}
\item 13 axiomes (voir support de cours)
\item \pause Une règle de déduction (d'inférence) : Modus Ponens

$$\{ P, P \Rightarrow Q \} \vdash Q$$

\pause aussi notée
$$\frac{P, P \Rightarrow Q}{Q}$$
\item \pause 
Ajouter la règle de substitution
\begin{itemize}
  \item Voir le théorème de substitution
  \item Sera reprise dans le cours sur les substitutions 
\end{itemize}  
\end{itemize} 
\end{frame}

\begin{frame}
 \frametitle{Déductions et démonstrations}
 \framesubtitle{Support de cours et compléments}
\begin{itemize}
\item Chapitre 6
\item Notation simplifiée, pour les théorèmes sous hypothèses

\pause
\begin{center}
$H_1, \ldots, H_n \vdash C$ au lieu de $\{H_1, \ldots, H_n\} \vdash C$
\end{center}
\item 
 \pause Partie IV essentielle
\end{itemize}
 
\pause Compléments

\begin{itemize}
  \item Notation des déductions plus visuelle 

       $$\frac{H_1, \ldots, H_n}{C}$$

  \item \pause Deux autres systèmes formels 
  \begin{itemize}
   \item  \pause Résolution propositionnelle (efficacement
   automatisable)
   \item \pause Déduction naturelle (imite le raisonnement humain,
   pas d'axiomes)
  \end{itemize}
\end{itemize}
\end{frame} 

\begin{frame}
 \frametitle{Déductions et démonstrations}
 \framesubtitle{Méta-théorème de la déduction}
 \begin{center}
 $H \vdash C$ est un th\'eor\`eme si et seulement si $H \Rightarrow
 C$ est un th\'eor\`eme
 \end{center}
\begin{itemize}
\item \pause Relie formules (dans la logique) et déductions (à propos de la
logique)
\item \pause Attention : ce n'est pas le théorème d'une logique
propositionnelle 
\pause mais un théorème \emph{au sujet de} toutes ces logiques
\item \pause C'est un théorème de la ``théorie de la démonstration'' 
\end{itemize}
\end{frame} 

\begin{frame}
\frametitle{Déductions et démonstrations}
\framesubtitle{Correction et complétude}
On veut qu'un système déductif (un système formel, un calcul, une
 logique) propositionnel (propositionnelle) soit \emph{correct} et
 \emph{complet} par rapport à l'interprétation booléenne
\begin{itemize}
\item \pause Correct : toutes les théorèmes sont des tautologies 
\pause 
 \begin{center}
 Si $\vdash F$ alors $\models F$
 \end{center}
\item On ne déduit que du ``vrai'', rien de faux
\item \pause Complet : toutes les tautologies sont des théorèmes

\pause 

 \begin{center}
 Si $\models F$ alors $\vdash F$
 \end{center}
\item On déduit tout ce qui est ``vrai''
\item \pause ``PR'', la résolution propositionnelle et la déduction
naturelle sont trois systèmes corrects et complets
\end{itemize}
\end{frame}