Règle d'inférence - Rule of inference

Dans la philosophie de la logique , une règle d'inférence , règle d'inférence ou règle de transformation est une forme logique consistant en une fonction qui prend place, analyse leur syntaxe , et renvoie une conclusion (ou conclusions ). Par exemple, la règle d'inférence appelée modus ponens prend deux prémisses, une sous la forme "Si p alors q" et une autre sous la forme "p", et renvoie la conclusion "q". La règle est valable par rapport à la sémantique de la logique classique (ainsi qu'à la sémantique de nombreuses autres logiques non classiques ), en ce sens que si les prémisses sont vraies (sous une interprétation), alors la conclusion l'est aussi.

Typiquement, une règle d'inférence préserve la vérité, une propriété sémantique. Dans la logique multivaluée , il conserve une désignation générale. Mais l'action d'une règle d'inférence est purement syntaxique et n'a besoin de préserver aucune propriété sémantique : toute fonction d'ensembles de formules en formules compte comme règle d'inférence. Habituellement, seules les règles récursives sont importantes ; c'est-à-dire des règles telles qu'il existe une procédure efficace pour déterminer si une formule donnée est la conclusion d'un ensemble donné de formules selon la règle. Un exemple d'une règle qui n'est pas efficace dans ce sens est la règle infinitaire .

Les règles populaires d'inférence dans la logique propositionnelle incluent le modus ponens , le modus tollens et la contraposition . La logique des prédicats du premier ordre utilise des règles d'inférence pour traiter les quantificateurs logiques .

Forme standard

Dans la logique formelle (et dans de nombreux domaines connexes), les règles d'inférence sont généralement données sous la forme standard suivante :

  Prémisse#1
  Prémisse#2
        ...
  Prémisse#n
  Conclusion

Cette expression indique que chaque fois qu'au cours d'une dérivation logique, les prémisses données ont été obtenues, la conclusion spécifiée peut également être considérée comme allant de soi. Le langage formel exact qui est utilisé pour décrire à la fois les prémisses et les conclusions dépend du contexte réel des dérivations. Dans un cas simple, on peut utiliser des formules logiques, comme dans :

