Le formule ben formate sono le espressioni sulle
quali è possibile applicare la funzione di verità -
informalmente parlando, si può dire che sono le "frasi" che la logica
esamina.
Solitamente esse sono definite attraverso una
grammatica context-free, ma niente impedisce in linea
teorica di utilizzare altre tecniche. In teoria, sarebbe addirittura concepibile una logica
il cui insieme di formule ben formate sia indecidibile.
Naturalmente, in pratica una logica siffatta sarebbe
estremamente scomoda, e per buona parte delle logiche si richiede che il
problema del riconoscimento delle formule ben formate ammetta soluzione,
pertanto il più delle volte l'insieme delle fbf sarà definito attraverso una
grammatica context-free o (raramente) attraverso metodi
equivalenti.