A formula in logic is generally a set of one or more propositional variables, or predicate symbols, and operators.

In any system of logic, the notion of what counts as a formula must be defined. For instance, in propositional logic, the rules for what counts as a formula are generally:

Any propositional variable is itself a formula. (So, P is a formula).

If φ and ρ are formulae, then so are:

¬φ

(φ ∧ ρ)

(φ ∨ ρ)

(φ → ρ)

(φ ↔ ρ)

All expressions that can be formulated from a finite number of applications of rules (1) and (2) are also formulae.

Rule (2) may be extended or reduced in logical systems that include a different set of operators.

Rule (3) is said to be schematic — that is, it is applied recursively and applies to any possible formula. So, if α is a formula, then (α → β) is a formula, and so too is ((α → β) ∧ γ).

In first- and second-order logics, additional rules are added to handle the quantification of object variables or predicate symbols.

On this site, formulae are represented by lowercase Greek letters, α, β, γ, δ … ω — this is to differentiate them from propositional variables. For example, α is used schematically to represent any formula, whereas (P ∨ Q) is a specific formula.

The world formula may be pluralized as either formulas or formulae. This site usually uses the term formulae.

Well-formed formulae

A formula is said to be well-formed when it is constructed according to the rules of well-formation, containing the proper number of parentheses and order of operations, without ambiguity.

For example, the string “α ↔ β ∧ γ” is not a well-formed formula, because the operations are not grouped. Note that there are two possible readings of this string. First, it could mean “alpha, if and only if both beta and gamma” or (α ↔ (β ∧ γ)). Alternatively, it could be read, “Both alpha, if and only if beta, and gamma.” ((α ↔ β) ∧ γ).

Because there is no ambiguity between ¬P and (¬P), there are generally no parentheses used in unary operations, such as negation. Also, when a formula contains a binary operation, the outermost set of parentheses is often left out, unless it is confusing to do so. For example, (α ∧ β) and (φ → (ρ ∨ ψ)) can be rendered as α ∧ β and φ → (ρ ∨ ψ) and retain the status of well-formation.

Finally, it can also be noted that with the operators ∧ and ∨, the order of operations is irrelevant. That is, formulas like (α ∧ (β ∧ γ)) and ((α ∧ β) ∧ γ) are equivalent. As such, the formula can sometimes be written as (α ∧ β ∧ γ), and be interpreted as either of the well-formed versions.

Sets of formulae

Uppercase Greek letters, beginning with Γ (Gamma), are conventionally used on this site to signify sets of formulas. (These sets will be defined when used.) For example, we may define a set as Γ = { α → β, α ∨ φ, ¬φ } and later refer to the set by Γ.