A logikában és a matematikában a képlet egy objektumok véges sorozata, olyan tulajdonságokkal felruházva, amelyek lehetővé teszik a szintaxist ezekben a mezőkben.
Adott egy sor E és egy funkciója tömeg p: E → N , a képlet egy szót kivont E kapott a következő két építési szabályok:
Felismerjük azokat a "jelentős szavakat", amelyek az E-re épített szabad Lo (E) monoid részhalmazát alkotják .
Az itt bevezetett elméleti jelölés Łukasiewicz vagy „lengyel jelölés” néven ismert ; de az algebrában és az elemzésben általában használt jelölés az, hogy zárójelekkel t (F 2 , ...., F n ); ha t súlya 2, akkor tF 1 F 2 helyett (F 1 ) t (F 2 ) írunk , és
[r (F 1 , ...., F m )] t [s (G 1 , ...., G n )] helyett a TRF 1 .... F m sG 1 .... G n .
Ha egy F képletet adunk meg, az F bármelyik intervalluma, amely képlet, részképlet . Így, F 1 , rF 1 .... F m , SG 1 .... G n al-képletei TRF 1 .... F m sG 1 .... G n .
Ha F = tF 1 F 2 .... F n , az F i 1≤i≤n a közvetlen al-képletek F.
Bármely sor képletek, a bináris reláció „F egy al-formula G” egy érdekében vonatkozásában : reflexív , antiszimmetrikus és tranzitív .
Mindebből az következik, hogy a képlet részképleteinek előfordulására vonatkozó inklúziós összefüggés egy elágazó rend , vagyis szintaktikai fa , amelyben bármely elem esetében az előző elemek is összehasonlíthatók.
A képleteket egy formális nyelvhez viszonyítva határozzák meg , amely a függvényszimbólumok és a relációs szimbólumok állandó szimbólumainak gyűjteménye , ahol a függvények és relációk mindegyik szimbóluma olyan aritással rendelkezik, amely jelzi az általa alkalmazott argumentumok számát.
Aztán meg egy rekurzív távon a
Végül egy képlet a következő formák egyikét ölti fel:
Az első két esetet atomi képleteknek nevezzük .