În logică și matematică , o formulă este o serie finită de obiecte, dotate cu proprietăți particulare care fac posibilă sintaxa în toate aceste câmpuri.
Având în vedere un set E și o funcție de greutate p: E → N , o formulă este un cuvânt extras din E obținut prin următoarele două reguli de construcție:
Recunoaștem „cuvintele semnificative” care formează un subset al monoidului liber Lo (E) construit pe E.
Notația teoretică introdusă aici este cea cunoscută sub numele de Łukasiewicz sau „notația poloneză”; dar notația folosită în mod obișnuit în algebră și în analiză este cea cu paranteze t (F 2 , ...., F n ); dacă t are greutatea 2, scriem (F 1 ) t (F 2 ) în loc de tF 1 F 2 și
[r (F 1 , ...., F m )] t [s (G 1 , ...., G n )] în loc de trF 1 .... F m sG 1 .... G n .
Dat fiind o formulă F, orice interval de F care este o formulă este o sub-formulă . Astfel, F 1 , rF 1 .... F m , sG 1 .... G n sunt sub-formule ale trF 1 .... F m sG 1 .... G n .
Dacă F = tF 1 F 2 .... F n , F i 1≤i≤n sunt sub-formulele imediate ale lui F.
În orice set de formule, relația binară "F este o sub-formulă a lui G" este o relație de ordine : reflexivă , antisimetrică și tranzitivă .
Din toate acestea rezultă că relația de incluziune asupra aparițiilor sub-formulelor unei formule este o ordine ramificată sau arborele sintactic , în care, pentru orice element, elementele anterioare sunt toate comparabile.
Formulele sunt definite în raport cu un limbaj formal , care este o colecție de simboluri constante ale simbolurilor funcției și ale simbolurilor relației , în care fiecare dintre simbolurile funcțiilor și relației vine cu o aritate care indică numărul de argumente pe care le ia.
Apoi definim recursiv un termen ca
În cele din urmă, o formulă ia una dintre următoarele forme:
Primele două cazuri se numesc formule atomice .