La sémantique formelle est un courant linguistique qui tâche de comprendre le sens en construisant des modèles mathématiques précis. On doit entre autres les origines de la sémantique formelle à Frege (1848-1925), et à son article fondateur intitulé « Über Sinn und Bedeutung », soit : « Sens et dénotation ». Plus généralement, la sémantique formelle établit des systèmes qui cherchent à croiser les questions de logique et de langage.
La logique s’intéresse aux arguments, à leur validité et à leur véracité. Un argument est la donnée d’une conclusion et d’un ensemble de prémisses censées la justifier. Ainsi, par exemple, « Si Paul boit, Jean trinque ». Les prémisses et les conclusions sont des énoncés qui sont susceptibles d’être vrais ou faux.
La sémantique est la partie de la logique qui s’occupe de l’interprétation du langage formel. Les expressions linguistiques décrivent (réfèrent à) une situation du monde. On dit qu’elles ont une dénotation. La dénotation d’une expression linguistique est la réalité extralinguistique à laquelle l’expression peut être reliée.
La sémantique formelle cherche à comprendre les principes utilisés par le locuteur pour définir des relations entre des expressions en langage naturel et les environnements qui supportent un discours faisant sens. Soit un discours valide et véridique selon l’approche logique.
Il existe principalement trois styles de sémantiques formelles : opérationnelles, axiomatiques et dénotationnelles.
Les sémantiques opérationnelles sont adaptées à la vérification formelle de propriétés sémantiques. Les sémantiques axiomatiques sont adaptées à la preuve de programmes. Les sémantiques dénotationnelles permettent de définir des sémantiques plus abstraites à l'aide de formalismes mathématiques.
