Sémantique formelle (logique)

En logique, la sémantique de la logique est l'étude de la sémantique, ou l'interprétation, des langages formels et naturels qui, en général, tentent de saisir la notion pré-théorique de déduction. Parmi les tâches des logiciens figure la fourniture de signification aux propositions. Avant l'avènement de la logique moderne, l'Organon d'Aristote, et en particulier De Interpretatione a servi de base à la compréhension de l'importance de la logique. L'introduction de la quantification, nécessaire à la résolution du problème de généralité multiple, a rendu impossible le genre d'analyse sujet-prédicat que régissait l'œuvre d'Aristote. Les principales approches modernes de la sémantique des langages formels sont les suivantes : La sémantique de la théorie des modèles est l'archétype de la théorie de la vérité d'Alfred Tarski, basé sur son schéma-T, et est l'un des concepts fondateurs de la théorie des modèles. Cette sémantique fournit les bases d'une approche à la théorie de la signification connue comme sous le nom de sémantique vériconditionnelle, qui a été développée, entre autres, par Richard Montague, David Lewis, Max Cresswell, Donald Davidson. La sémantique de Kripke introduit des innovations, mais largement conformes à la théorie tarskienne. La théorie de la démonstration donne le sens des propositions par le rôle qu'elles jouent dans des inférences. Gerhard Gentzen, Dag Prawitz et Michael Dummett sont considérés comme les fondateurs de cette approche; celle-ci est fortement liée à la philosophie de Ludwig Wittgenstein, en particulier à son aphorisme « meaning is use ». La sémantique de la valeur de vérité a été préconisée par Ruth Barcan Marcus pour les logiques modales au début des années 1960 et a plus tard été défendue par Dunn, Belnap et Leblanc pour la logique du premier ordre standard. Quand les langages formels sont des langages de programmation ou des systèmes décrivant des calculs, la sémantique formelle comporte trois branches: La sémantique axiomatique définit le sens de chaque élément de programme en caractérisant l'état du système avant et après l'application de cet élément de programme.