Formell semantik är en bred språklig teori, avsedd att studera hur språket fungerar och dess förhållande till verkligheten. Lingvister definierar noggrant varje påståendes sanningsvillkor, vilket är de situationer som måste vara fakta för att meningen ska vara sann. Meningar transkriberas sedan till matematiska ekvationer, främst med hjälp av maskinskriven lambda-kalkyl.
Teorin om formell semantik utvecklades först av den amerikanske filosofen och matematikern Richard Montague på 1960-talet. Hans specifika version är känd som Montague Grammar. Sedan dess har denna teori utvecklats i många riktningar, inklusive kategorisk grammatik, som pionjären av Yehoshua Bar-Hillel på 1970-talet, och Glue semantics, publicerad av Mary Dalrymple på 1990-talet.
En annan typ, diskursrepresentationsteori, utvecklades 1981 av den holländska lingvisten Hans Kamp. Denna specifika språkliga teori hänvisas ibland till under den generiska termen formell semantik. Diskursrepresentationsteori försöker analysera hela diskursen, eller konversationen, snarare än isolerade meningar, och presentera den i matematiska ekvationer.
Alla grenar av formell semantik fokuserar på förhållandet mellan språk och verklighet; med andra ord, deras mål är att hitta sambandet mellan vad som sägs och vad som är. Ord hänvisas till som signifiers medan själva sakerna kallas för denotata, eller, i diskursrepresentationsteori, diskursreferenser. I meningen ”Hunden skällde” är ordet ”hund” en betecknare, medan den faktiska hunden är en diskursreferent.
Ett påstående kan ha mer än ett sanningsvillkor eller krav för att vara sant. Ofta leder dessa sanningsvillkor till entailment, vilket är termen som används när en menings sanning kräver att en annan är sann. Med andra ord, i en medförd situation, om mening A är sann, måste mening B också vara sann.
För att bestämma ett påståendes sanningsvillkor måste lingvister leta efter eventuella kvantifierare som finns. En kvantifierare är ett ord som anger hur många saker som är inblandade, till exempel varje, varje, någon och några. Dessa ord kan ändra ett uttalandes betydelse väsentligt.
Den typ av matematik som oftast används för att analysera språk i formell semantik är typad lambda-kalkyl. Ord kan identifieras som olika variabler och placeras i en ekvation; i diskursrepresentationsteori är dessa ekvationer kända som diskursrepresentationsstrukturer. Även om den främst är en språklig teori, är formell semantik ett multidisciplinärt område. Språkvetare, filosofer, logiker, matematiker och programmerare är alla inblandade. Att analysera och skapa programmeringsspråk och till och med studera artificiell intelligens kan alla involvera formell semantik.