La semantica formale è un’ampia teoria linguistica, intesa a studiare come funziona il linguaggio e il suo rapporto con la realtà. I linguisti definiscono attentamente le condizioni di verità di ogni affermazione, che sono quelle situazioni che devono essere fatti affinché la frase sia vera. Le frasi vengono quindi trascritte in equazioni matematiche, principalmente utilizzando il lambda calcolo tipizzato.
La teoria della semantica formale è stata sviluppata per la prima volta dal filosofo e matematico americano Richard Montague negli anni ‘1960. La sua versione specifica è conosciuta come Montague Grammar. Da quel momento, questa teoria si è sviluppata in molte direzioni, inclusa la grammatica categoriale, introdotta da Yehoshua Bar-Hillel negli anni ‘1970, e la semantica Glue, pubblicata da Mary Dalrymple negli anni ‘1990.
Un altro tipo, la teoria della rappresentazione del discorso, è stato sviluppato nel 1981 dal linguista olandese Hans Kamp. Questa specifica teoria linguistica è talvolta indicata con il termine generico semantica formale. La teoria della rappresentazione del discorso tenta di analizzare l’intero discorso, o conversazione, piuttosto che frasi isolate, e presentarlo in equazioni matematiche.
Tutti i rami della semantica formale si concentrano sul rapporto tra linguaggio e realtà; in altre parole, il loro obiettivo è trovare la connessione tra ciò che viene detto e ciò che è. Le parole sono chiamate significanti mentre le cose stesse sono chiamate denotata o, nella teoria della rappresentazione del discorso, referenti del discorso. Nella frase “Il cane abbaia”, la parola “cane” è un significante, mentre il cane reale è un referente del discorso.
Un’affermazione può avere più di una condizione di verità, o requisito per essere vera. Spesso queste condizioni di verità portano all’implicazione, che è il termine usato quando la verità di una frase richiede che un’altra sia vera. In altre parole, in una situazione implicata, se l’enunciato A è vero, allora anche l’enunciato B deve essere vero.
Per determinare le condizioni di verità di un’affermazione, i linguisti devono cercare tutti i quantificatori presenti. Un quantificatore è una parola che indica quante cose sono coinvolte, come ciascuna, ogni, qualsiasi e alcune. Queste parole possono cambiare sostanzialmente il significato di un’affermazione.
Il tipo di matematica più spesso utilizzato per analizzare il linguaggio nella semantica formale è il lambda calcolo tipizzato. Le parole possono essere identificate come variabili diverse e collocate all’interno di un’equazione; nella teoria della rappresentazione del discorso, queste equazioni sono note come strutture di rappresentazione del discorso. Sebbene sia principalmente una teoria linguistica, la semantica formale è un campo multidisciplinare. Sono coinvolti linguisti, filosofi, logici, matematici e programmatori. L’analisi e la creazione di linguaggi di programmazione e persino lo studio dell’intelligenza artificiale possono coinvolgere la semantica formale.