A formula that contains no logical connectives (such as ∧, ∨, →, ¬) and no quantifiers; in first-order logic an atomic formula (atom) is typically a predicate symbol applied to a tuple of terms (including equality atoms), serving as the indivisible building block of complex formulas.

Principle

Atomic formulas represent elementary assertions about terms; complex sentences are formed by combining atoms with logical connectives and quantifiers, and many proof systems reduce reasoning to manipulations of atoms (e.g., resolution works on clauses built from atoms and their negations).

Demonstration

In first-order arithmetic, expressions like P(a,b) or x = y (once variables are instantiated) are atomic formulas; contrast P(a) ∧ Q(a) which is not atomic because it combines two atoms with a connective.

Misapplication

Treating a compound sentence such as R(x) ∨ S(y) or a quantified expression ∀x P(x) as atomic in procedures that require atoms (for instance, feeding a non-atomic formula into an algorithm that expects ground atoms leads to errors).

Consequence

Atoms provide the base elements for syntactic normal forms (conjunctive/disjunctive normal form, clauses) and for automated reasoning: identifying and manipulating atoms is crucial to unification, resolution, model building, and tableau methods.

Reversal

A molecular formula is the inversion: any formula constructed by applying connectives or quantifiers to atoms, whose meaning depends on composition and whose logical behaviour cannot be reduced to a single predicate application.

Boundary

In propositional logic atomic formulas are propositional variables; in first-order logic atoms include predicate applications and equality; some extended logics add built-in connectives or higher-order atoms, which changes what is considered atomic.

Semantic Tension

Tension arises between 'atomic formula' and 'atomic sentence' (the former may contain free variables while the latter is closed), and between ground atoms (no variables) used in model checking and general atoms used in proof calculi.

Synthesis

An atomic formula is the irreducible assertion in a logical language: a predicate (or equality) applied to terms, forming the basis from which complex formulas, normal forms, and automated reasoning procedures are constructed.