## [Sémantique Preuve-Théorique](/fr/node/61002) Définition 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 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 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 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 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 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 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 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 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.