diapos/logique/.svn/text-base/deduc.tex.svn-base

   1 \begin{frame}
   2  \frametitle{Déductions et démonstrations}
   3  \framesubtitle{Conséquence logique}
   4 \begin{itemize}
   5 \item Principe de causalité
   6 \item Relation binaire ``\ldots a pour conséquence logique \ldots''
   7 \item \pause ``$F$ a pour conséquence logique $G$'' est noté $F
   8 \vdash G$
   9 \item \pause On veut axiomatiser cette relation par des
  10 ``règles de déduction''
  11 \item \pause Extension à $n$ ``hypothèses'' $H_1, \ldots, H_n$
  12 \item $H_1, \ldots, H_n \vdash C$
  13 \end{itemize}
  14 \end{frame}
  15
  16 \begin{frame}
  17  \frametitle{Déductions et démonstrations}
  18  \framesubtitle{Démonstration d'un théorème}
  19 \begin{itemize}
  20 \item Une démonstration est une suite de déductions correctes
  21 \item Chaque déduction respecte une règle donnée
  22 \item \pause A partir d'axiomes (formules admises)
  23 \item \pause Produit des formules à partir d'autres formules
  24 \item La dernière formule de la suite est le théorème ainsi
  25 démontré
  26 \end{itemize}
  27 \end{frame}
  28
  29
  30 \begin{frame}
  31  \frametitle{Exemple de système déductif propositionnel}
  32  \framesubtitle{Variante du système de Hilbert et Ackermann}
  33 \begin{itemize}
  34 \item 13 axiomes (voir support de cours)
  35 \item \pause Une règle de déduction (d'inférence) : Modus Ponens
  36
  37 $$\{ P, P \Rightarrow Q \} \vdash Q$$
  38
  39 \pause aussi notée
  40 $$\frac{P, P \Rightarrow Q}{Q}$$
  41 \item \pause
  42 Ajouter la règle de substitution
  43 \begin{itemize}
  44   \item Voir le théorème de substitution
  45   \item Sera reprise dans le cours sur les substitutions
  46 \end{itemize}
  47 \end{itemize}
  48 \end{frame}
  49
  50 \begin{frame}
  51  \frametitle{Déductions et démonstrations}
  52  \framesubtitle{Support de cours et compléments}
  53 \begin{itemize}
  54 \item Chapitre 6
  55 \item Notation simplifiée, pour les théorèmes sous hypothèses
  56
  57 \pause
  58 \begin{center}
  59 $H_1, \ldots, H_n \vdash C$ au lieu de $\{H_1, \ldots, H_n\} \vdash C$
  60 \end{center}
  61 \item
  62  \pause Partie IV essentielle
  63 \end{itemize}
  64
  65 \pause Compléments
  66
  67 \begin{itemize}
  68   \item Notation des déductions plus visuelle
  69
  70        $$\frac{H_1, \ldots, H_n}{C}$$
  71
  72   \item \pause Deux autres systèmes formels
  73   \begin{itemize}
  74    \item  \pause Résolution propositionnelle (efficacement
  75    automatisable)
  76    \item \pause Déduction naturelle (imite le raisonnement humain,
  77    pas d'axiomes)
  78   \end{itemize}
  79 \end{itemize}
  80 \end{frame}
  81
  82 \begin{frame}
  83  \frametitle{Déductions et démonstrations}
  84  \framesubtitle{Méta-théorème de la déduction}
  85  \begin{center}
  86  $H \vdash C$ est un th\'eor\`eme si et seulement si $H \Rightarrow
  87  C$ est un th\'eor\`eme
  88  \end{center}
  89 \begin{itemize}
  90 \item \pause Relie formules (dans la logique) et déductions (à propos de la
  91 logique)
  92 \item \pause Attention : ce n'est pas le théorème d'une logique
  93 propositionnelle
  94 \pause mais un théorème \emph{au sujet de} toutes ces logiques
  95 \item \pause C'est un théorème de la ``théorie de la démonstration''
  96 \end{itemize}
  97 \end{frame}
  98
  99 \begin{frame}
 100 \frametitle{Déductions et démonstrations}
 101 \framesubtitle{Correction et complétude}
 102 On veut qu'un système déductif (un système formel, un calcul, une
 103  logique) propositionnel (propositionnelle) soit \emph{correct} et
 104  \emph{complet} par rapport à l'interprétation booléenne
 105 \begin{itemize}
 106 \item \pause Correct : toutes les théorèmes sont des tautologies
 107 \pause
 108  \begin{center}
 109  Si $\vdash F$ alors $\models F$
 110  \end{center}
 111 \item On ne déduit que du ``vrai'', rien de faux
 112 \item \pause Complet : toutes les tautologies sont des théorèmes
 113
 114 \pause
 115
 116  \begin{center}
 117  Si $\models F$ alors $\vdash F$
 118  \end{center}
 119 \item On déduit tout ce qui est ``vrai''
 120 \item \pause ``PR'', la résolution propositionnelle et la déduction
 121 naturelle sont trois systèmes corrects et complets
 122 \end{itemize}
 123 \end{frame}