Editing First-order logic (section)

====Formulas====
The set of ''[[formula (mathematical logic)|formulas]]'' (also called ''[[Well-formed formula|well-formed formulas]]''<ref>Some authors who use the term "well-formed formula" use "formula" to mean any string of symbols from the alphabet. However, most authors in mathematical logic use "formula" to mean "well-formed formula" and have no term for non-well-formed formulas. In every context, it is only the well-formed formulas that are of interest.</ref> or ''WFFs'') is inductively defined by the following rules:
# ''Predicate symbols''. If ''P'' is an ''n''-ary predicate symbol and ''t''<sub>1</sub>, ..., ''t''<sub>''n''</sub> are terms then ''P''(''t''<sub>1</sub>,...,''t''<sub>''n''</sub>) is a formula.
# ''[[logical equality|Equality]]''. If the equality symbol is considered part of logic, and ''t''<sub>1</sub> and ''t''<sub>2</sub> are terms, then ''t''<sub>1</sub> = ''t''<sub>2</sub> is a formula.
# ''Negation''. If <math>\varphi</math> is a formula, then <math>\lnot\varphi</math> is a formula.
# ''Binary connectives''. If {{tmath|\varphi}} and {{tmath|\psi}} are formulas, then (<math>\varphi\rightarrow\psi</math>) is a formula. Similar rules apply to other binary logical connectives.
# ''Quantifiers''. If <math>\varphi</math>  is a formula and ''x'' is a variable, then <math>\forall x \varphi</math> (for all x, <math>\varphi</math> holds) and <math>\exists x \varphi</math> (there exists x such that <math>\varphi</math>) are formulas.
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 formula]]s''.

For example:
:<math>\forall x \forall y (P(f(x)) \rightarrow\neg (P(x) \rightarrow Q(f(y),x,z)))</math>
is a formula, if ''f'' is a unary function symbol, ''P'' a unary predicate symbol, and Q a ternary predicate symbol. However, <math>\forall x\, x \rightarrow</math> 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.