Petit « cours de logique »

Cette page est une simple annexe aux explications fournies sur la page du poème « Rigueur » bâti sur une preuve logique en déduction naturelle (pour en savoir plus, on peut lire dans Wikipédia l’article sur la Déduction Naturelle introduite par Gerhard Gentzen  ) :

La formule logique suivante
( a -> e ) -> (( a -> i) -> ( a -> e & i))
se lit ainsi

si je sais que « a » entraîne « e »
et si de plus « a » entraîne « i »,
alors dès que je sais que « a » est vrai
j’en déduis « e et i  »

Comment prouve-t-on une telle chose ? On suppose que (a -> e) est vrai et on démontre alors que  ( a -> i) -> ( a -> e & i). Pour ce faire on suppose tour à tour que (a -> i) puis que a sont vrais et il reste à prouver e & i.

Sous ces 3 hypothèses, la preuve peut se construire sous la forme d’un « arbre de preuve » dans lequel chaque « fraction » représente un petit syllogisme de la forme

hypothèses
----------
conclusion

Voici cet arbre de preuve :

a -> e   a            a -> i  a
----------            ---------
    e                     i
    -----------------------
             e & i

Tout logicien est alors convaincu qu’on a prouvé a -> e & i sous les hypothèses (a -> e) et (a -> i), ce qu’on représentera par

a -> e   [a]            a -> i  [a]
------------            -----------
     e                       i
     -------------------------
               e & i
            ----------
            a -> e & i

On dit qu’on a « déchargé » l’hypothèse a. De même en déchargeant successivement les deux autres hypothèses on obtient la preuve de la formule désirée :

[a -> e]   [a]            [a -> i]  [a]
--------------            -------------
      e                         i
      ---------------------------
                 e & i
            ---------------
              a -> e & i
      --------------------------
      ( a -> i) -> ( a -> e & i)
------------------------------------------
( a -> e ) -> (( a -> i) -> ( a -> e & i))

Par commodité, la contrainte mise en œuvre dans le poème se base sur l’écriture de cette preuve sous une forme linéaire, chaque conclusion trouvant ses hypothèses au dessus d’elle. Il y a plusieurs façons de le faire, par exemple comme suit :

[ a -> e ]
[a]
e
[ a -> i ]
[a]
i
e & i
a -> e & i
( a -> i ) -> ( a -> e & i )
( a -> e ) -> ( ( a -> i ) -> ( a -> e & i ))