Une approche qui attribue du sens aux connecteurs logiques et aux formules par leurs rôles dans l'inférence — règles d'introduction et d'élimination — plutôt que par des conditions de vérité modèle-théoriques.

Principe

Le sens est donné par les schémas inférentiels canoniques : les connecteurs sont caractérisés par les mouvements inférentiels qui les introduisent et les éliminent dans les preuves, faisant des transformations de preuve le cœur de la sémantique.

Démonstration

En déduction naturelle, la conjonction reçoit son sens par la règle d'introduction (à partir de A et B on infère A∧B) et par les règles d'élimination (à partir de A∧B on infère A ou B) ; ces règles déterminent conjointement le fonctionnement sémantique du connecteur dans les contextes de preuve.

Mauvaise application

Considérer arbitrairement des systèmes de preuve comme fournissant une sémantique sans garantir l'harmonie ou la normalisation peut produire des significations inconsistantes ; prendre des règles syntactiques comme sens sans vérifier leur stabilité sous transformations de preuve est une mauvaise application.

Conséquence

Les connecteurs et les formules acquièrent des sens liés à leur usage inférentiel ; cela rapproche fortement théorie des preuves et sémantique, soutient des comptes normatifs de l'assertion et de l'inférence, et peut guider des interprétations constructives des constantes logiques.

Inversion

La sémantique modèle-théorique inverse l'accent en définissant le sens par la vérité dans des structures, puis en dérivant des règles de preuve, au lieu de partir des rôles inférentiels.

Limite

S'applique principalement aux systèmes dont les règles de preuve sont bien comportées (canoniques, en harmonie et supportant la normalisation) ; elle est limitée pour traiter des propriétés purement extensionnelles, basées sur les modèles, ou des logiques sans systèmes de preuve adéquats.

Tension sémantique

Tension entre sens inférentiel (d'usage) et sens modèle-théorique (fondé sur la vérité) : certains phénomènes sont naturellement saisis par les preuves (contenu constructif) tandis que d'autres exigent des modèles extensionnels (conditions de vérité sur des structures).

Synthèse

La Sémantique Preuve-Théorique conçoit le sens logique comme émergent des opérations de preuve canoniques : expliciter le comportement d'introduction et d'élimination et leur harmonie fournit une sémantique qui relie les schémas normatifs d'inférence à l'interprétation des constantes logiques.