In mathematical logic, a formula is a formal syntactic object that expresses a proposition. Mathematical logic is a major area of mathematics, which grew out of symbolic logic. ... This article is about the word proposition as it is used in logic, philosophy, and linguistics. ...

The exact definition of a formula depends on the particular development of formal logic in question, but a fairly typical one (specific to first-order logic) goes as follows: Formulas are defined relative to a particular language, which consists of a collection of variables, constants, logic symbols, function symbols, and relation symbols, where each of the function and relation symbols comes supplied with an arity that indicates the number of arguments it takes. First-order logic (FOL) is a universal language in symbolic science, and is in use everyday by mathematicians, philosophers, linguists, computer scientists and practitioners of artificial intelligence. ... The mathematical term arity sprang from words like unary, binary, ternary, etc. ...

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: In mathematical logic, an atomic formula or atom is a formula with no underlying propositional structure. ...

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. is a formula when φ is a formula;
2. and are formulae when φ and ψ are formulae;
3. is a formula when x is a variable and φ is a formula;
4. is a formula when x is a variable and φ is a formula (alternatively, could be defined as an abbreviation for ).

If a formula has no occurrences of or , 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

• WFF

In logic, WFF is an abbreviation for well-formed formula. ...

References

Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-568-81262-0.