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:

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