Well-formed Formula - Predicate Logic

Predicate Logic

The definition of a formula in first-order logic is relative to the signature of the theory at hand. This signature specifies the constant symbols, relation symbols, and function symbols of the theory at hand, along with the arities of the function and relation symbols.

The definition of a formula comes in several parts. First, the set of terms is defined recursively. Terms, informally, are expressions that represent objects from the domain of discourse.

1. Any variable is a term.
2. Any constant symbol from the signature is a term
3. an expression of the form f(t₁,...,t_n), where f is an n-ary function symbol, and t₁,...,t_n are terms, is again a term.

The next step is to define the atomic formulas.

1. If t₁ and t₂ are terms then t₁=t₂ is an atomic formula
2. If R is an n-ary relation symbol, and t₁,...,t_n are terms, then R(t₁,...,t_n) is an atomic formula

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

1. is a formula when is a formula
2. and are formulas when and are formulas;
3. is a formula when is a variable and is a formula;
4. is a formula when 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, then it is called quantifier-free. An existential formula is a formula starting with a sequence of existential quantification followed by a quantifier-free formula.