{\style d'affichage A\à B}

{\underline {A\quad \quad \quad }}\,\!

{\style d'affichage B\!}

C'est la règle du modus ponens de la logique propositionnelle . Les règles d'inférence sont souvent formulées sous forme de schémas utilisant des métavariables . Dans la règle (schéma) ci-dessus, les métavariables A et B peuvent être instanciées à n'importe quel élément de l'univers (ou parfois, par convention, à un sous-ensemble restreint tel que les propositions ) pour former un ensemble infini de règles d'inférence.

Un système de preuve est formé d'un ensemble de règles enchaînées pour former des preuves, également appelées dérivations . Toute dérivation n'a qu'une seule conclusion finale, qui est l'énoncé prouvé ou dérivé. Si les prémisses ne sont pas satisfaites dans la dérivation, alors la dérivation est une preuve d'un énoncé hypothétique : « si les prémisses sont vraies, alors la conclusion est vraie. »

Exemple : systèmes de Hilbert pour deux logiques propositionnelles

Dans un système de Hilbert , les prémisses et la conclusion des règles d'inférence sont simplement des formules d'un langage, employant généralement des métavariables. Pour la compacité graphique de la présentation et pour souligner la distinction entre axiomes et règles d'inférence, cette section utilise la notation séquentielle ( ) au lieu d'une présentation verticale des règles. Dans cette notation, ${\style d'affichage \vdash }$

${\begin{array}{c}{\text{Premise }}1\\{\text{Premise }}2\\\hline {\text{Conclusion}}\end{array}}$

est écrit comme . $({\text{Local }}1),({\text{Local }}2)\vdash ({\text{Conclusion}})$

Le langage formel de la logique propositionnelle classique peut être exprimé en utilisant uniquement la négation (¬), l'implication (→) et les symboles propositionnels. Une axiomatisation bien connue, comprenant trois schémas d'axiomes et une règle d'inférence ( modus ponens ), est :

(CA1) ⊢ A → (B → A)

(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(MP)  A, A → B ⊢ B

Il peut sembler redondant d'avoir deux notions d'inférence dans ce cas, ⊢ et →. Dans la logique propositionnelle classique, ils coïncident en effet ; le théorème de la déduction stipule que A ⊢ B si et seulement si ⊢ A → B . Il y a cependant une distinction à souligner même dans ce cas : la première notation décrit une déduction , c'est-à-dire une activité de passage de phrases en phrases, alors que A → B est simplement une formule faite avec un connecteur logique , implication dans ce cas. Sans règle d'inférence (comme le modus ponens dans ce cas), il n'y a pas de déduction ou d'inférence. Ce point est illustré dans le dialogue de Lewis Carroll intitulé " Ce que la tortue a dit à Achille ", ainsi que dans les tentatives ultérieures de Bertrand Russell et Peter Winch pour résoudre le paradoxe introduit dans le dialogue.

Pour certaines logiques non classiques, le théorème de déduction ne tient pas. Par exemple, la logique à trois valeurs de ukasiewicz peut être axiomatisée comme :

(CA1) ⊢ A → (B → A)

(LA2) ⊢ (A → B) → ((B → C) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(LA4) ⊢ ((A → ¬A) → A) → A

(MP)  A, A → B ⊢ B

Cette séquence diffère de la logique classique par le changement de l'axiome 2 et l'ajout de l'axiome 4. Le théorème de déduction classique ne tient pas pour cette logique, cependant une forme modifiée est vraie, à savoir A ⊢ B si et seulement si ⊢ A → ( A → B ).

Admissibilité et dérivabilité

Dans un ensemble de règles, une règle d'inférence pourrait être redondante dans le sens où elle est admissible ou dérivable . Une règle dérivable est une règle dont la conclusion peut être déduite de ses prémisses en utilisant les autres règles. Une règle admissible est une règle dont la conclusion est valable chaque fois que les prémisses sont vérifiées. Toutes les règles dérivables sont admissibles. Pour apprécier la différence, considérons l'ensemble de règles suivant pour définir les nombres naturels (le jugement affirme le fait qu'il s'agit d'un nombre naturel) : $n\,\,{\mathsf {nat}}$ ${\style d'affichage n}$

{\begin{matrix}{\begin{array}{c}\\\hline {\mathbf {0} \,\,{\mathsf {nat}}}\end{array}}&{\begin {array}{c}{n\,\,{\mathsf {nat}}}\\\hline {\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}\ end{tableau}}\end{matrice}}

La première règle indique que 0 est un nombre naturel et la seconde indique que s( n ) est un nombre naturel si n l' est. Dans ce système de preuve, la règle suivante, démontrant que le deuxième successeur d'un nombre naturel est aussi un nombre naturel, est dérivable :

{\begin{array}{c}{n\,\,{\mathsf {nat}}}\\\hline {\mathbf {s(s(} n\mathbf {))} \,\, {\mathsf {nat}}}\end{array}}

Sa dérivation est la composition de deux utilisations de la règle du successeur ci-dessus. La règle suivante pour affirmer l'existence d'un prédécesseur pour tout nombre différent de zéro est simplement admissible :

{\begin{array}{c}{\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}\\\hline {n\,\,{\mathsf {nat}}}\end{array}}

C'est un fait vrai des nombres naturels, comme on peut le prouver par induction . (Pour prouver que cette règle est admissible, supposez une dérivation de la prémisse et induisez-la pour produire une dérivation de .) Cependant, elle n'est pas dérivable, car elle dépend de la structure de la dérivation de la prémisse. Pour cette raison, la dérivabilité est stable sous des ajouts au système de preuve, alors que l'admissibilité ne l'est pas. Pour voir la différence, supposons que la règle de non-sens suivante ait été ajoutée au système de preuve : $n\,\,{\mathsf {nat}}$

{\begin{array}{c}\\\hline {\mathbf {s(-3)} \,\,{\mathsf {nat}}}\end{array}}

Dans ce nouveau système, la règle du double successeur est toujours dérivable. Cependant, la règle pour trouver le prédécesseur n'est plus admissible, car il n'y a aucun moyen de dériver . La fragilité de l'admissibilité vient de la manière dont elle est prouvée : puisque la preuve peut induire sur la structure des dérivations des prémisses, les extensions au système ajoutent de nouveaux cas à cette preuve, qui peut ne plus tenir. $\mathbf {-3} \,\,{\mathsf {nat}}$

Les règles admissibles peuvent être considérées comme des théorèmes d'un système de preuve. Par exemple, dans un calcul séquentiel où l' élimination de coupe est vérifiée, la règle de coupe est admissible.

Languages

In other projects

Règle d'inférence - Rule of inference

Contenu

Forme standard

Exemple : systèmes de Hilbert pour deux logiques propositionnelles

Admissibilité et dérivabilité

Voir également

Les références