Semantica formală este o teorie lingvistică largă, menită să studieze modul în care funcționează limbajul și relația sa cu realitatea. Lingviștii definesc cu atenție condițiile de adevăr ale fiecărei afirmații, care sunt acele situații care trebuie să fie fapte pentru ca propoziția să fie adevărată. Propozițiile sunt apoi transcrise în ecuații matematice, utilizând în primul rând calculul lambda tipizat.
Teoria semanticii formale a fost dezvoltată pentru prima dată de filozoful și matematicianul american Richard Montague în anii 1960. Versiunea lui specifică este cunoscută sub numele de Gramatică Montague. De atunci, această teorie s-a dezvoltat în multe direcții, inclusiv gramatica categorică, așa cum a fost lansată de Yehoshua Bar-Hillel în anii 1970, și semantica Glue, publicată de Mary Dalrymple în anii 1990.
Un alt tip, teoria reprezentării discursului, a fost dezvoltată în 1981 de lingvistul olandez Hans Kamp. Această teorie lingvistică specifică este uneori menționată sub termenul generic semantică formală. Teoria reprezentării discursului încearcă să analizeze întregul discurs, sau conversația, mai degrabă decât propoziții izolate, și să o prezinte în ecuații matematice.
Toate ramurile semanticii formale se concentrează pe relația dintre limbaj și realitate; cu alte cuvinte, scopul lor este să găsească legătura dintre ceea ce se spune și ceea ce este. Cuvintele sunt denumite semnificanți, în timp ce lucrurile în sine sunt numite denotata sau, în teoria reprezentării discursului, referenți de discurs. În propoziția „Câinele a lătrat”, cuvântul „câine” este un semnificant, în timp ce câinele propriu-zis este un referent de discurs.
O afirmație poate avea mai mult de o condiție de adevăr sau o cerință pentru a fi adevărată. Adesea, aceste condiții de adevăr duc la implicare, care este termenul folosit atunci când adevărul unei propoziții cere ca alta să fie adevărată. Cu alte cuvinte, într-o situație implicată, dacă propoziția A este adevărată, atunci propoziția B trebuie să fie și ea adevărată.
Pentru a determina condițiile de adevăr ale unei afirmații, lingviștii trebuie să caute orice cuantificatori prezenți. Un cuantificator este un cuvânt care indică câte lucruri sunt implicate, cum ar fi fiecare, fiecare, oricare și unele. Aceste cuvinte pot schimba în mod substanțial sensul unei afirmații.
Tipul de matematică cel mai des folosit pentru a analiza limbajul în semantica formală este calculul lambda tipizat. Cuvintele pot fi identificate ca variabile diferite și plasate într-o ecuație; în teoria reprezentării discursului, aceste ecuații sunt cunoscute ca structuri de reprezentare a discursului. Deși în primul rând o teorie lingvistică, semantica formală este un domeniu multidisciplinar. Sunt implicați lingviști, filozofi, logicieni, matematicieni și programatori. Analiza și crearea limbajelor de programare și chiar studiul inteligenței artificiale pot implica toate semantica formală.