La semántica formal es una teoría lingüística amplia, destinada a estudiar cómo funciona el lenguaje y su relación con la realidad. Los lingüistas definen cuidadosamente las condiciones de verdad de cada enunciado, que son aquellas situaciones que deben ser un hecho para que el enunciado sea verdadero. Luego, las oraciones se transcriben en ecuaciones matemáticas, principalmente utilizando cálculo lambda escrito.
La teoría de la semántica formal fue desarrollada por primera vez por el filósofo y matemático estadounidense Richard Montague en la década de 1960. Su versión específica se conoce como Montague Grammar. Desde entonces, esta teoría se ha desarrollado en muchas direcciones, incluida la gramática categórica, como fue pionera en Yehoshua Bar-Hillel en la década de 1970, y la semántica de Glue, publicada por Mary Dalrymple en la década de 1990.
Otro tipo, la teoría de la representación del discurso, fue desarrollada en 1981 por el lingüista holandés Hans Kamp. Esta teoría lingüística específica a veces se denomina bajo el término genérico semántica formal. La teoría de la representación del discurso intenta analizar el discurso completo, o la conversación, en lugar de oraciones aisladas, y presentarlo en ecuaciones matemáticas.
Todas las ramas de la semántica formal se centran en la relación entre el lenguaje y la realidad; en otras palabras, su objetivo es encontrar la conexión entre lo que se dice y lo que se dice. Las palabras se denominan significantes, mientras que las cosas mismas se denominan denotata o, en la teoría de la representación del discurso, referentes del discurso. En la frase “El perro ladró”, la palabra “perro” es un significante, mientras que el perro real es un referente del discurso.
Una declaración puede tener más de una condición de verdad o requisito para ser verdadera. A menudo, estas condiciones de verdad conducen a la implicación, que es el término utilizado cuando la verdad de una oración requiere que otra sea verdadera. En otras palabras, en una situación implicada, si el enunciado A es verdadero, entonces el enunciado B también debe serlo.
Para determinar las condiciones de verdad de un enunciado, los lingüistas deben buscar cualquier cuantificador presente. Un cuantificador es una palabra que indica cuántas cosas están involucradas, como cada, cada, cualquiera y algunas. Estas palabras pueden cambiar sustancialmente el significado de una declaración.
El tipo de matemáticas más utilizado para analizar el lenguaje en semántica formal es el cálculo lambda. Las palabras pueden identificarse como diferentes variables y colocarse dentro de una ecuación; en la teoría de la representación del discurso, estas ecuaciones se conocen como estructuras de representación del discurso. Aunque es principalmente una teoría lingüística, la semántica formal es un campo multidisciplinario. Están involucrados lingüistas, filósofos, lógicos, matemáticos y programadores. Analizar y crear lenguajes de programación e incluso estudiar la inteligencia artificial pueden involucrar semántica formal.