Formaalne semantika on lai lingvistiline teooria, mille eesmärk on uurida keele toimimist ja selle seost tegelikkusega. Keeleteadlased määratlevad hoolikalt iga väite tõesuse tingimused, mis on need olukorrad, mis peavad olema faktid, et lause oleks tõene. Seejärel transkribeeritakse laused matemaatilisteks võrranditeks, kasutades peamiselt trükitud lambda-arvutust.
Formaalse semantika teooria töötas esmakordselt välja Ameerika filosoof ja matemaatik Richard Montague 1960. aastatel. Tema konkreetne versioon on tuntud kui Montague Grammar. Sellest ajast alates on see teooria arenenud mitmes suunas, sealhulgas kategooriline grammatika, mille teerajajaks oli Yehoshua Bar-Hillel 1970. aastatel, ja liimi semantika, mille avaldas Mary Dalrymple 1990. aastatel.
Teise tüübi, diskursuse representatsiooni teooria, töötas 1981. aastal välja hollandi keeleteadlane Hans Kamp. Seda spetsiifilist keeleteooriat nimetatakse mõnikord üldmõiste formaalne semantika all. Diskursuse esituse teooria püüab analüüsida kogu diskursust või vestlust, mitte üksikuid lauseid, ja esitada seda matemaatiliste võrranditena.
Kõik formaalsemantika harud keskenduvad keele ja tegelikkuse suhetele; teisisõnu, nende eesmärk on leida seos öeldu ja selle vahel, mis on. Sõnu nimetatakse tähistajateks, asju endid aga denotaadiks või diskursuse esituse teoorias diskursuse referentideks. Lauses “koer haukus” on sõna “koer” tähistajaks, tegelik koer aga diskursuse referent.
Väitel võib olla rohkem kui üks tõesuse tingimus või nõue, et olla tõene. Sageli viivad need tõetingimused tagajärjeni, mida kasutatakse siis, kui ühe lause tõde nõuab, et teine oleks tõene. Teisisõnu, kui lause A on tõene, peab lause B olema ka kaasnevas olukorras tõene.
Väite tõesuse tingimuste kindlaksmääramiseks peavad keeleteadlased otsima olemasolevaid kvantoreid. Kvantori on sõna, mis näitab, kui palju asju on kaasatud, näiteks iga, iga, mis tahes ja mõned. Need sõnad võivad avalduse tähendust oluliselt muuta.
Formaalsemantikas keele analüüsimiseks kõige sagedamini kasutatav matemaatika tüüp on lambdaarvutus. Sõnu saab identifitseerida erinevate muutujatena ja asetada võrrandisse; diskursuse esituse teoorias on need võrrandid tuntud kui diskursuse esitusstruktuurid. Kuigi formaalne semantika on peamiselt keeleteooria, on see multidistsiplinaarne valdkond. Kaasatud on keeleteadlased, filosoofid, loogikud, matemaatikud ja programmeerijad. Programmeerimiskeelte analüüsimine ja loomine ning isegi tehisintellekti uurimine võib kõik hõlmata formaalset semantikat.