Logique et ensemblesFormule · Glossaire
Règle d'inférence
Une règle d'inférence est une loi formelle de déduction qui permet de passer de prémisses à une conclusion dans un système logique. Elle s'écrit généralement sous forme d'une fraction dont le numérateur contient les prémisses et le dénominateur la conclusion. Les règles d'inférence les plus connues sont le modus ponens (de P et de 'si P alors Q', déduire Q) et le modus tollens. Dans le calcul des séquents et la déduction naturelle, les règles d'inférence définissent les étapes légales de construction d'une preuve formelle.
Sommaire
Ce que vous allez apprendre
- Distinguer les prémisses, la conclusion et la règle qui autorise leur enchaînement.
- Lire le schéma formel du modus ponens et remplacer P et Q par des propositions concrètes.
- Vérifier pas à pas une application avec un témoin allumé et un système prêt.
- Reconnaître l'affirmation du conséquent et la négation de l'antécédent.
- Relier les règles d'inférence à la déduction naturelle et au calcul des séquents.
En clair
Un témoin est allumé. Une consigne annonce : « Si le témoin est allumé, alors le système est prêt. » Ces deux informations autorisent une nouvelle ligne : « Le système est prêt. »
Une règle d'inférence est ce passage contrôlé. Elle ne devine pas la conclusion : elle indique quelle conclusion est permise par la forme exacte des prémisses. Ici, la règle employée est le modus ponens.
Définition
Dans un système logique, une règle d'inférence fixe une transition autorisée entre des formules. Les formules placées au-dessus du trait sont les prémisses ; celle placée au-dessous est la conclusion. Appliquer la règle ajoute donc une étape légale à une preuve formelle.
Pour le modus ponens, la lettre P désigne une proposition et la lettre Q une autre proposition. Les prémisses sont P et l'implication « si P, alors Q » ; la conclusion est Q. Le modus tollens part de la même implication et de la négation de Q pour conclure à la négation de P. Dans chaque cas, les occurrences de P et de Q doivent correspondre exactement.
Une règle décrit une forme de passage, non le contenu particulier des propositions. En déduction naturelle comme dans le calcul des séquents, une preuve se construit en enchaînant de telles étapes selon les règles du système choisi.
Le principe
Le modus ponens s'applique lorsque P est disponible et que l'implication de P vers Q est disponible. Il autorise alors la conclusion Q. Son schéma est :
Le trait ne signifie pas une division. Il sépare les prémisses, au-dessus, de la conclusion autorisée, au-dessous.
Quand l'utiliser
L'application se fait dans un système logique dont les formules et les règles sont fixées. Pour le modus ponens, il faut disposer de deux prémisses : une formule P et une implication ayant exactement P pour antécédent et Q pour conséquent. La conclusion obtenue est alors Q.
Si l'on dispose seulement de l'implication et de Q, le passage vers P est bloqué : ce n'est pas le modus ponens. Il faut chercher une autre règle autorisée ou une prémisse supplémentaire. De même, remplacer P par une proposition simplement ressemblante ne satisfait pas le schéma.
Un exemple, pas à pas
Construisons une étape de preuve avec deux données. Première prémisse : « Le témoin est allumé. » Seconde prémisse : « Si le témoin est allumé, alors le système est prêt. »
1. Notons P la proposition « le témoin est allumé » et Q la proposition « le système est prêt ».
2. La première prémisse a la forme P. La seconde a la forme . La figure rassemble ces deux lignes et la conclusion qu'elles autorisent.
3. Les deux prémisses correspondent exactement au schéma du modus ponens. Nous pouvons donc conclure Q, c'est-à-dire : « Le système est prêt. »
4. Contrôlons la substitution : P occupe bien la première prémisse et l'antécédent de l'implication ; Q est bien son conséquent. La conclusion recopie Q, sans inverser l'implication ni ajouter d'information.
En pratique
Dans une preuve formelle, on repère les lignes déjà obtenues, puis on cherche une règle dont les prémisses ont exactement cette forme. Si aucune correspondance n'existe, on poursuit la preuve au lieu de forcer la conclusion.
En déduction naturelle, chaque nouvelle ligne est justifiée par une règle et par les lignes utilisées. Dans le calcul des séquents, on vérifie plutôt la transformation autorisée d'un séquent en un autre. Le système choisi détermine la présentation à employer.
Pour relire un raisonnement, on remplace les phrases par P et Q. Cette abstraction fait apparaître une inversion éventuelle : posséder Q et « si P, alors Q » ne suffit pas à conclure P.
À ne pas confondre
Implication et règle d'inférence. L'implication « si P, alors Q » est une formule qui peut servir de prémisse. Le modus ponens est la règle qui combine cette formule avec P pour produire Q. Dans l'exemple, la consigne est l'implication ; le passage à « le système est prêt » est l'inférence.
Règle et preuve. Une règle autorise un type d'étape ; une preuve est un enchaînement complet d'étapes légales. Voir un modus ponens justifie donc une transition précise, mais ne décrit pas à lui seul toute la preuve.
Limites et pièges
Affirmer le conséquent. De Q et de « si P, alors Q », conclure P inverse illégitimement le passage. Le symptôme est l'absence de P parmi les prémisses ; il faut renoncer à cette conclusion ou fournir une autre justification.
Nier l'antécédent. De la négation de P et de « si P, alors Q », on ne peut pas conclure la négation de Q. Ce couple ne correspond ni au modus ponens ni au modus tollens ; une autre règle ou une autre prémisse est nécessaire.
Correspondance seulement apparente. Une prémisse proche de P ne remplit pas automatiquement la place de P. Si les formules diffèrent, il faut d'abord justifier leur passage par une règle du système.
Prémisses non établies. Une application formellement correcte montre ce qui suit des prémisses ; elle ne fournit pas, à elle seule, leur justification. Il faut donc distinguer le contrôle de l'étape et l'établissement des lignes dont elle part.
Pour aller plus loin
modus ponens — Approfondir la règle utilisée dans l'exemple et sa forme avec deux prémisses.
modus tollens — Examiner l'inférence qui part de la négation du conséquent pour nier l'antécédent.
déduction naturelle — Voir comment des règles d'inférence organisent ligne après ligne une preuve formelle.
Les théorèmes d'incomplétude de Gödel — Situer les limites de certains systèmes formels au-delà de l'application locale de leurs règles.
Explorez les mathématiques autrement
Retrouvez nos magazines, podcasts et jeux pour explorer les mathématiques autrement.
Découvrir les offres