Un schéma ou un modèle qui permet de déduire une formule conclusion à partir d'une ou plusieurs formules prémisses dans un système déductif ; les règles d'inférence spécifient les pas admis dans les preuves formelles.

Principe

Une règle d'inférence transforme des prémisses en une conclusion tout en préservant une relation désignée (typiquement la vérité ou la dérivabilité) ; les règles saines préservent la vérité des prémisses vers la conclusion selon la sémantique visée.

Démonstration

Le modus ponens est une règle d'inférence : de 'P' et 'Si P alors Q' on déduit 'Q'. En calcul propositionnel, l'application de modus ponens aux formules P et P→Q produit Q comme pas déductif valide.

Mauvaise application

Appliquer une règle d'inférence en dehors de son contexte formel (par exemple utiliser des règles modales dans une dérivation purement classique) ou utiliser une règle non saine (qui ne préserve pas la vérité) conduit à des preuves invalides ou à des inférences fallacieuses.

Conséquence

Les règles d'inférence structurent les preuves et déterminent ce qui compte comme une dérivation ; avec les axiomes elles définissent la provabilité, permettent la démonstration de théorèmes et soutiennent des propriétés métathéoriques comme la correction et la complétude.

Inversion

L'inversion oppose les règles syntaxiques à la conséquence sémantique : au lieu de déduire des conclusions par des règles, on peut vérifier si les conclusions sont impliquées par les prémisses dans tous les modèles (conséquence sémantique plutôt que dérivation syntaxique).

Limite

Une règle d'inférence est spécifiée par rapport à un langage formel et à un calcul déductif choisis ; ce n'est pas elle-même une affirmation sémantique, et des systèmes différents adoptent des règles différentes (dédiction naturelle, calcul des séquents, systèmes de Hilbert).

Tension sémantique

Il existe une tension entre la recherche algorithmique de preuves (règles comme étapes opérationnelles en déduction automatique) et la justification normative (règles comme préservant la vérité) ; les stratégies pratiques peuvent privilégier des formulations de règles différentes des comptes philosophiques de l'inférence.

Synthèse

Une règle d'inférence est le mécanisme formel qui, à partir de prémisses, produit des conclusions admissibles selon l'appareil déductif ; elle opérationnalise la déduction, relie axiomes et théorèmes et garantit que les preuves respectent la relation sémantique visée.