Règle d'inférence

Dans un système logique, les règles d'inférence sont les règles qui fondent le processus de déduction, de dérivation ou de démonstration. L'application des règles sur les axiomes du système permet d'en démontrer les théorèmes.

Définitions et représentations

Une règle d'inférence est une fonction qui prend un $n$ -uplet de formules et rend une formule. Les formules arguments sont appelées « les prémisses » et la formule retournée est appelée la « conclusion ». Les règles d'inférence peuvent également être vues comme des relations liant prémisses et conclusions par lesquelles une conclusion est dite « déductible » ou « dérivable » des prémisses. Si l'ensemble des prémisses est vide, alors la conclusion est appelée un « théorème » ou un « axiome » de la logique.

Les règles d'inférences sont en général données dans la forme standard suivante :

  Prémisse n^o 1
  Prémisse n^o 2
        ...
  Prémisse n^o n
  Conclusion

Cette expression dit que si on se trouve au milieu d'une dérivation logique, où les prémisses ont été déjà obtenues (c'est-à-dire dérivées logiquement des axiomes), alors on peut affirmer que la conclusion est obtenue. Le langage formel utilisé pour décrire les prémisses et la conclusion dépend du système formel ou logique où l'on s'est placé. Dans le cas le plus simple, les formules sont tout simplement des expressions logiques; c'est ainsi le cas pour le modus ponens :

  A→B
  A
  ∴B

Les règles d'inférence peuvent aussi être formulées de cette manière :

un certain nombre de prémisses (peut-être aucune) ;
un symbole de dérivation $\vdash$ signifiant « infère », « démontre » ou « conclut » ;
une conclusion.

Cette formulation représente habituellement la vision relationnelle (par opposition à fonctionnelle) d'une règle d'inférence, où le symbole de dérivation représente une relation de démontrabilité existant entre prémisses et conclusion.

Les règles d'inférences sont aussi parfois présentées à la manière de cette expression du modus ponens, qui exprime bien la nécessité que les prémisses soient des théorèmes :

Si

\vdash

A → B et

\vdash

A, alors

\vdash

B.

Les règles d'inférence sont en général formulées comme des « schémas de règles », par l'utilisation de variables universelles. Dans les schémas ci-dessus, A et B peuvent être remplacés par n'importe quelle formule bien formée de la logique propositionnelle (on se limite parfois à un sous-ensemble des formules de la logique, comme les propositions) pour former un ensemble infini de règles d'inférence.

Un système de démonstration est formé d'un ensemble de règles, pouvant être enchaînées les unes aux autres pour former des démonstrations, ou dérivations. Une dérivation n'a qu'une seule conclusion finale, qui est l'expression démontrée ou dérivée. Si les prémisses ne sont pas satisfaites, alors la dérivation est la démonstration d'une expression hypothétique : si les prémisses sont satisfaites, alors la conclusion est satisfaite.

De même que les axiomes sont des règles sans prémisse, les schémas d'axiome peuvent également être vus comme des schémas de règles d'inférence sans prémisse.

Exemples

La règle d'inférence de base de la logique propositionnelle est le modus ponens, à côté d'elle on trouve le modus tollens et des règles qui décrivent le comportement des connecteurs. Pour la logique des prédicats du premier ordre, il existe des règles d'inférence qui gèrent les quantificateurs comme la règle de généralisation.

Il existe aujourd'hui de nombreux systèmes de logique formelle, chacun ayant son propre langage de formules bien formées, ses propres règles d'inférence et sa propre sémantique; c'est le cas des logiques modales qui font usage de la règle de nécessitation.

Règles d'inférence et axiomes

Les règles d'inférence doivent être distingués des axiomes d'une théorie. En termes de sémantique, les axiomes sont des assertions valides. Les axiomes sont habituellement considérés comme des points de départ pour l'application de règles d'inférence et la génération d'ensembles de conclusions. Ou encore, en termes moins techniques :

Les règles sont des affirmations à propos du système, les axiomes sont des affirmations appartenant au système. Par exemple :

