Atomic formula
In first-order logic, an atomic formula is the most basic well-formed formula, constructed by applying an n-ary predicate symbol to exactly n terms or by asserting equality between two terms.[1] Terms themselves are either constant symbols, variable symbols, or function symbols applied to appropriate numbers of terms, allowing atomic formulas to express simple assertions about objects in a domain, such as P(c, x) where P is a binary predicate, c a constant, and x a variable.[2] These formulas form the foundational building blocks from which all complex formulas are recursively built using logical connectives (like negation, conjunction, and disjunction) and quantifiers (universal and existential).[3] Atomic formulas play a central role in the syntax and semantics of first-order logic, enabling the precise formalization of mathematical and philosophical statements about relations and identities among entities.[4] For instance, in languages with equality, atomic formulas include expressions like t_1 = t_2, which denote that two terms refer to the same object, a feature essential for theories involving identity, such as those in set theory or arithmetic.[5] Unlike compound formulas, atomic formulas contain no nested structure beyond their constituent terms and lack free logical operators, making their truth values directly interpretable in models via assignments to predicates and interpretations of terms.[6] The concept of atomic formulas emerged in the development of modern logic during the late 19th and early 20th centuries, formalized by figures like Gottlob Frege and Bertrand Russell as part of efforts to rigorize mathematics, distinguishing first-order logic from propositional logic where "atomic" simply refers to indivisible propositional variables without terms or predicates.[7] This distinction underscores first-order logic's greater expressive power for quantifying over objects and relations, foundational to fields like model theory, automated theorem proving, and database query languages.[8]Fundamentals
Definition
In mathematical logic, an atomic formula is a well-formed formula (WFF) that contains no logical connectives, quantifiers, or subformulas, rendering it indivisible and serving as the fundamental building block for constructing more complex logical expressions.[9] This simplicity ensures that atomic formulas represent the most basic assertions or relations within a formal system, without internal decomposition into simpler components.[10] Unlike molecular or compound formulas, which arise from combining atomic formulas through operations such as conjunction (\wedge), disjunction (\vee), or negation (\neg), atomic formulas stand alone as primitive units.[10] This distinction underscores their role as the irreducible elements from which all other formulas are recursively built in logical languages.[9] The terminology "atomic" traces its origin to Bertrand Russell and Alfred North Whitehead's Principia Mathematica (1910–1913), where the authors employed the concept of "atomic propositions" to highlight their indecomposable structure in the foundations of mathematics and logic.[11] In the general syntax of formal languages, an atomic formula takes the form of either a propositional variable, as in propositional logic, or a predicate applied to terms, as in first-order logic.[9]Role in Logical Formulas
Atomic formulas constitute the foundational building blocks of logical systems, serving as the primitive units from which all compound formulas are constructed through the application of logical connectives in propositional logic and quantifiers in first-order extensions.[10] This base-level role ensures that complex expressions, such as implications or universal statements, ultimately reduce to combinations of these indivisible atoms, providing a structured hierarchy for logical reasoning.[9] The construction of logical formulas is defined inductively, with atomic formulas forming the initial case of the recursion. For instance, atomic propositions like p or q qualify as formulas, and if A and B are formulas, then expressions such as (A \land B) or \neg A are also formulas, built by applying connectives to prior levels.[10] This recursive process, often formalized through unique readability theorems, guarantees that every formula has a finite decomposition into atomic components, enabling precise syntactic parsing and manipulation in formal derivations.[12] In proof theory, atomic formulas are essential as the core propositions that are asserted, denied, or assumed in deductions, forming the basis for truth-functional composition via inference rules like modus ponens.[9] They represent the minimal units of assertion in axiomatic systems, where compound proofs emerge from applying connectives to these atoms, ensuring soundness and completeness in deriving theorems from premises.[12] Unlike compound formulas, which exhibit internal logical structure amenable to analysis through decomposition, atomic formulas have no deeper propositional content and cannot be further subdivided or examined for subcomponents.[13] Their simplicity allows direct evaluation via truth assignments or model interpretations, without recourse to connective-based reasoning.[10]Propositional Logic
Syntax of Atomic Formulas
In propositional logic, atomic formulas serve as the fundamental units from which all more complex expressions are constructed. These atomic formulas are simply propositional variables, typically denoted by lowercase letters such as p, q, r, possibly with subscripts (e.g., p_1, q_2) to distinguish multiple instances, drawn from a countable set of propositional symbols.[10][14] Unlike predicates in higher-order logics, propositional atomic formulas possess no internal structure, arguments, or dependencies on terms or functions; they stand alone as indivisible assertions that represent basic propositions without further decomposition.[10] This simplicity ensures that atomic formulas capture elementary statements, such as "it is raining" or "the switch is on," abstracted to symbolic form without embedding additional logical content.[15] Regarding well-formedness, any single propositional variable qualifies as a well-formed formula (WFF) in propositional logic, requiring no additional syntactic elements like parentheses or operators at this atomic level.[14] The syntax enforces this by defining the language's alphabet to include the set of propositional variables alongside logical connectives—such as negation (\neg), conjunction (\wedge), disjunction (\vee), implication (\rightarrow), and biconditional (\leftrightarrow)—and parentheses for delimiting compound expressions.[10][15] These connectives enable the combination of atomic formulas into larger well-formed structures, bridging to the formation of complex logical expressions.Semantics and Truth Values
In propositional logic, the semantics of atomic formulas centers on their assignment of truth values through valuations, which provide the interpretive framework for evaluating formulas. A valuation, also known as a truth assignment or interpretation, is a function that maps each propositional variable (atomic formula) to a truth value from the set {T, F}, where T denotes true and F denotes false.[16][17] This mapping ensures that the semantics of atomic formulas are fully determined by the valuation, with no additional structure required beyond the variable's identity.[18] Classical propositional logic adheres to bivalent semantics, meaning every atomic formula receives exactly one of two truth values under any given valuation, establishing a binary foundation for logical evaluation.[18][16] These assignments form the basis for assessing compound formulas, as the truth value of more complex expressions is computed recursively from the atomic components using the semantics of connectives like conjunction, disjunction, and negation.[16] Atomic formulas carry no inherent semantic content; their truth values depend solely on the arbitrary assignment in the valuation, allowing for flexible interpretations across different contexts.[17][18] The set of all possible valuations for a language with n distinct atomic formulas comprises 2n elements, each representing a unique combination of truth assignments and serving as the rows in a truth table to exhaustively determine a formula's behavior.[16][18] For instance, with atomic formulas p and q, the four possible valuations are:- v(p) = T, v(q) = T
- v(p) = T, v(q) = F
- v(p) = F, v(q) = T
- v(p) = F, v(q) = F
First-Order Logic
Terms and Predicates
In first-order logic, the construction of atomic formulas relies on two fundamental components: terms and predicates, which together with the signature of the language define the basic expressive vocabulary. The signature is a collection of constant symbols, function symbols, and predicate symbols, where each non-constant symbol is assigned a fixed arity indicating the number of arguments it accepts.[8] Terms represent objects or expressions denoting potential elements of the domain and are defined inductively. The base cases consist of constant symbols (e.g., a, b), which denote specific individuals, and variable symbols (e.g., x, y), which act as placeholders for arbitrary domain elements.[8] More complex terms are formed by applying function symbols to sequences of existing terms; for an n-ary function symbol f, the expression f(t_1, \dots, t_n) qualifies as a term if each t_i is itself a term.[8] This inductive process ensures that terms can nest arbitrarily to express composite denotations. Predicates, or relation symbols, capture properties of or relations among domain elements and are also specified by arity in the signature. An n-place predicate symbol P of arity n denotes an n-ary relation, such as a unary predicate for a property of single elements or a binary predicate for a relation between pairs of elements.[8] These symbols provide the relational structure essential for expressing factual assertions in the language. Within terms used in atomic formulas, all variables are free, meaning they are unbound and range over the entire domain without restriction from quantifiers at this syntactic level.[8] Propositional atomic formulas represent a simplified case, akin to 0-ary predicates without terms.[9]Structure of Atomic Formulas
In first-order logic, an atomic formula is formed by applying an n-ary predicate symbol P to a sequence of n terms t_1, \dots, t_n, denoted as P(t_1, \dots, t_n), where the terms are constructed from constants, variables, and function applications as detailed in the prior section on terms and predicates.[19][20] Equality is also considered an atomic formula in the form t_1 = t_2, treating = as a binary predicate.[19] Atomic formulas contain no logical connectives or quantifiers, ensuring their simplicity as the basic propositional units from which complex formulas are built; for instance, Loves(John, Mary) asserts a binary relation where Loves is the predicate symbol and John, Mary are constant terms.[20][19] All variable occurrences within an atomic formula are free, as there are no binding mechanisms like quantifiers to restrict their scope.[19] The syntactic structure can be formalized using a BNF-like grammar:where P is an n-ary predicate symbol and each term_i is a term.[20][19]atom ::= P(term_1, ..., term_n) | term_1 = term_2atom ::= P(term_1, ..., term_n) | term_1 = term_2