In mathematical logic, a well-formed formula (often abbreviated WFF, pronounced "wiff") is a symbol or string of symbols (a formula) that is generated by the formal grammar of a formal language. To say that a string S is a WFF with respect to a given formal grammar G is equivalent to saying that S belongs to the language generated by G, i.e. S ∈ L(G). A formal language can be identified with the set of its WFFs.
In formal logic, proofs are sequences of WFFs with certain properties, and the final WFF in the sequence is what is proven. This final WFF is called a theorem when it plays a significant role in the theory being developed, or a lemma when it plays an accessory role in the proof of a theorem.
Reference:
http://en.wikipedia.org/wiki/Well-formed_formula
