Well-formed formula

In

The abbreviation wff is pronounced "woof", or sometimes "wiff", "weff", or "whiff". [12]

A formal language can be identified with the set of formulas in the language. A formula is a

The formulas of propositional calculus, also called propositional formulas,^[14] are expressions such as ${\displaystyle (A\land (B\lor C))}$. Their definition begins with the arbitrary choice of a set V of propositional variables. The alphabet consists of the letters in V along with the symbols for the propositional connectives and parentheses "(" and ")", all of which are assumed to not be in V. The formulas will be certain expressions (that is, strings of symbols) over this alphabet.

The formulas are

• Each propositional variable is, on its own, a formula.
• If φ is a formula, then ¬φ is a formula.
• If φ and ψ are formulas, and • is any binary connective, then ( φ • ψ) is a formula. Here • could be (but is not limited to) the usual operators ∨, ∧, →, or ↔.

This definition can also be written as a formal grammar in Backus–Naur form, provided the set of variables is finite:

<alpha set> ::= p | q | r | s | t | u | ... (the arbitrary finite set of propositional variables)
<form> ::= <alpha set> | ¬<form> | (<form>∧<form>) | (<form>∨<form>) | (<form>→<form>) | (<form>↔<form>)

Using this grammar, the sequence of symbols

(((p → q) ∧ (r → s)) ∨ (¬q ∧ ¬s))

is a formula, because it is grammatically correct. The sequence of symbols

((p → q)→(qq))p))

is not a formula, because it does not conform to the grammar.

A complex formula may be difficult to read, owing to, for example, the proliferation of parentheses. To alleviate this last phenomenon, precedence rules (akin to the

(((p → q) ∧ (r → s)) ∨ (¬q ∧ ¬s))

may be abbreviated as

p → q ∧ r → s ∨ ¬q ∧ ¬s

This is, however, only a convention used to simplify the written representation of a formula. If the precedence was assumed, for example, to be left-right associative, in following order: 1. ¬   2. ∧  3. ∨  4. →, then the same formula above (without parentheses) would be rewritten as

(p → (q ∧ r)) → (s ∨ (¬q ∧ ¬s))

The definition of a formula in first-order logic ${\displaystyle {\mathcal {QS}}}$ is relative to the

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 predicate 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. ${\displaystyle \neg \phi }$ is a formula when ${\displaystyle \phi }$ is a formula
2. ${\displaystyle (\phi \land \psi )}$ and ${\displaystyle (\phi \lor \psi )}$ are formulas when ${\displaystyle \phi }$ and ${\displaystyle \psi }$ are formulas;
3. ${\displaystyle \exists x\,\phi }$ is a formula when ${\displaystyle x}$ is a variable and ${\displaystyle \phi }$ is a formula;
4. ${\displaystyle \forall x\,\phi }$ is a formula when ${\displaystyle x}$ is a variable and ${\displaystyle \phi }$ is a formula (alternatively, ${\displaystyle \forall x\,\phi }$ could be defined as an abbreviation for ${\displaystyle \neg \exists x\,\neg \phi }$).

If a formula has no occurrences of ${\displaystyle \exists x}$ or ${\displaystyle \forall x}$, for any variable ${\displaystyle x}$, 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.

An atomic formula is a formula that contains no

According to some terminology, an open formula is formed by combining atomic formulas using only logical connectives, to the exclusion of quantifiers.^[15] This is not to be confused with a formula which is not closed.

A closed formula, also