Bonjour,

J'apprends la logique en autodidacte et je calle sur un exemple de dérivation en déduction naturelle en format de séquent donné dans mon livre (Logique T.1, Gochet et Gribomont, p.152) parce que je ne parviens pas à identifier les règles qui permettent de passer d'une étape à l'autre à plusieurs reprises. Je vais essayer d'être le plus clair possible (je numérote les lignes pour signaler les inférences qui me posent problème.)

T = {s>(bVt),(bVa)>(rVm),-r}
0
1    T,b,(bVa)> (r^m) = (bva)> (r^m)
2    T,b = (bVa) > (r^m)
3    T,b,(bVa) = r^m (1)            T,b,(bVa),-r = -r (2)
4    T,b,(bVa)= r    (1)            T,b,(bVa) = -r (2)
5    T,b = b         T,b,(bVa) = F
6    T,b = bVa       T,b = - (bVa)
7              T,b = F
8 T = s>(bVt)(1) T,b = t (2) T,t = t (3)
9 T,s = (bVt)(1) T,s,b = t (2) T,s,t,=t (3)
10               T,s = t
11               T = s >t

Avec = pour la conséquence logique et > pour l'implication matérielle.

Les passages qui me posent problème sont :
- 0 à 1;
- 1 à 2 (même si je vois bien qu'on supprime (bVa)>(r^m) à  
gauche) ;
-2 à 3(2) (comme 0 à 1);
-3(2) à 4 (2) (comme 1 à 2)
- 7 à 8(2) et 7 à 8(3)

Ce n'est sans doute pas grand chose mais le manuel ne signale pas les règles qui lui permettent ces inférences. Merci par avance à tous ceux qui voudront bien m'aider.