[1] The abbreviation wff is pronounced "woof", or sometimes "wiff", "weff", or "whiff".
Although the term "formula" may be used for written marks (for instance, on a piece of paper or chalkboard), it is more precisely understood as the sequence of symbols being expressed, with the marks being a token instance of formula.
This distinction between the vague notion of "property" and the inductively-defined notion of well-formed formula has roots in Weyl's 1910 paper "Uber die Definitionen der mathematischen Grundbegriffe".
Their definition begins with the arbitrary choice of a set V of propositional variables.
The alphabet consists of the letters in V along with the symbols for the propositional connectives and parentheses "(" and ")", all of which are assumed to not be in V. The formulas will be certain expressions (that is, strings of symbols) over this alphabet.
The formulas are inductively defined as follows: This definition can also be written as a formal grammar in Backus–Naur form, provided the set of variables is finite: Using this grammar, the sequence of symbols is a formula, because it is grammatically correct.
A complex formula may be difficult to read, owing to, for example, the proliferation of parentheses.
Terms, informally, are expressions that represent objects from the domain of discourse.
The precise form of atomic formulas depends on the formal system under consideration; for propositional logic, for example, the atomic formulas are the propositional variables.
If A is a formula of a first-order language in which the variables v1, …, vn have free occurrences, then A preceded by ∀v1 ⋯ ∀vn is a universal closure of A.
[17][18][19][20] Modern usages (especially in the context of computer science with mathematical software such as model checkers, automated theorem provers, interactive theorem provers) tend to retain of the notion of formula only the algebraic concept and to leave the question of well-formedness, i.e. of the concrete string representation of formulas (using this or that symbol for connectives and quantifiers, using this or that parenthesizing convention, using Polish or infix notation, etc.)
The expression "well-formed formulas" (WFF) also crept into popular culture.
WFF is part of an esoteric pun used in the name of the academic game "WFF 'N PROOF: The Game of Modern Logic", by Layman Allen,[21] developed while he was at Yale Law School (he was later a professor at the University of Michigan).
The suite of games is designed to teach the principles of symbolic logic to children (in Polish notation).