Alògica matemàtica, una fórmula ben formada, també anomenada paraula, expressió o fórmula, i sovint abreujada fbf, és unacadena de caràcters generada segons unagramàtica formal a partir d'unalfabet donat. Unllenguatge 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 lalògica formal, lesdemostracions 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 diuteorema quan té un paper important en la teoria sent desenvolupada, olema quan té un paper accessori en la demostració d'un teorema.