8 Formula of the relational calculus

A well formed formula (abbreviated wff or just formula) of the relational calculus is a finite sequence of symbols from a given alphabet that is part of a formal language.

A term is either a literal (i.e. an expression denoting a value) or a variable.

An atomic formula or atom is a predicate symbol together with its arguments where each argument is a term, or it is an expression of the form t1=t2 where t1 and t2 are terms. An atomic formula is a formula that contains no logical connectives nor quantifiers.

For example P(x), Q(y,10) and R(z) are atoms.

A formula is defined inductively as follows:

• the truth constants ⊤ for "true" and ⊥ for "false" are formulas
• Each atom is a formula
• If φ is a formula, then ¬φ is a formula
• If φ and ψ are formulas, then (φ ∨ ψ), (φ ∧ ψ), (φ → ψ) and (φ ↔ ψ) are formulas
• If x is a variable and φ is a formula then ∃x φ is a formula
• If x is a variable and φ is a formula then ∀x φ is a formula

A closed formula, also ground formula or sentence, is a formula in which there are no free occurrences of any variable.