Fórmula ben formada
A lògica matemàtica, una fórmula ben formada , també anomenada paraula , expressió o fórmula , i sovint abreujada fbf , és una cadena de caràcters generada segons una gramàtica formal a partir d'un alfabet donat. Un llenguatge formal es defineix com el conjunt de totes les seves fórmules ben formades.
Per exemple, un alfabet podria ser el conjunt{ a , b }, i una gramàtica podria definir a les fórmules ben formades com aquelles cadenes que tenen el mateix nombre de caràcters a que b . Llavors, algunes fórmules ben formades del llenguatge serien: ab , ba , abab , ababba , etc. El llenguatge formal seria el conjunt de totes aquestes fórmules ben formades.
A la lògica formal, les demostracions són seqüències de fórmules ben formades amb certes propietats, on la darrera fórmula de la seqüència és allò que es demostra. Aquesta fórmula final es diu teorema quan té un paper important en la teoria sent desenvolupada, o lema quan té un paper accessori en la demostració d'un teorema.