atomic formula

In mathematical logic, an atomic formula (also known as an atom or a prime 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, a propositional variable is often more briefly referred to as an "atomic formula", but, more precisely, a propositional variable is not an atomic formula but a formal expression that denotes an atomic formula. For predicate logic, the atoms are predicate symbols together with their arguments, each argument being a term. In model theory, atomic formulas 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:
* $t \equiv c \mid x \mid f (t_,\dotsc, t_)$,

that is, a term is recursively defined to be a constant ''c'' (a named object from the domain of discourse), or a variable ''x'' (ranging over the objects in the domain of discourse), or an ''n''-ary function ''f'' whose arguments are terms ''t''_''k''. Functions map tuples of objects to objects.

Propositions:
* $A, B, ... \equiv P (t_,\dotsc, t_) \mid A \wedge B \mid \top \mid A \vee B \mid \bot \mid A \supset B \mid \forall x.\ A \mid \exists x.\ A$,

that is, a proposition is recursively defined to be an ''n''-ary predicate ''P'' whose arguments are terms ''t''_''k'', or an expression composed of logical connectives (and, or) and quantifiers (for-all, there-exists) 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'' (''t''₁ ,…, ''t''_''n'') for ''P'' a predicate, and the ''t''_''n'' terms.

All other well-formed formulae are obtained by composing atoms with logical connectives and quantifiers.

For example, the formula ∀''x. P'' (''x'') ∧ ∃''y. Q'' (''y'', ''f'' (''x'')) ∨ ∃''z. R'' (''z'') contains the atoms
* $P (x)$
* $Q (y, f (x))$
* $R (z)$.
As there are no quantifiers appearing in an atomic formula, all occurrences of variable symbols in an atomic formula are free.W. V. O. Quine, ''Mathematical Logic'' (1981), p.161. Harvard University Press, 0-674-55451-5

See also

* In model theory, structures assign an interpretation to the atomic formulas.
* In proof theory, polarity assignment for atomic formulas is an essential component of focusing.
* Atomic sentence

References

Further reading

*

{{Mathematical logic

Predicate logic
Logical expressions

de:Aussage (Logik)#einfache Aussagen - zusammengesetzte Aussagen