In mathematical logic, a formula is a type of abstract object a token of which is a symbol or string of symbols which may be interpreted as any meaningful unit (i.e. a name, an adjective, a proposition, a phrase, a string of names, a string of phrases, etcetera) in a formal language. Two different strings of symbols may be tokens of the same formula. It is not necessary for the existence of a formula that there be any tokens of it. The exact definition of a formula depends on the particular formal language in question.^[1]

A fairly typical definition (specific to first-order logic) goes as follows: Formulas are defined relative to a particular formal language and relation symbols, where each of the function and relation symbols comes supplied with an arity that indicates the number of arguments it takes.

Then a term is defined recursively as

1. A variable,
2. A constant, or
3. f(t₁,...,t_n), where f is an n-ary function symbol, and t₁,...,t_n are terms.

An atomic formula is one of the form:

1. t₁=t₂, where t₁ and t₂ are terms, or
2. R(t₁,...,t_n), where R is an n-ary relation symbol, and t₁,...,t_n are terms.

Finally, the set of formulae is defined to be the smallest set containing the set of atomic formulae such that the following holds:

1. \neg\phi is a formula when \ \phi is a formula;
2. (\phi \land \psi) and (\phi \lor \psi) are formulae when \ \phi and \ \psi are formulae;
3. \exists x\, \phi is a formula when x is a variable and \ \phi is a formula;
4. \forall x\, \phi is a formula when \ x is a variable and \ \phi is a formula (alternatively, \forall x\, \phi could be defined as an abbreviation for \neg\exists x\, \neg\phi).

If a formula has no occurrences of \exists x or \forall x, for any variable \ x, then it is called quantifier-free. An existential formula is a string of existential quantification followed by a quantifier-free formula.

See also

• Well-formed formula
• Theorem

References

ca:Fórmula cs:Formule (logika) es:Fórmula matemática fr:Formule (logique mathématique) ja:??? pl:Formu?a logiczna pt:Fórmula (lógica) ru:?????? ??????? zh:?? (????)