logique/BethTab.tex

   1 % AG. Sur ce sujet voir GochetGribomont et [Fitting90].
   2
   3 \subsection{Tableaux de Beth}
   4 Il s'agit d'une autre méthode de démonstration formelle, ignorant
   5 tout système d'axiomes, mais comportant de nombreuses règles
   6 d'inférence, également appelée méthode des tableaux sémantiques.
   7
   8 Elle est particulièrement adaptée à l'automatisation des
   9 démonstrations, et constitue une ouverture sur les algorithmes
  10 étudiés en seconde année (utilisation systématique du \og théorème de
  11 falsification\fg{}  qui sera envisagé plus loin).\psaut
  12
  13 \subsubsection{Principe de la méthode}
  14
  15 Il s'agit de montrer qu'une formule $F$ est un théorème( $\theor F$);
  16 le résultat est obtenu en montrant que la \og réfutation\fg{}  de $F$
  17 conduit à une contradiction.
  18
  19 La \og réfutation\fg{}  se conduit dans un arbre (appelé tableau de
  20 Beth (logicien néerlandais). \og Réfuter\fg{}  $F$, c'est le \og
  21 nier\fg{}, selon sa forme, en suivant les règles d'inférences qui
  22 sont données dans le tableau :\gsaut
  23
  24 % \centerline{\begin{tabular}{|c|c|}
  25 % \noalign{\hrule}
  26 % Règles d'affirmation & Règles de réfutation
  27 % \noalign{\hrule} \\
  28 % $\begin{array}{c}\tvii{15}\non A \cr\sur A \cr \end{array}$
  29 % &
  30 % $\begin{array}{c} \tvii{15}\sur{\non A} \cr A \cr \end{array}$
  31 % \noalign{\hrule}\\
  32 % $\begin{array}{c} \tvii{15}A\ou B \cr \swarrow\searrow \cr A\qquad B\cr \end{array}$
  33 % &
  34 % $\begin{array}{c} \tvii{15}\sur{A\ou B} \cr \sur A \cr \sur B \cr \end{array}$
  35 % \noalign{\hrule}\\
  36 % $\begin{array}{c} \tvii{15}A\et B \cr A \cr B \cr \end{array}$
  37 % &
  38 % $\begin{array}{c} \tvii{15}\sur{A\et B} \cr \swarrow\searrow \cr \sur A\qquad\sur B \cr
  39 % \end{array}$
  40 % \noalign{\hrule}\\
  41 % $\begin{array}{c} \tvii{15}A\imp B \cr \swarrow\searrow \cr \sur A\qquad B\cr \end{array}$
  42 % &
  43 % $\begin{array}{c} \tvii{15}\sur{A\imp B} \cr A \cr \sur B
  44 %   \cr \end{array}$
  45 % \noalign{\hrule}
  46 % \end{tabular}}
  47
  48
  49
  50 La règle de contradiction est
  51 \begin{tabular}{|c|}\noalign{\hrule}$A$\\$\sur A$\\$\clv$\\
  52 \noalign{\hrule}\end{tabular}\ .\gsaut
  53
  54
  55 \'Ecrire, dans un tableau de Beth, $A$ signifie \og j'affirme
  56 $A$\fg{}  et $\sur A$ signifie \og je nie $A$\fg{}  (ne pas confondre
  57 avec $\non A$).
  58
  59
  60 Une branche d'un tableau de Beth est considérée comme terminée
  61 lorsque plus aucune règle ne peut s'appliquer et elle est considérée
  62 comme close lorsqu'elle contient le symbole de contradiction $\clv$.
  63
  64 Il n'est pas nécessaire, pour l'application de la règle de
  65 contradiction, que $A$ et $\sur A$ figurent dans cet ordre, ni même
  66 consécutivement, dans l'arbre : il suffit qu'ils soient dans la même
  67 branche.
  68
  69 \subsubsection{Justification de la méthode}
  70
  71 Le théorème suivant fonde cette méthode :\saut
  72
  73 \begin{Th}[Théorème de Beth]
  74 \index{théorème!de Beth}
  75 La formule $F$ est un théorème si et seulement si $\sur F$ est la
  76 racine d'un arbre dont toutes les branches sont closes.
  77 \end{Th}
  78
  79
  80
  81 \subsubsection{Exemple}
  82
  83 Démonstration de $\theor ((P\imp Q)\imp P)\imp P$\saut
  84 $$\begin{array}{|c|c|}
  85 \noalign{\hrule}
  86 \multicolumn{2}{|c|}{\tvii{15}\sur{((P\imp Q)\imp P)\imp P}}\cr
  87 \noalign{\hrule}
  88 \multicolumn{2}{|c|}{\tvii{15}\sur P}\cr
  89 \noalign{\hrule}
  90 \multicolumn{2}{|c|}{\tvii{15}(P\imp Q)\imp Q}\cr
  91 \noalign{\hrule}
  92 \tvii{15}\sur{P\imp Q} &  P\cr
  93 \noalign{\hrule}
  94 \tvii{15}  P      &        \clv\cr
  95 \noalign{\hrule}
  96 \tvii{15} \sur Q & \cr
  97 \noalign{\hrule}
  98 \tvii{15}  \clv & \cr
  99 \noalign{\hrule}
 100 \end{array}$$