---
tag: D039R5C8TC
kind: statement
role: proposition
name: Atomic formula in first-order logic
sources:
  - wikipedia: en:4472066@r1317547099
    locator: Atomic formula, section Atomic formula in first-order logic
    note: adopted
    mention: wikipedia://en/4472066#VIWL
    sections: [Statement]
inventory: [7NDQWKWMHG]
---

## Statement

The well-formed terms and propositions of ordinary [[first-order logic|086QKPF0A6]] 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*<sub>*k*</sub>. 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*<sub>*k*</sub>, or an expression composed of logical connectives (and, or) and [[quantifiers|0FYQMKFE77]] (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*<sub>1</sub> ,…, *t*<sub>*n*</sub>) for *P* a predicate, and the *t*<sub>*n*</sub> terms.

All other well-formed formulas 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.