Formalna semantika je široka jezikovna teorija, namenjena preučevanju delovanja jezika in njegovega odnosa z realnostjo. Jezikoslovci natančno opredelijo pogoje resnice vsake izjave, ki so tiste situacije, ki morajo biti resnične, da je stavek resničen. Stavki se nato prepišejo v matematične enačbe, predvsem z uporabo vtipkanega lambda računa.
Teorijo formalne semantike je v šestdesetih letih prejšnjega stoletja prvi razvil ameriški filozof in matematik Richard Montague. Njegova posebna različica je znana kot slovnica Montague. Od takrat se je ta teorija razvila v številnih smereh, vključno s kategorično slovnico, kot jo je v sedemdesetih letih prejšnjega stoletja uvedel Yehoshua Bar-Hillel, in semantiko lepila, ki jo je v 1960. letih objavila Mary Dalrymple.
Drugo vrsto, teorijo predstavitve diskurza, je leta 1981 razvil nizozemski jezikoslovec Hans Kamp. To specifično jezikovno teorijo včasih imenujemo s splošnim izrazom formalna semantika. Teorija predstavitve diskurza poskuša analizirati celoten diskurz oziroma pogovor, ne pa izolirane stavke, in ga predstaviti v matematičnih enačbah.
Vse veje formalne semantike se osredotočajo na razmerje med jezikom in realnostjo; z drugimi besedami, njihov cilj je najti povezavo med povedanim in tem, kar je. Besede imenujemo označevalci, stvari same pa se imenujejo denotata ali, v teoriji predstavitve diskurza, diskurzni referenti. V stavku »Pes je lajal« je beseda »pes« označevalec, medtem ko je dejanski pes diskurzni referent.
Izjava ima lahko več kot en pogoj resnice ali zahtevo, da je resnična. Ti pogoji resnice pogosto vodijo do posledic, kar je izraz, ki se uporablja, ko resnica enega stavka zahteva, da je drugi resničen. Z drugimi besedami, v zapleteni situaciji, če je stavek A resničen, mora biti resničen tudi stavek B.
Za določitev pogojev resnice izjave morajo jezikoslovci iskati vse prisotne kvantifikatorje. Kvantifikator je beseda, ki označuje, koliko stvari je vključenih, na primer vsaka, vsaka, katera koli in nekaj. Te besede lahko bistveno spremenijo pomen izjave.
Vrsta matematike, ki se najpogosteje uporablja za analizo jezika v formalni semantiki, je vtipkani lambda račun. Besede je mogoče identificirati kot različne spremenljivke in jih postaviti v enačbo; v teoriji predstavitve diskurza so te enačbe znane kot strukture predstavitve diskurza. Čeprav je predvsem jezikovna teorija, je formalna semantika multidisciplinarno področje. Vključeni so jezikoslovci, filozofi, logiki, matematiki in programerji. Analiza in ustvarjanje programskih jezikov ter celo preučevanje umetne inteligence lahko vključuje formalno semantiko.