{{Revisarrevisar Tradtraducción}} En la [[lógica matemática]], una '''fórmula bien formulada''' (a menudo abreviado a FBF) es un símbolo o una serie de síbolos (una [[Fórmula_matemáticaFórmula matemática|fórmula]]) que es generada por la [[gramática formal]] de un [[lenguaje formal]]. Decir que una serie <math>\ S</math> es una FBF con respecto a una gramática formal dada <math>\ G</math> es igual que decir que <math>\ S</math> pertenece al lenguaje generado por <math>\ G</math>, i. e. <math>S \in \boldsymbol{L}(G)</math>. Un lenguaje formal se puede identificarse con la serie de sus FBFs.
En la [[lógica formal]], las [[demostración_matemáticademostración matemática|demostraciones]] son secuencias de FBFs con ciertas propiedades, y la final FBF en la secuencia es lo que se demuestre. Esta FBF final se llama un [[teorema]] cuando juega un papel significante en la teoría siendo desarrollada, o una [[lema]] cuando juega un papel accesorio en la demostración de una teorema.