La règle qui dit qu'à partir de $\vdash$ p on peut inférer $\vdash$ Démontrable(p) est une affirmation disant que si l'on a démontré p, alors p est démontrable. Cette règle s'applique dans l'arithmétique de Peano, par exemple ;
L'axiome p $\to$ Démontrable(p) voudrait dire que toute assertion vraie est démontrable. Cette affirmation est par contre fausse dans l'arithmétique de Peano (c'est la caractérisation de son incomplétude).

Propriétés

Effectivité

Une propriété désirable pour une règle d'inférence est qu'elle soit effective[1]. C'est-à-dire, qu'il y ait une procédure effective déterminant si une formule donnée est dérivable d'un ensemble de formules défini. La omega-règle[2], qui est une règle infinitaire, est un exemple de règle non effective. Il est possible cependant de définir des démonstrations avec omega-règles effectives, mais c'est une contrainte que l'on ajoute et qui ne vient pas de la nature des règles, comme c'est le cas pour les systèmes de démonstrations ordinaires.

Une règle d'inférence ne préserve pas nécessairement les propriétés sémantiques comme la vérité ou la validité. En fait, une logique caractérisée de manière purement syntaxique n'a pas forcément de sémantique. Une règle peut préserver, par exemple, la propriété d'être la conjonction d'une sous-formule de la plus longue formule de l'ensemble des prémisses. Cependant, dans de nombreux systèmes, les règles d'inférences sont utilisées pour engendrer (c'est-à-dire démontrer) des théorèmes à partir d'autres théorèmes et d'axiomes.

Admissibilité et dérivabilité

Dans un ensemble de règles, une règle d'inférence peut être redondante au sens où elle est « admissible » ou « dérivable ». Une règle dérivable est une règle dont la conclusion peut être dérivée de ses prémisses en utilisant les autres règles. Une règle admissible est une règle dont la conclusion est dérivable, quand les prémisses sont dérivables. Toutes les règles dérivables sont donc admissibles, mais dans certains systèmes de règles, il peut exister des règles admissibles non dérivables. Pour apprécier la différence, on peut considérer un ensemble de règles pour définir les entiers naturels (le jugement $n\,\,{\mathsf {nat}}$ affirmant le fait que $n$ est un entier naturel) :

${\begin{matrix}{\frac {}{\mathbf {0} \,\,{\mathsf {nat}}}}&{\frac {n\,\,{\mathsf {nat}}}{\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}}\\\end{matrix}}$

La première règle dit que 0 est un entier naturel, la deuxième dit que s(n), le successeur de n, est un entier naturel si n en est un. Dans ce système logique, la règle suivante, qui dit que le second successeur d'un entier naturel est également un entier naturel, est dérivable :

${\frac {n\,\,{\mathsf {nat}}}{\mathbf {s(s(} n\mathbf {))} \,\,{\mathsf {nat}}}}$

Sa dérivation est simplement la composition de deux utilisations de la règle de succession citée plus haut. La règle suivante, qui affirme l'existence d'un prédécesseur pour chaque entier naturel non nul, n'est qu'admissible :

${\frac {\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}{n\,\,{\mathsf {nat}}}}$

Le fait est vrai pour les entiers naturels et peut être démontré par induction (pour montrer l'admissibilité de cette règle, il faudrait supposer que la prémisse est dérivable, et obtenir par induction une dérivation de $n\,\,{\mathsf {nat}}$ ). Par contre, elle n'est pas dérivable, parce qu'elle dépend de la structure de la dérivation de la prémisse. Pour cette raison, la dérivabilité est préservée quand on étend un système logique, alors que l'admissibilité ne l'est pas. Pour voir la différence, supposons que la règle suivante (absurde) soit ajoutée au système logique :

${\frac {}{\mathbf {s(-3)} \,\,{\mathsf {nat}}}}$

Dans ce nouveau système, la règle du double-successeur est toujours dérivable. Par contre, la règle d'existence d'un prédécesseur n'est plus admissible, parce qu'il est impossible de dériver $\mathbf {-3} \,\,{\mathsf {nat}}$ . La relative fragilité de l'admissibilité vient de la manière dont elle est démontrée : puisque la démonstration procède par induction sur la structure de la dérivation des prémisses, les extensions du système ajoutent de nouveaux cas à cette démonstration, qui peut ne plus être valable.

Les règles admissibles peuvent être considérées comme des théorèmes d'un système logique. Par exemple, dans le calcul des séquents où l'élimination des coupures est valide, la règle de coupure est admissible.

Terminologie

Les règles d'inférence ont été définies formellement par Gerhard Gentzen, qui les a appelées des figures ou des figures de déduction (Schlußfiguren). Dans leur présentation $H_{1}$ , ..., $H_{n}$ $\vdash$ $C$ , ces objets mathématiques sont appelées des séquents ou des jugements. Les $H_{i}$ sont alors appelées les antécédents ou les hypothèses et $C$ est appelée le conséquent ou la conséquence.

Notes et références

Church, 1956.
Jean-Yves Girard Proof Theory and Logical Complexity, ch. 6.

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Rule of inference » (voir la liste des auteurs).

Articles connexes

Portail de la logique
Portail de l'informatique théorique

Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.

[1] Church, 1956.

[2] Jean-Yves Girard Proof Theory and Logical Complexity, ch. 6.