structural:scholar_edition
Formulas

The set of formulas (also called well-formed formulas or WFFs) is inductively defined by the following rules:

Only expressions which can be obtained by finitely many applications of rules 1–5 are formulas. The formulas obtained from the first two rules are said to be atomic formulas.

For example:

is a formula, if f is a unary function symbol, P a unary predicate symbol, and Q a ternary predicate symbol. However, ∀ x x → {\displaystyle \forall x\,x\rightarrow } is not a formula, although it is a string of symbols from the alphabet.

The role of the parentheses in the definition is to ensure that any formula can only be obtained in one way—by following the inductive definition (i.e., there is a unique parse tree for each formula). This property is known as unique readability of formulas. There are many conventions for where parentheses are used in formulas. For example, some authors use colons or full stops instead of parentheses, or change the places in which parentheses are inserted. Each author's particular definition must be accompanied by a proof of unique readability.