Inmathematical logic, anatomic formula (also known as anatom or aprime formula) is aformula with no deeperpropositional structure, that is, a formula that contains nological connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplestwell-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; forpropositional logic, for example, apropositional 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. Forpredicate logic, the atoms are predicate symbols together with their arguments, each argument being aterm. Inmodel theory, atomic formulas are merelystrings of symbols with a givensignature, which may or may not besatisfiable with respect to a given model.^[1]

The well-formed terms and propositions of ordinaryfirst-order logic have the followingsyntax:

Terms:

• ${\displaystyle t\equiv c\mid x\mid f(t_1,\dots ,t_n)}$,

that is, a term isrecursively defined to be a constantc (a named object from thedomain of discourse), or a variablex (ranging over the objects in the domain of discourse), or ann-ary functionf whose arguments are termst_k. Functions maptuples of objects to objects.

Propositions:

• ${\displaystyle A,B,...\equiv P(t_1,\dots ,t_n)\mid A\wedge B\mid \mathrm{\top }\mid A\vee B\mid \mathrm{\perp }\mid A\supset B\mid \mathrm{\forall }x.A\mid \mathrm{\exists }x.A}$,

that is, a proposition is recursively defined to be ann-arypredicateP whose arguments are termst_k, or an expression composed oflogical connectives (and, or) andquantifiers (for-all, there-exists) used with other propositions.

Anatomic formula oratom is simply a predicate applied to a tuple of terms; that is, an atomic formula is a formula of the formP (t₁ ,…,t_n) forP a predicate, and thet_n 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

• ${\displaystyle P(x)}$
• ${\displaystyle Q(y,f(x))}$
• ${\displaystyle R(z)}$.

As there are no quantifiers appearing in an atomic formula, all occurrences of variable symbols in an atomic formula are free.^[2]

• Inmodel theory,structures assign an interpretation to the atomic formulas.
• Inproof theory,polarity assignment for atomic formulas is an essential component offocusing.
• Atomic sentence

• Hinman, P. (2005).Fundamentals of Mathematical Logic. A K Peters.ISBN 1-56881-262-0.

• Predicate logic
• Logical expressions

• Articles with short description
• Short description matches Wikidata