Atomic formula

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 formulas 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[]

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

Terms:

$t\equiv c\mid x\mid f(t_{1},\dotsc ,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 t_k. Functions map tuples of objects to objects.

Propositions:

$A,B,...\equiv P(t_{1},\dotsc ,t_{n})\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)$

References[]

^ Wilfrid Hodges (1997). A Shorter Model Theory. Cambridge University Press. pp. 11–14. ISBN 0-521-58713-1.

v t Mathematical logic
General	Formal proof Formal semantics Set Element Class Classical logic Axiom Rule of inference Theorem Logical consequence Type theory Theory
Syntax & Language	Alphabet Arity Expression Ground Relation Formal Grammar Language Proof System Theory Formation rule Formula Atomic Open Free/bound variable Logical connective ¬ ∨ ∧ → ↔ = Predicate Functional Variable Propositional variable Quantifier ∃ ∀ Sentence Atomic Signature String Substitution Symbol Function Logical/Constant Non-logical Variable Term
Systems	Formal system Deductive system Axiomatic system Hilbert style systems Natural deduction Sequent calculus
Traditional logic	Proposition Inference Logical equivalence Argument Validity Syllogism Square of opposition Venn diagram
Propositional calculus and Boolean logic	Boolean functions Propositional calculus Propositional formula Logical connectives Truth tables Many-valued logic
Predicate logic	First-order Quantifiers Predicate Second-order Monadic predicate calculus
Naive set theory	Set Empty set Element Enumeration Extensionality Finite set Infinite set Inhabited set Subset Power set Countable set Uncountable set Recursive set Domain Codomain Image Map Function Relation Ordered pair
Set theory	Foundations of mathematics Zermelo–Fraenkel set theory Axiom of choice General set theory Kripke–Platek set theory Von Neumann–Bernays–Gödel set theory Morse–Kelley set theory Tarski–Grothendieck set theory
Model theory	Model Interpretation Non-standard model Finite model theory Strength Truth value Validity
Proof theory	Formal proof Deductive system Formal system Theorem Logical consequence Rule of inference Syntax
Computability theory	Recursion Computable set Computably enumerable Decision problem Church–Turing thesis Computable function Primitive recursive function

Atomic formula

Contents

Atomic formula in first-order logic[]

See also[]

References[]

Further reading[]