Atomic formula

From Wikipedia, the free encyclopedia
Jump to: navigation, search

In mathematical logic, an atomic formula (also known simply as an atom) 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.[1]

Atomic formula in first-order logic[edit]

The well-formed terms and propositions of ordinary first-order logic have the following syntax:

Terms:

  • t \equiv c \ | \  x \ | \  f (t_{1}, ..., t_{n}),

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 tk. Functions map tuples of objects to objects.

Propositions:

  • A, B, ... \equiv P (t_{1}, ..., t_{n}) \ | \  A \wedge B \ | \top | \ A \vee B \  | \perp | \ A \supset B \ | \ \forall x. A \ | \ \exists x. \ A ,

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, 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 (t1, …, tn) for P a predicate, and the tk 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)

When all of the terms in an atom are ground terms, then the atom is called a ground atom or ground predicate.

See also[edit]

References[edit]

  1. ^ Wilfrid Hodges (1997). A Shorter Model Theory. Cambridge University Press. pp. 11–14. ISBN 0-521-58713-1. 
  • Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.