La sémantique formelle est une théorie linguistique large, destinée à étudier le fonctionnement du langage et sa relation avec la réalité. Les linguistes définissent soigneusement les conditions de vérité de chaque énoncé, qui sont les situations qui doivent être des faits pour que la phrase soit vraie. Les phrases sont ensuite transcrites en équations mathématiques, principalement en utilisant le calcul lambda typé.
La théorie de la sémantique formelle a été développée pour la première fois par le philosophe et mathématicien américain Richard Montague dans les années 1960. Sa version spécifique est connue sous le nom de Montague Grammar. Depuis lors, cette théorie s’est développée dans de nombreuses directions, y compris la grammaire catégorique, lancée par Yehoshua Bar-Hillel dans les années 1970, et la sémantique Glue, publiée par Mary Dalrymple dans les années 1990.
Un autre type, la théorie de la représentation du discours, a été développé en 1981 par le linguiste néerlandais Hans Kamp. Cette théorie linguistique spécifique est parfois désignée sous le terme générique de sémantique formelle. La théorie de la représentation du discours tente d’analyser l’ensemble du discours, ou de la conversation, plutôt que des phrases isolées, et de le présenter dans des équations mathématiques.
Toutes les branches de la sémantique formelle se concentrent sur la relation entre langage et réalité ; en d’autres termes, leur objectif est de trouver le lien entre ce qui est dit et ce qui est. Les mots sont appelés signifiants tandis que les choses elles-mêmes sont appelées denotata, ou, dans la théorie de la représentation du discours, référents du discours. Dans la phrase Le chien a aboyé, le mot chien est un signifiant, alors que le chien lui-même est un référent du discours.
Une déclaration peut avoir plus d’une condition de vérité, ou exigence pour être vraie. Souvent, ces conditions de vérité conduisent à l’implication, qui est le terme utilisé lorsque la vérité d’une phrase exige qu’une autre soit vraie. En d’autres termes, dans une situation impliquée, si la phrase A est vraie, alors la phrase B doit être vraie aussi.
Pour déterminer les conditions de vérité d’un énoncé, les linguistes doivent rechercher tous les quantificateurs présents. Un quantificateur est un mot qui indique combien de choses sont impliquées, telles que chacune, toutes, toutes et certaines. Ces mots peuvent changer considérablement le sens d’un énoncé.
Le type de mathématiques le plus souvent utilisé pour analyser le langage en sémantique formelle est le lambda-calcul typé. Les mots peuvent être identifiés comme différentes variables et placés dans une équation ; dans la théorie de la représentation du discours, ces équations sont appelées structures de représentation du discours. Bien que principalement une théorie linguistique, la sémantique formelle est un domaine multidisciplinaire. Linguistes, philosophes, logiciens, mathématiciens et programmeurs sont tous impliqués. Analyser et créer des langages de programmation et même étudier l’intelligence artificielle peuvent tous impliquer une sémantique formelle.