Un dispositif formel constitué d'un langage formel accompagné d'un ensemble d'axiomes (ou schémas d'axiomes) et de règles d'inférence qui déterminent quelles suites de formules constituent des dérivations valides des prémisses aux conclusions.

Principe

Spécifier des vérités primitives et des étapes de transformation admissibles de sorte que la dérivabilité soit mécaniquement vérifiable et préserve des propriétés sémantiques voulues comme la correction et la complétude par rapport à une sémantique.

Démonstration

Un système déductif de type Hilbert pour la logique propositionnelle peut comporter des schémas d'axiomes et le modus ponens comme seule règle ; avec les axiomes et leurs instances, l'application répétée du modus ponens permet de dériver des théorèmes.

Mauvaise application

Mélanger des règles d'inférence sans tenir compte de la capture de variables ou des conditions latérales — par exemple appliquer l'instanciation universelle à une formule où la variable est liée ailleurs — produit des dérivations invalides et des preuves non correctes.

Conséquence

Un système déductif bien spécifié clarifie la provabilité, permet la recherche et la mécanisation de preuves, et soutient des résultats métathéoriques (p. ex. cohérence, décidabilité, complétude) lorsqu'on le compare à la sémantique.

Inversion

La vue inverse met l'accent sur la conséquence sémantique seule (modèles et implication) et considère les règles et axiomes comme des artefacts secondaires plutôt que comme la définition principale de la conséquence.

Limite

Désigne les systèmes formels avec règles syntaxiques explicites ; n'inclut pas l'argumentation informelle, l'inférence empirique ou les notions purement modèle-théoriques de conséquence qui omettent les dérivations syntaxiques.

Tension sémantique

Une tension existe entre les définitions proof-théoriques de la conséquence (dérivabilité dans un système) et les définitions sémantiques (implication dans tous les modèles) ; les résultats de correction et de complétude servent à les réconcilier.

Synthèse

Un système déductif est le moteur syntaxique produisant des preuves formelles : les axiomes fournissent les formules de départ et les règles d'inférence les pas licites, définissant ensemble la relation de dérivabilité dans une logique.