Atomic formula


In mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic. Compound formulas are formed by combining the atomic formulas using the logical connectives.
The precise form of atomic formulas depends on the logic under consideration; for propositional logic, for example, the atomic formulas are the propositional variables. For predicate logic, the atoms are predicate symbols together with their arguments, each argument being a term. In model theory, atomic formula are merely strings of symbols with a given signature, which may or may not be satisfiable with respect to a given model.

Atomic formula in first-order logic

The well-formed terms and propositions of ordinary first-order logic have the following syntax:
Terms:
that is, a term is recursively defined to be a constant c, or a variable x, or an n-ary function f whose arguments are terms tk. Functions map tuples of objects to objects.
Propositions:
that is, a proposition is recursively defined to be an n-ary predicate P whose arguments are terms tk, or an expression composed of logical connectives and quantifiers used with other propositions.
An atomic formula or atom is simply a predicate applied to a tuple of terms; that is, an atomic formula is a formula of the form P for P a predicate, and the tn terms.
All other well-formed formulae are obtained by composing atoms with logical connectives and quantifiers.
For example, the formula ∀x. P ∧ ∃y. Q ∨ ∃z. R contains the atoms
*