Fact-checked by Grok 2 weeks ago

First-order logic

First-order logic, also known as first-order predicate logic, is a that extends propositional logic by allowing quantification over individual objects in a , enabling the expression of statements about properties, relations, and functions involving those objects. It serves as a foundational in , , and for rigorously analyzing and modeling complex structures. The system's syntax includes constants, variables, predicates, functions, logical connectives (such as , , disjunction, and ), and quantifiers (∀ for "for all" and ∃ for "there exists"), which together form well-formed formulas that can be either open (with free variables) or closed (sentences without free variables). Semantics are provided by structures consisting of a non-empty and interpretations for the non-logical symbols, determining whether a formula is true or false relative to an assignment of values to variables. The development of first-order logic emerged in the late 19th and early 20th centuries as part of efforts to formalize the foundations of , particularly in addressing ambiguities in and exploring the logical structure of arithmetic and . Key contributions include Gottlob Frege's 1879 , which introduced predicate calculus and quantifiers, and subsequent refinements by and in (1910–1913), which aimed to derive all of from logical axioms. In 1929, proved the , establishing that every semantically valid formula in first-order logic is provable within a suitable , linking syntax and semantics tightly. However, and independently demonstrated in 1936 that first-order logic is undecidable: no algorithm exists to determine, for every formula, whether it is a valid . In practice, first-order logic underpins , , and database query languages like SQL, where predicates model real-world relations and quantifiers handle aggregation over data. Its expressive power is limited compared to higher-order logics—it cannot fully capture concepts like or second-order properties without extensions—but this restriction ensures desirable properties like the , which guarantees the existence of models of various cardinalities. Despite undecidability, decidable fragments (e.g., monadic or ) find applications in verification and , highlighting first-order logic's balance of expressiveness and analyzability.

Introduction

Overview

First-order logic (FOL), also known as first-order predicate logic, is a for expressing statements about objects and their relations in a precise, symbolic manner. It employs quantifiers (such as ∀ for "for all" and ∃ for "there exists"), predicates to describe properties and relations, functions to denote operations on objects, and logical connectives (including ¬, ∧, disjunction ∨, and →) to combine these elements into well-formed expressions. This system allows for the representation of complex assertions about domains of individuals, making it a cornerstone for rigorous argumentation in various fields. The term "first-order" distinguishes FOL from higher-order logics, as its quantifiers range exclusively over individual objects (or variables) in a given , rather than over predicates, relations, or functions themselves. The core components of FOL include its syntax, which defines the rules for constructing well-formed formulas from these symbols; its semantics, which interprets formulas in mathematical structures (such as domains with assigned meanings to predicates and functions) to determine truth values; and proof systems, which provide deductive rules for deriving valid inferences from premises. These elements together enable the formal analysis of and validity. FOL plays a pivotal role in the foundations of mathematics, where it underpins axiomatic systems like Zermelo-Fraenkel set theory with choice (ZFC), allowing all mathematical entities to be modeled as sets and theorems to be derived via first-order deduction. In computer science, it forms the basis for automated reasoning tools and theorem provers, facilitating tasks such as program verification and artificial intelligence inference. Philosophically, FOL provides a framework for clarifying concepts of truth, entailment, and necessity in arguments. For instance, the statement "All humans are mortal" can be formalized in FOL as ∀x (Human(x) → Mortal(x)), where Human and Mortal are unary predicates.

Historical background

The roots of first-order logic trace back to Aristotelian syllogistic logic, which formalized deductive reasoning through categorical propositions in the 4th century BCE, laying foundational principles for later developments in quantificational inference. In the 19th century, George Boole advanced algebraic approaches to logic with his 1847 work The Mathematical Analysis of Logic, treating logical operations as mathematical manipulations of classes, which influenced the shift toward symbolic methods. Augustus De Morgan further contributed by exploring relational logic and introducing early notions of quantifiers in his 1847 and subsequent papers on syllogisms, extending Boolean algebra to handle relations and negation laws that prefigured modern predicate structures. Gottlob Frege's (1879) marked the inception of modern predicate logic, presenting the first complete system of first-order logic with a formal notation for quantifiers ( and existential) and function-argument structures, enabling precise expression of mathematical inferences beyond propositional limits. This innovation addressed deficiencies in earlier systems by incorporating quantification over variables ranging over individual objects, establishing a conceptual-script for pure thought modeled on arithmetic. Alfred North Whitehead and Bertrand Russell's Principia Mathematica (1910–1913) employed ramified type theory, a higher-order logical system, to pursue logicism, attempting to derive all of mathematics from logical axioms, which restricted quantification to avoid paradoxes like Russell's own antinomy. David Hilbert's formalist program in the 1920s sought to prove the consistency of mathematical systems using finitary methods, promoting first-order logic as a rigorous framework for metamathematics; this culminated in the 1928 textbook Grundzüge der theoretischen Logik co-authored with Wilhelm Ackermann, which standardized first-order syntax and proof theory. Kurt Gödel's 1930 completeness theorem demonstrated that every valid first-order formula is provable within the system, confirming its adequacy for capturing semantic entailment and solidifying its status as the canonical logic for mathematics. Alan Turing's 1936 results on undecidability, via his analysis of computable functions, revealed inherent limits to mechanizing first-order theorem proving, influencing understandings of logical decidability. Post-World War II advancements in and were propelled by Alfred Tarski's semantic foundations for truth and in the 1930s–1950s, alongside Leon Henkin's 1949 simplification of the proof using term models, which enhanced accessibility and applications in model-theoretic constructions.

Syntax

Alphabet and symbols

The alphabet of first-order logic consists of a fixed set of logical symbols, which are common to all first-order languages, and a variable set of non-logical symbols, which depend on the specific language being used. The logical symbols include the Boolean connectives for negation (¬), conjunction (∧), disjunction (∨), implication (→), and equivalence (↔); the quantifiers for universal quantification (∀) and existential quantification (∃); and auxiliary punctuation such as parentheses ((), to group subexpressions. These symbols provide the basic machinery for constructing compound expressions and binding variables, ensuring a standardized way to express logical relationships across different domains. Non-logical symbols, in contrast, are tailored to the and include variables, constant symbols, function symbols, and predicate symbols. Variables, typically denoted by letters such as x, y, z or indexed as v_1, v_2, \dots, form a countably to allow for arbitrary quantification. Constant symbols, such as c or a, represent specific objects in the . Function symbols, like f for a or g for a , denote mappings from objects to other objects, while predicate symbols, such as P for a predicate or R for a , express properties or relations among objects (e.g., P(x) or R(x, y). There is an infinite supply of these non-logical symbols available in principle, but practical languages employ only a finite . The collection of non-logical symbols used in a particular language is specified by its (or ), which assigns an (number of arguments) to each and while listing the (which have ). For example, a signature for the language of ordered structures might include a binary < (representing the less-than ) and a $0. Signatures are typically finite for specific theories, enabling focused axiomatizations, though the overall pool of possible symbols remains infinite to accommodate extensions. This distinction between logical and non-logical symbols allows logic to be both universal in its connective structure and adaptable to diverse mathematical and non-mathematical applications.

Terms

In first-order logic, terms are the basic expressions used to denote objects in a , constructed recursively from the language's without involving predicates or quantifiers. A is either a , a constant , or an application of a function to one or more . The set of terms is defined inductively as follows: variables and constant symbols form the base cases, serving as ; for the inductive step, if f is an n-ary function symbol and t_1, \dots, t_n are , then f(t_1, \dots, t_n) is also a . This recursive allows for nested applications, enabling terms to represent complex expressions built from simpler ones. Terms may contain , all of which are free since variable occurs only in formulas through quantifiers. For example, in the first-order theory of groups, where the signature includes a constant symbol e for the identity, a binary function symbol \cdot for multiplication, and a unary function symbol ^{-1} for inversion, the expression x \cdot (y^{-1}) is a term denoting the product of x and the inverse of y. This illustrates how terms can nest functions to capture algebraic operations without evaluating truth values.

Formulas

In first-order logic, formulas, also known as well-formed formulas (wffs), are constructed recursively from terms, symbols, logical connectives, and quantifiers, ensuring that every expression is syntactically valid. The recursive begins with formulas as the base case and builds compound formulas through iterative application of connectives and quantifiers. This structure guarantees that all subexpressions within a formula are themselves well-formed, with parentheses used to delineate the scope of operators and quantifiers. Atomic formulas are the simplest well-formed expressions and consist of either a predicate symbol applied to a sequence of terms or an equality between two terms, if equality is included in the language's signature. Specifically, if P is an n-ary predicate symbol and t_1, \dots, t_n are terms, then P(t_1, \dots, t_n) is an atomic formula; likewise, t_1 = t_2 forms an atomic formula when the equality symbol = is part of the signature. Terms serve as the arguments to predicates, representing objects or computations within the logic. Examples include P(a) for a unary predicate P and constant a, or =(f(x), c) for a function f, variable x, and constant c. Compound formulas are formed by applying logical connectives or quantifiers to existing well-formed formulas. The connectives include \neg \phi, \phi \wedge \psi, disjunction \phi \vee \psi, \phi \to \psi, and \phi \leftrightarrow \psi, where \phi and \psi are formulas. Quantifiers introduce universal \forall x \, \phi or existential \exists x \, \phi quantification over a x in a formula \phi. This recursive process ensures propagates: if \phi and \psi are well-formed, so are the resulting compounds, with parentheses enforcing —for instance, (\neg \phi) \wedge \psi. Notational conventions simplify writing formulas while preserving clarity. Parentheses are often suppressed based on operator precedence: quantifiers and negation bind most tightly, followed by conjunction and disjunction (same level, left-associative), then implication and equivalence (also same level, left-associative). For example, \forall x \, P(x) \to Q(x) is understood as \forall x \, (P(x) \to Q(x)) without additional parentheses. Bound variables in quantified formulas may be distinguished notationally with bars, such as \forall \bar{x} \, \phi(\bar{x}), though this is optional and context-dependent. A representative example is the formula \forall x (P(x) \to Q(x)), which expresses that for every x, if P(x) holds, then Q(x) holds.

Variable binding

In first-order logic, variables in a can be either or bound, depending on whether they fall within the of a quantifier. A is one that is not governed by any universal quantifier \forall or existential quantifier \exists, allowing it to act as a placeholder that can be instantiated with specific terms during . For instance, in the P(x), the x is , as no quantifier restricts its scope. Conversely, a bound is captured by a quantifier within whose it appears, limiting its reference to the elements quantified over. In the \forall x \, P(x), the x is bound by the universal quantifier, meaning its occurrences are tied exclusively to the quantification. The distinction between free and bound variables is crucial for understanding formula structure and equivalence. Formulas are considered up to alpha-equivalence, where two formulas are logically identical if they differ only in the renaming of bound variables, provided no variables are affected. For example, \forall x \, P(x) is alpha-equivalent to \forall y \, P(y), as the bound variable can be consistently renamed without altering the formula's meaning. This equivalence ensures that the choice of variable names for binding is arbitrary and does not impact logical content. A special case arises with sentences, which are formulas containing no free variables—all variables are bound by quantifiers, making the formula self-contained and interpretable as a complete without external parameters. For example, \forall x \, P(x) is a , whereas P(x) is not, due to the free occurrence of x. In axiomatic theories, such as the axioms of , like \forall x \, \exists y \, (x * y = e) express properties where y (the ) is bound by the existential quantifier, while x and e (the ) are appropriately scoped. Substitution operations further highlight the need for careful handling of variable bindings to avoid unintended capture. The [t/x]\phi replaces all free occurrences of x in the \phi with a term t, but only if t is "free for x" in \phi—meaning no free variables in t would become bound by quantifiers in \phi after . For example, substituting a constant c for x in P(x) yields P(c), but substituting y for x in \exists x \, P(x, y) must preserve y's freeness to avoid capturing it as bound. This precaution maintains the formula's intended structure and prevents errors in logical manipulation.

Semantics

Structures

In first-order logic, a , also known as a model, provides an for the symbols of a , consisting of a non-empty together with assignments of meanings to the non-logical symbols in the 's . Formally, for a L with \sigma comprising symbols, symbols, and symbols, a \mathcal{M} for L is a pair (\mathcal{D}, I), where \mathcal{D} is a non-empty set called the (or ) of , and I is an that assigns: to each symbol c \in \sigma an element I(c) \in \mathcal{D}; to each n-ary symbol f \in \sigma an n-ary I(f): \mathcal{D}^n \to \mathcal{D}; and to each n-ary symbol P \in \sigma an n-ary relation I(P) \subseteq \mathcal{D}^n. The \sigma must match the L, ensuring that every symbol in L receives an and no extraneous symbols are interpreted. A representative example is the structure for the theory of ordered abelian groups, where the signature includes a binary function symbol +, a constant symbol $0, and a binary predicate symbol <. Here, the domain \mathcal{D} = \mathbb{Z} (the integers), I(+) is the usual addition on integers, I(0) = 0, and I(<) is the standard less-than relation on integers. Structures related by mappings that preserve their interpretations are connected through homomorphisms and isomorphisms. A homomorphism h: \mathcal{M} \to \mathcal{N} between structures \mathcal{M} = (\mathcal{D}, I) and \mathcal{N} = (\mathcal{E}, J) for the same language preserves constants, functions, and relations: for any constant c, h(I(c)) = J(c); for any n-ary function f and elements d_1, \dots, d_n \in \mathcal{D}, h(I(f)(d_1, \dots, d_n)) = J(f)(h(d_1), \dots, h(d_n)); and for any n-ary predicate P and d_1, \dots, d_n \in \mathcal{D}, (d_1, \dots, d_n) \in I(P) if and only if (h(d_1), \dots, h(d_n)) \in J(P). An isomorphism is a bijective homomorphism, meaning h is one-to-one and onto, establishing that \mathcal{M} and \mathcal{N} are essentially the same up to relabeling of elements. For instance, the structure (\mathbb{N}, +, 0) of natural numbers under addition is isomorphic to the structure of even natural numbers (\{2n \mid n \in \mathbb{N}\}, +_G, 0) via the map h(n) = 2n, where +_G is ordinary addition. The requirement of a non-empty domain in standard semantics excludes empty structures, as they lead to issues such as both \forall x (x = x) and \exists x (x = x) being vacuously true or false in conflicting ways, complicating logical inference. However, some alternative semantics, such as those proposed by , permit empty domains by distinguishing between bound and free variable ranges using a super-domain, allowing empty structures in certain contexts while addressing these inconsistencies through modified axiomatizations.

Satisfaction relation

In first-order logic, the satisfaction relation determines whether a given satisfies a relative to a variable assignment. It is denoted M \models \phi, where M is a , \phi is a , and v is a variable assignment that maps the free variables of \phi to elements of the domain of M. This provides the semantic foundation for evaluating the truth of within specific interpretations. The relation is defined recursively, following the inductive structure of formulas. For an P(t_1, \dots, t_n), where P is an n-ary and t_1, \dots, t_n are , M \models P(t_1, \dots, t_n) holds \langle v(t_1), \dots, v(t_n) \rangle belongs to the of P in M, with v(t_i) denoting the value of t_i under v. For , M \models \neg \phi it is not the case that M \models \phi . For , M \models (\phi \land \psi) M \models \phi and M \models \psi . For the universal quantifier, M \models \forall x \, \phi for every element d in the domain of M, M \models \phi [v[x \mapsto d]], where v[x \mapsto d] is the that agrees with v except possibly at x, which maps to d. This recursive characterization ensures that can be computed bottom-up from subformulas to complex ones. This framework originates from Alfred Tarski's foundational work on the concept of truth for formalized languages, introduced in his paper, which established a rigorous semantic theory for logical systems including first-order logic. When \phi is a closed formula, or , with no variables, its satisfaction in M is independent of the variable assignment v, so one simply writes M \models \phi. For instance, in the structure of the integers under as the group operation (with domain \mathbb{Z}, binary function symbol * interpreted as +, and constant e as ), the \forall x \, (x * e = x) is satisfied, since for every d in the domain, d + 0 = d holds in the structure.

Validity and logical consequence

In first-order logic, a formula φ is valid, denoted ⊧ φ, if it is true in every structure for the language under every variable assignment. This means that no matter how the non-logical symbols are interpreted in a domain, φ always evaluates to true, capturing the idea of logical necessity independent of specific models. A formula φ is satisfiable if there exists at least one structure and variable assignment in which φ is true. Equivalently, φ has a model, where a model is a structure satisfying φ. The negation of satisfiability is unsatisfiability, where no structure satisfies φ, implying that ¬φ is valid. Logical consequence relates sets of formulas to individual ones: a set Γ logically entails φ, denoted Γ ⊧ φ, if every satisfying all formulas in Γ also satisfies φ. This defines semantic entailment, where the truth of φ is preserved in all models of Γ. A set Γ is inconsistent if it is unsatisfiable, meaning Γ ⊧ ψ for every formula ψ, including contradictions. Two formulas φ and ψ are logically equivalent if φ ↔ ψ is valid, so they agree in across all structures and assignments. This underpins many syntactic manipulations in . For example, the set {∀x P(x), ∃x ¬P(x)} is unsatisfiable because ∀x P(x) requires P to hold for every element in the , while ∃x ¬P(x) requires some element where P fails, yielding no possible model.

Theories and models

In first-order logic, a theory T is a set of sentences in a first-order language \mathcal{L} that is deductively closed, meaning it contains all logical consequences of its members; such theories are often axiomatizable, generated as the closure under deduction of a set of axioms \Gamma, where T = \mathrm{Cn}(\Gamma). A model of a theory T, or \mathcal{L}-structure \mathcal{A}, is any structure that satisfies every sentence in T, denoted \mathcal{A} \models T, or equivalently \mathcal{A} \models \phi for all \phi \in T. The of a \mathcal{A}, denoted \mathrm{Th}(\mathcal{A}), is the complete deductively of all \mathcal{L}- satisfied by \mathcal{A}. Two structures \mathcal{A} and \mathcal{B} are elementarily if they satisfy exactly the same , i.e., \mathrm{Th}(\mathcal{A}) = \mathrm{Th}(\mathcal{B}); this is a coarser than , which requires a bijective structure-preserving map between the domains that preserves all and functions, implying elementary equivalence but not conversely, as non-isomorphic models can share the same . An elementary embedding between structures \mathcal{A} and \mathcal{B} is an injective map e: |\mathcal{A}| \to |\mathcal{B}| that preserves satisfaction of all \mathcal{L}-formulas with parameters, meaning for any formula \phi(\mathbf{x}) and tuple \mathbf{a} from \mathcal{A}, \mathcal{A} \models \phi[\mathbf{a}] if and only if \mathcal{B} \models \phi[e(\mathbf{a})]. An elementary class is the class of all models of a fixed first-order theory T, which is closed under elementary equivalence since any two models satisfy the same sentences in T. A prominent example is Peano arithmetic (PA), a first-order theory in the language of arithmetic with symbols for successor, addition, and multiplication, axiomatized by the Peano axioms including induction schema; its models include the standard natural numbers \mathbb{N} but also non-standard models with infinite elements, all elementarily equivalent yet non-isomorphic.

Deductive systems

Hilbert-style systems

Hilbert-style systems, also known as axiomatic systems, provide a formal framework for deriving theorems in first-order logic using a finite set of axiom schemata and inference rules, emphasizing their applicability to a wide range of logical theories. These systems were developed in the tradition of David Hilbert's program for formalizing mathematics, extending propositional logic to handle quantifiers through specific axioms and rules that capture quantification principles. Unlike other deductive systems, Hilbert-style proofs proceed linearly from axioms via repeated application of rules, without local introduction or elimination operations for connectives. The axioms in a Hilbert-style system for first-order logic without consist of two main categories. First, all propositional tautologies serve as schemata, including instances such as \phi \to (\psi \to \phi), (\phi \to (\psi \to \chi)) \to ((\phi \to \psi) \to (\phi \to \chi)), \neg \phi \to (\phi \to \psi), and \phi \to \neg \neg \phi, where \phi, \psi, and \chi are any formulas built from formulas using connectives. These ensure the propositional fragment is complete. Second, quantifier s handle universal and : for any formula \phi and term t substitutable for the x in \phi, the universal \forall x \, \phi \to \phi[t/x]; and for , \exists x \, \phi \leftrightarrow \phi[y/x], where y is a for x in \phi (i.e., y does not occur in any part of \phi depending on occurrences of x). These s allow of terms for bound s while preserving logical structure. The inference rules are minimal: , which infers \psi from \phi and \phi \to \psi; and , which infers \forall x \, \phi from \phi, applicable without restrictions on the variable x. These rules, combined with the axioms, enable the derivation of all logically valid formulas. A proof is a finite sequence of formulas where each entry is either an axiom instance or follows from prior entries by one of the rules. To illustrate, consider deriving the valid distribution principle \forall x (\phi \to \psi) \to (\forall x \, \phi \to \forall x \, \psi), assuming x does not occur free in \phi. The proof proceeds as follows (using propositional tautologies and rules; subscripts denote line numbers for clarity):
  1. \forall x (\phi \to \psi) \to (\phi \to \forall x \, \psi) (quantifier axiom, with t a fresh parameter for the antecedent \phi \to \psi).
  2. \forall x (\phi \to \psi) (assumption).
  3. \phi \to \forall x \, \psi (modus ponens on 1 and 2).
  4. \forall x \, \phi \to (\phi \to \forall x \, \psi) (propositional tautology: \alpha \to (\beta \to \gamma) \to (\alpha \to \beta) \to (\alpha \to \gamma), with \alpha = \forall x \, \phi, \beta = \phi, \gamma = \forall x \, \psi, specialized from line 3).
  5. \forall x \, \phi (assumption).
  6. \phi (universal instantiation axiom on 5).
  7. \forall x \, \psi (modus ponens on 3 and 6).
  8. \forall x \, \phi \to \forall x \, \psi (propositional tautology, discharging the assumption in 5 via deduction meta-theorem, or directly via generalization on 7 under assumption 5).
  9. \forall x (\phi \to \psi) \to (\forall x \, \phi \to \forall x \, \psi) (propositional tautology on 4 and 8, discharging assumption 2).
This derivation highlights how propositional reasoning interacts with quantification rules to establish key validities. Hilbert-style systems are sound and complete: every provable is valid, and conversely, every valid (without ) is provable. The completeness theorem was established by in 1930, proving that any satisfiable in every has a proof from the axioms. This result holds for the standard Hilbert-style axiomatization, confirming its adequacy for first-order logic.

Natural deduction

Natural deduction is a deductive system for first-order logic that formalizes proofs using inference rules designed to closely resemble everyday reasoning processes. Developed by in his seminal work Untersuchungen über das logische Schließen (published in two parts in 1934 and 1935), the system emphasizes introduction rules for building compound formulas and elimination rules for extracting information from them. This approach contrasts with more axiomatic systems, such as Hilbert-style ones, by organizing derivations in a tree-like structure where assumptions are discharged as proofs progress. The rules for propositional connectives form the foundation of the system. For conjunction (\land), the introduction rule (\landI) allows inferring \phi \land \psi from premises \phi and \psi, while the elimination rules (\landE) permit deriving either \phi or \psi from \phi \land \psi. For disjunction (\lor), introduction (\lorI) infers \phi \lor \psi from either \phi or \psi alone, and elimination (\lorE) derives \chi from \phi \lor \psi by cases: assuming \phi to derive \chi and assuming \psi to derive \chi, then discharging both assumptions. Implication (\to) uses introduction (\toI), where assuming \phi to derive \psi yields \phi \to \psi upon discharging the assumption, and elimination (\toE), or modus ponens, derives \psi from \phi \to \psi and \phi. Negation (\lnot) is handled via introduction (\lnotI), assuming \phi to derive a contradiction and thus inferring \lnot \phi, and elimination (\lnotE), rejecting \phi if \lnot \phi leads to contradiction. These rules ensure that proofs proceed intuitively, with each step justified by direct inference. Quantifier rules extend the system to first-order logic, incorporating variable binding and substitution restrictions to avoid capture errors. For the universal quantifier (\forall), introduction (\forallI) requires deriving \phi(x)—where x is a fresh not free in undischarged assumptions—then inferring \forall x \, \phi(x); this enforces generality over arbitrary domains. Elimination (\forallE) substitutes any term t (free for x in \phi(x)) into \forall x \, \phi(x) to obtain \phi(t). For the existential quantifier (\exists), introduction (\existsI) infers \exists x \, \phi(x) from \phi(t) for any term t, witnessing the existence. Elimination (\existsE) assumes \phi(y) for a fresh y (eigenvariable condition), derives \psi (independent of y), and infers \psi from \exists x \, \phi(x), discharging the assumption; this isolates the existential witness. These rules, as formulated by Gentzen, support both intuitionistic and classical variants, with the latter adding rules like double negation elimination for full expressive power. To illustrate, consider a derivation of the theorem \exists x \, P(x) \to \forall y \, (P(y) \to \exists x \, P(x)), which demonstrates the interplay of quantifiers and . Begin by assuming \exists x \, P(x) (line 1). To derive the consequent, introduce an arbitrary y for . Assume P(y) (line 2). Apply \existsE to the assumption in line 1: let z be fresh, assume P(z) (line 3), then by \existsI infer \exists x \, P(x) (line 4, since P(z) it). Discharge the subassumption P(z) to obtain \exists x \, P(x) from line 1 (line 5). Discharge P(y) via \toI to get P(y) \to \exists x \, P(x) (line 6). Since y was arbitrary and no assumptions depend on it, apply \forallI to infer \forall y \, (P(y) \to \exists x \, P(x)) (line 7). Finally, discharge the initial assumption via \toI to yield the (line 8). This proof highlights how existential elimination provides a witness usable in subsequent steps without dependency issues. A key metatheoretical property of is , where any valid proof can be transformed into free of "detours"—sequences where an is immediately followed by the corresponding elimination. Gentzen outlined this in his original work, showing that normal proofs consist solely of introduction rules followed by eliminations, which simplifies and proves the of the system relative to its axioms. Later refinements by Dag Prawitz in 1965 established strong for intuitionistic , ensuring termination of the . This feature underscores the system's suitability for automated proof search and theoretical investigations in .

Sequent calculus

Sequent calculus provides a formal framework for deriving logical consequences in first-order logic through structured inference rules applied to sequents of the form \Gamma \vdash \Delta, where \Gamma is a finite of formulas representing assumptions (the antecedent) and \Delta is a finite of formulas representing conclusions (the succedent), indicating that the formulas in \Gamma jointly imply those in \Delta. This representation allows proofs to be constructed as trees, with each node corresponding to a sequent and branches determined by the application of rules, facilitating the of proof normalization and consistency. The system operates via two main categories of rules: logical rules, which introduce or eliminate connectives and quantifiers, and structural rules, which manipulate the sequents without altering their logical content. Logical rules are divided into left rules (applied to formulas in the antecedent) and right rules (applied to formulas in the succedent). For instance, the universal quantifier left rule (\forallL) states that from a sequent \Gamma, \forall x \, \phi \vdash \Delta, one may infer \Gamma, \phi[t/x] \vdash \Delta for any term t free for x in \phi, provided x does not occur free in \Gamma or \Delta; this instantiates the universal quantifier with a specific term while preserving the implication. Similar rules exist for other connectives, such as the implication right rule (\toR): from \Gamma, \phi \vdash \psi, \Delta, infer \Gamma \vdash \phi \to \psi, \Delta. These rules ensure that derivations correspond to valid inferences in first-order logic. Structural rules include weakening (W), which adds a formula to either side without changing provability: from \Gamma \vdash \Delta, infer \Gamma, A \vdash \Delta or \Gamma \vdash \Delta, A; contraction (C), which merges duplicate formulas on the left: from \Gamma, A, A \vdash \Delta, infer \Gamma, A \vdash \Delta; and (S), which permutes formulas within \Gamma or \Delta to handle multisets. The cut rule (Cut) allows combining two sequents sharing a formula A: from \Gamma \vdash \Delta, A and \Gamma', A \vdash \Delta', infer \Gamma, \Gamma' \vdash \Delta, \Delta', enabling the elimination of intermediate formulas across proofs. These rules, particularly weakening and contraction, distinguish sequent calculus from natural deduction by explicitly managing resource usage in proofs. Gerhard Gentzen introduced the foundational sequent calculi for and LJ for in his 1934–1935 work, where permits multiple formulas in the succedent while LJ restricts it to a single formula to capture intuitionistic principles. In , the rules are symmetric for classical , whereas LJ adjusts right rules to enforce single-succedent structure, ensuring derivations align with intuitionistic semantics. Both systems extend to first-order logic by incorporating quantifier rules with eigenvalue conditions to avoid capture. A simple example illustrates the use of these rules in : to derive the sequent \vdash \phi \to \phi (expressing the tautology that \phi implies itself), start from the axiom \phi \vdash \phi (initial sequent where an atomic formula appears on both sides), apply \toR to obtain \vdash \phi \to \phi. For a more involved case assuming \phi, derive \phi \vdash \phi \to \psi only if \psi follows, but consider deriving \phi, \phi \to \psi \vdash \psi: from axiom \phi \vdash \phi, weaken to \phi, \phi \to \psi \vdash \phi, then apply \toL (implication left: from \phi, \psi \vdash \psi via weakening and axiom, combined with the antecedent \phi \to \psi) to yield the target sequent, demonstrating . This tree structure highlights how rules build from atomic cases to complex implications. Central to sequent calculus is Gentzen's cut-elimination theorem, which asserts that if a sequent is provable using the cut rule, it remains provable without it, resulting in cut-free proofs that are analytic—meaning every formula in the proof is a subformula of the end-sequent or its assumptions. This theorem, proved via an inductive normalization procedure that reduces cut complexity, establishes the subformula property and underpins consistency proofs for first-order logic by eliminating non-constructive cuts.

Proof methods

Proof methods in first-order logic primarily involve algorithmic techniques for automated deduction, focusing on refutation procedures to establish unsatisfiability of negated formulas. These methods, such as semantic tableaux and resolution, transform logical proofs into systematic search problems, enabling computer implementation for theorem proving. Semantic tableaux, also known as analytic tableaux, provide a tree-based method to test for unsatisfiability by exploring branches that represent possible truth assignments. Starting from a set of formulas including the negation of the conjecture, the procedure branches on connectives and quantifiers: for disjunctions, split into cases where one or the other disjunct holds; for negations, propagate opposite truth values; universal quantifiers instantiate with new terms, while existentials introduce Skolem functions or constants. A branch closes if it contains both a formula and its negation, indicating a contradiction; if all branches close, the original set is unsatisfiable, proving the conjecture. This method was independently developed by Evert W. Beth in 1955 and Jaakko Hintikka in the same year, and later refined by Raymond Smullyan in his 1968 book on first-order logic. Resolution is a clausal refutation that reduces first-order proofs to inferences between clauses, emphasizing subsumption and unification for efficiency. Formulas are first converted to , then to clausal normal form by Skolemization (replacing existentials with functions) and distributing connectives to yield disjunctions of literals. The core rule infers from two s \neg A \lor B and A \lor C (where A may involve s) the resolvent B \lor C, provided A and \neg A are unifiable via that matches terms. Unification resolves bindings algorithmically, ensuring most general instances. A empty derived from the negated conjecture's clauses signals unsatisfiability. Introduced by J. Alan Robinson in , forms the basis for many automated provers due to its completeness in logic. Herbrand's theorem underpins these refutation methods by characterizing provability in terms of propositional over instances from the Herbrand (terms built from symbols). It states that a set of first-order sentences is unsatisfiable if and only if some of its instances is propositionally unsatisfiable, allowing to propositional logic via . This result, from Jacques Herbrand's 1930 doctoral thesis, justifies the focus on and tableaux expansions in practice. For example, consider proving P(a) \vdash \exists x P(x), or equivalently, refuting \neg \exists x P(x) under P(a). The is \forall x \neg P(x), with clauses P(a) and \neg P(x) ( implicit). Instantiating yields \neg P(a), resolving with P(a) to the empty clause, a . While efficient for propositional logic—reducible to SAT, solvable in practice by algorithms like DPLL—first-order proof search remains undecidable due to the halting problem equivalence, though heuristics like ordering and subsumption mitigate complexity in automated systems.

Equality

Logic without equality

First-order logic without equality, also known as equationaless first-order logic, modifies the standard syntax by excluding the equality predicate as a logical symbol. In this variant, the language consists of variables, constant symbols, function symbols, predicate symbols (other than equality), and logical connectives including quantifiers. Atomic formulas are formed solely by applying non-equality predicates to terms, such as P(t_1, \dots, t_n), where terms are built from variables, constants, and function applications, without the form t_1 = t_2. Identities, if needed, must be expressed indirectly through other predicates or axioms within a specific theory, though this is not part of the core logic itself. Semantically, structures for first-order logic without equality are interpretations comprising a non-empty , interpretations for symbols as operations on the domain, and interpretations for symbols as relations on the domain, but without a designated fixed to the on the domain. Satisfaction of formulas proceeds recursively as in standard first-order logic: an P(t_1, \dots, t_n) holds in a under a assignment if the denotations of the terms lie in the interpreted by P. This setup permits models where the relation, if introduced as an ordinary predicate, need not coincide with actual identity, allowing for non-standard interpretations. A key consequence of omitting equality is that the logic cannot distinguish between elements that satisfy precisely the same formulas; distinct elements may be indistinguishable if they participate identically in all and operations defined by the predicates and functions. For instance, in a model, two elements a and b could satisfy P(a, c) \leftrightarrow P(b, c) and Q(a) \leftrightarrow Q(b) for all predicates P and Q, without the logic forcing a = b. This leads to coarser models compared to those with , where the relation enforces uniqueness. Such indistinguishability affects proofs and , as validity and consequence may hold in broader classes of structures. An illustrative example arises in axiomatizations of , where the sole primitive predicate is membership \in, without . Here, the logic cannot natively express that two sets are distinct solely based on differing members; instead, the theory must incorporate mechanisms to enforce separation of elements that share all membership properties, highlighting the need for careful construction to avoid collapsing distinct sets. In general, the expressiveness of first-order logic without is equivalent to that with , as the latter does not augment the class of definable properties, but the absence of a primitive complicates direct formulation of or injectivity. To partially simulate equality, congruence relations—equivalence relations compatible with the structure's functions and predicates—can be employed. A congruence identifies elements that behave identically under all operations and relations, effectively quotienting the to mimic within equivalence classes. This approach is useful in decision procedures, such as congruence closure algorithms, which efficiently check of quantifier-free formulas by merging congruent terms. However, full recovery of equality's discriminatory power requires additional theoretical commitments beyond the bare logic.

Equality axioms

In first-order logic with , the equality symbol "=" is treated as a , a that must satisfy specific axioms to capture the notion of . These axioms ensure that equality behaves as an with substitutivity properties, allowing replacement of equals by equals in any context without altering truth values. The fundamental axiom is reflexivity, which states that every object is equal to itself: \forall x \, (x = x) This axiom guarantees that the equality relation holds identically for any element in the domain. Complementing reflexivity are the substitution axioms, which form schemas parameterized by the function and predicate symbols in the language. For an n-ary function symbol f, the axiom schema is: \forall x_1 \dots \forall x_n \forall y \, (x_i = y \to f(x_1, \dots, x_i, \dots, x_n) = f(x_1, \dots, y, \dots, x_n)) for each position i = 1, \dots, n. Similarly, for an n-ary predicate symbol P, the schema is: \forall x_1 \dots \forall x_n \forall y \, (x_i = y \to (P(x_1, \dots, x_i, \dots, x_n) \leftrightarrow P(x_1, \dots, y, \dots, x_n))) for each i. These schemas extend to all arities and ensure : equal arguments yield equal results for functions and preserve truth for predicates. A more general schema, applicable to arbitrary well-formed formulas \phi where y is for x in \phi, is x = y \to (\phi(x) \to \phi(y)). These axioms are integrated into deductive systems to handle equality proofs. In Hilbert-style systems, reflexivity is added as a specific (often labeled A6), and the substitution schemas serve as additional axiom schemas (e.g., A7), alongside the standard propositional and quantifier axioms, with and as inference s. Properties like (x = y \to y = x) and (x = y \land y = z \to x = z) are then derivable theorems. In natural deduction systems, such as Fitch-style, reflexivity is an introduction allowing \sigma = \sigma for any \sigma, while is an elimination : from \phi[\tau_1] and \tau_1 = \tau_2 (with \tau_2 substitutable for \tau_1), infer \phi[\tau_2]. For example, in the first-order theory of groups, equality axioms interact with group axioms like the existence of an e satisfying \forall x \, (x * e = x), where * is the . Using , one can derive \forall x \, (e * x = x) by reflexivity and on the operation, ensuring consistent manipulation of identities in proofs of group properties. Collectively, these axioms force any model of the logic to interpret "=" as the actual relation on the , distinguishing it from mere indiscernibility and enabling "normal models" where distinct are distinguishable by formulas.

Interpreting equality

In first-order logic without a , can be interpreted using non-logical predicates via Leibniz's law, which characterizes two objects as if they share all properties expressible in the . Formally, this is captured by the second-order condition x = y \forall P (P(x) \leftrightarrow P(y)), where P ranges over all predicates; however, in a first-order with a finite , this reduces to a first-order expressing that x and y satisfy exactly the same relations with respect to all tuples of other . This interpretation yields what is known as Leibniz equality, an definable by conjoining conditions for each and in the —for instance, for a binary R, including clauses like \forall u \forall v (R(u, v, x) \leftrightarrow R(u, v, y)) and permutations thereof. In theories where the non-logical symbols are sufficiently rich to distinguish all distinct elements in every model, this Leibniz coincides with the actual on the . A concrete example occurs in the theory of dense linear s, formulated in the language with a single binary predicate < for the strict order. Here, is interpretable as the first-order formula \neg (x < y \lor y < x), which holds precisely when x and y are the same element, as the axioms ensure totality and irreflexivity of <. This definition aligns with the standard semantics, where models like the rationals (\mathbb{Q}, <) satisfy the and no-endpoints conditions, rendering the interpreted faithful to the . In the theory of arithmetic, such as Peano arithmetic in the language with constants and , binary functions + and \times, can be interpreted as the relation congruent with respect to these operations: x = y holds if for all z, the terms z + x and z + y are interchangeable, and similarly for , formalized through the properties in the axioms. This interpretation ensures that behaves as the in models where the operations uniquely determine elements, as in the standard natural numbers. Indiscernibility arises in structures where the interpreted acts as a , meaning it preserves the non-logical symbols: if [x = y](/page/X&Y), then relations hold equivalently for x and y, and function applications yield congruent results. In model-theoretic terms, this corresponds to models where the Leibniz is trivial, ensuring no distinct elements are swapped by automorphisms while respecting the structure's operations and relations. However, such interpretations have limitations: in theories lacking sufficient non-logical symbols (e.g., empty signatures), no non-trivial definition of is possible, as there are no formulas to distinguish elements. Even in richer theories, ensuring the interpreted coincides exactly with the across all models often requires an infinite , such as replacement axioms for every formula, to exclude indiscernible distinct elements; a finite axiomatization cannot guarantee this in general.

Metalogic

Completeness theorem

, a foundational result in , asserts that in first-order logic, a \phi is semantically valid—true in every — it is syntactically provable from the logical axioms using the inference rules (\models \phi \iff \vdash \phi). This equivalence holds more generally for theories: a set of \Gamma semantically entails \phi (\Gamma \models \phi) \phi is provable from \Gamma (\Gamma \vdash \phi). The theorem establishes a perfect correspondence between the semantic and syntactic notions of consequence in first-order logic, ensuring that the deductive systems capture all valid inferences. Proved by Kurt Gödel in his 1930 paper, the theorem's soundness direction (\vdash \phi \implies \models \phi) follows directly from the definitions of provability and truth in models, while the completeness direction (\models \phi \implies \vdash \phi) requires a non-trivial construction. Gödel's original proof used a method involving maximal consistent sets and canonical models, but a more accessible approach, known as the Henkin construction, was later developed by Leon Henkin in 1949. In this construction, starting from a consistent set of sentences \Gamma, one iteratively expands \Gamma into a maximally consistent theory by adding "witnesses" (new constants and sentences witnessing existential quantifiers, such as \exists x \, \psi(x) \to \psi(c) for a new constant c). The resulting theory is then used to define a term model where the interpretation of each term is itself, ensuring satisfaction of all sentences in the expanded set; this model satisfies the original \Gamma, proving that consistency implies satisfiability. A key corollary is that every consistent theory admits a model, linking syntactic consistency (no proof of ) to semantic (a structure making all axioms true). For example, Peano arithmetic, being consistent, has a model (such as the standard natural numbers), though non-standard models also exist due to other results. The theorem has implications for decidability: since provability is semi-decidable (one can search for proofs), shows that the set of valid first-order formulas is recursively enumerable, providing a computational perspective on logical validity without resolving full decidability.

Undecidability

The Entscheidungsproblem, formulated by David Hilbert and Wilhelm Ackermann, asks whether there exists an algorithm that can determine, for any given sentence in first-order logic, whether it is valid—meaning true in every possible model—or whether it is satisfiable in some model. In 1936, Alonzo Church and Alan Turing independently provided negative solutions to this problem, demonstrating that first-order logic is undecidable: no general algorithm exists to decide the validity or satisfiability of arbitrary first-order sentences. Church's proof relied on his work with λ-calculus, reducing the to the undecidability of whether two λ-expressions are equivalent. Turing's approach, using his newly introduced concept of computable numbers and , reduced the Entscheidungsproblem to the : determining whether a halts on a given input is undecidable, and this mirrors the non-computability of validity in first-order logic by encoding logical structures into machine computations. Both results established that the set of valid first-order sentences is not recursive, though it is recursively enumerable (one can search for a proof to confirm validity), but there is no algorithm to confirm invalidity in general. This undecidability extends to specific first-order theories, particularly arithmetical ones. For instance, Peano arithmetic, a standard first-order theory of natural numbers with axioms for successor, addition, and multiplication, is undecidable: there is no algorithm to determine whether a given sentence in its language is provable from the axioms. This follows from Kurt Gödel's second incompleteness theorem (1931), which implies the existence of undecidable sentences within any consistent, sufficiently powerful axiomatizable theory like Peano arithmetic, combined with the recursive enumerability of its theorems via exhaustive proof enumeration. The theorems of Peano arithmetic form a recursively enumerable set, as proofs can be generated and checked mechanically, but the full set of valid sentences (true in the ) is not recursive due to these undecidable instances. A concrete example arises in (often denoted ), a finitely axiomatized fragment of Peano arithmetic that includes basic axioms for successor and but omits full . is essentially undecidable, meaning any consistent extension that interprets the full structure of natural numbers (with multiplication) remains undecidable. For instance, the Gödel sentence constructed for , which asserts its own unprovability, is valid (true in the ) but neither provable nor refutable in , illustrating a whose validity cannot be algorithmically decided within the theory. This undecidability holds even though is too weak to prove many simple arithmetic truths, such as the totality of .

Löwenheim–Skolem theorem

The is a fundamental result in stating that if a first-order theory in a of \lambda has an infinite model, then for every infinite \kappa \geq \max(\aleph_0, \lambda), the theory has a model of \kappa. This encompasses both the downward Löwenheim–Skolem theorem, which guarantees the existence of countable models for satisfiable theories in countable languages, and the upward version, which ensures models of arbitrarily large infinite cardinalities. The theorem originated with Leopold Löwenheim's 1915 proof of the downward version, showing that any satisfiable first-order sentence in a countable has a countable model. extended this in 1920 by proving the full theorem, including the upward direction, through a combinatorial argument that constructs models by selecting es for existential quantifiers in a controlled manner. Modern proofs often rely on the Henkin construction, which builds a model by expanding the with constants for each existential and applying the theorem to obtain a consistent theory with the desired . Alternatively, the upward Löwenheim–Skolem theorem can be proved using : given an infinite model of \mu, one forms an ultraproduct over \mu many copies with a suitable ultrafilter to yield an elementary extension of \kappa for \kappa \geq \mu. (Note: This is from a , but assuming a URL; actually, for Chang-Keisler, it's a , so perhaps use a reference.) A key implication of the theorem is the non-categoricity of first-order theories with infinite models: no such theory can specify a unique model up to in any infinite , as the existence of models of varying sizes precludes uniqueness. For instance, the first-order theory of dense linear orders without endpoints—axiomatized by the axioms of a strict plus density (\forall x \forall y (x < y \to \exists z (x < z \wedge z < y))) and no endpoints (\forall x \exists y (x < y) and \forall y \exists x (x < y))—has non-isomorphic models of different cardinalities, such as the countable rationals \mathbb{Q} and the uncountable reals \mathbb{R}. The theorem also gives rise to Skolem's paradox, first noted by Skolem in 1922: a countable model of set theory (such as ZFC) must contain elements interpreted as uncountable sets, like the power set of the natural numbers, yet the model's overall domain is countable from the external viewpoint. Skolem resolved this by emphasizing that countability is not absolute but relative to the model's internal notion of ; what appears uncountable inside the model may be countable externally due to the model's non-standard .

Compactness theorem

The compactness theorem is a fundamental result in the of logic, stating that a set of sentences \Gamma is every finite of \Gamma is . This principle implies that in logic can be reduced to checking finite portions of any potentially infinite theory, highlighting the logic's finite character despite its ability to express infinite structures. The theorem emerged in the 1930s as a consequence of Kurt Gödel's 1930 proof of the completeness theorem for logic, which establishes that every consistent set of has a model. Earlier, a version of was known for propositional logic, but Gödel's work extended it to the first-order setting by showing that if a is finitely satisfiable, a model exists, as any proof of inconsistency would be finite. Alternative proofs include the model-theoretic approach using ultraproducts, introduced by Jerzy Łoś in , which constructs a model from an ultrafilter on a family of finite models. Another proof employs Leon Henkin's 1949 construction, which builds a model by systematically extending maximally consistent sets of , ensuring the whole is realized in a countable model. A classic example illustrates the theorem's power: consider the theory consisting of sentences \phi_n asserting "there are at least n distinct elements in the domain" for each n. Each finite subset \{\phi_{n_1}, \dots, \phi_{n_k}\} is satisfiable in a finite model with \max\{n_1, \dots, n_k\} elements, so by , the entire has a model, which must be infinite. This demonstrates how guarantees the existence of infinite models from finite approximations. Applications of the compactness theorem extend beyond pure logic. In non-standard analysis, used it in 1966 to construct models of the real numbers augmented with , enabling rigorous calculus by extending the of real closed fields with sentences forcing "infinitesimal" elements. It also proves the existence of non-standard models of arithmetic, linking to the by ensuring models of various infinite cardinalities.

Expressiveness and limitations

Expressive power

First-order logic can define certain subsets of structures through formulas that specify properties of elements. In the structure of natural numbers equipped with the successor function S, for instance, every finite subset is first-order definable by iterating the successor from the zero element a finite number of times. Similarly, every cofinite subset is definable, as it consists of all elements except a finite definable set. These definable sets capture basic arithmetic relations but are limited to ultimately periodic patterns in the successor structure. Despite these capabilities, first-order logic faces significant expressive limitations, particularly in capturing infinitary or global properties. It cannot define finiteness, as any purported first-order axiomatization of finite structures would, by the , admit infinite models: if every finite subset of the axioms is satisfiable in a finite model, the entire set is satisfiable in some model, which must be to satisfy arbitrarily large finite approximations. Likewise, first-order logic cannot express well-ordering in the language of linear orders, since compactness allows for non-well-ordered models that satisfy any finite subset of well-ordering axioms, such as descending chain conditions of finite length. It also fails to define in topological structures, as the logical precludes axiomatizing properties that distinguish compact from non-compact spaces in first-order terms. The Ehrenfeucht–Fraïssé games provide a precise to quantify the expressive power of logic by modeling the back-and-forth exploration of structures. In these games, two players, the Duplicator and the , alternately select elements in two structures over a fixed number of rounds, with the Duplicator aiming to preserve relations; a winning strategy for the Duplicator up to quantifier rank k shows that the structures are indistinguishable by first-order sentences of quantifier depth at most k. This game-theoretic characterization reveals the local nature of first-order expressiveness, where global distinctions require higher quantifier ranks. A concrete illustration of these limits is that first-order logic cannot distinguish finite from infinite models in certain theories, such as the theory of dense linear orders without endpoints; by the upward , infinite models exist alongside finite approximations, and compactness ensures no first-order sentence forces finiteness across all models. In the of logics, first-order logic sits below monadic second-order logic, which extends expressiveness by quantifying over unary predicates (sets of elements). While first-order logic cannot define graph connectivity—requiring paths between all pairs of vertices—monadic second-order logic can express it via over edge sets forming a connected spanning . This added power allows monadic second-order logic to capture regularity and properties that elude first-order formulas, establishing a strict expressive .

Formalizing natural language

First-order logic excels at formalizing simple quantified statements in , such as "Every dog barks," which translates directly to the formula \forall x (Dog(x) \to Barks(x)), capturing over individuals satisfying a property. This approach succeeds for basic categorical assertions, where predicates denote properties or relations, and quantifiers align with determiners like "every" or "some," enabling precise semantic evaluation in model-theoretic terms. However, translating natural language into first-order logic encounters significant challenges due to linguistic features like tense, modality, anaphora, and plurals, which often require extensions beyond standard first-order structures. Tense introduces temporal dependencies, such as in "John walked," which demands additional temporal parameters or operators not native to first-order logic. Modality, as in "John might walk," involves possible worlds semantics that first-order logic alone cannot fully accommodate without modal enrichments. Anaphora poses issues with pronoun resolution, particularly in cases where references depend on prior discourse rather than strict variable binding. Plurals complicate matters further, as expressions like "some dogs bark" can imply distributive readings (each dog barks) or collective ones (the group barks together), which first-order logic struggles to distinguish without auxiliary mechanisms. A notable example of these difficulties is the in donkey sentences, such as "Every farmer who owns a beats it," where the "it" can receive a interpretation (the beats every owned) or an existential one (the beats some owned), defying straightforward formalization due to scope constraints on indefinites and . This arises because quantifiers cannot easily capture the dynamic required for anaphoric dependencies across clauses. Montague grammar addresses some of these gaps by providing a formal semantic framework that bridges and logical forms, using compositional rules to translate into interpretations, though it highlights logic's limitations in handling full expressivity. Another key limitation is logic's inability to express generalized quantifiers common in , such as "most," which requires comparing cardinalities (e.g., "Most students smoke" means the number of smoking students exceeds non-smoking ones), a property undefinable in terms without higher machinery. This stems from logic's restriction to first-order definable sets, as shown by Lindström's theorem, preventing direct encoding of proportion-based determiners like "most" or "exactly half."

Comparison to other logics

First-order logic (FOL) extends propositional logic by incorporating predicates, functions, and quantifiers, allowing it to express relations and properties among objects that propositional logic cannot capture. Propositional logic operates solely on atomic propositions and truth-functional connectives like , , and disjunction, treating sentences as indivisible units without internal structure, which limits it to analyzing validity based on truth values alone. In contrast, FOL's universal (∀) and existential (∃) quantifiers enable statements about "all" or "some" individuals in a domain, such as ∀x ∃y (Parent(x, y) → HasChild(x)), expressing relational dependencies that propositional logic renders as mere propositional atoms without quantification. Compared to higher-order logics, FOL restricts quantification to individual variables, avoiding the ability to quantify over predicates or sets of individuals, which both enhances its consistency relative to set-theoretic paradoxes and curtails its expressive power. Higher-order logics, such as , permit quantification over relations (e.g., ∀P ∃x P(x)), enabling the formulation of principles like that uniquely characterize structures like the natural numbers up to , a feat impossible in FOL due to its limited scope. For instance, can define the property of well-ordering—a where every non-empty has a least element—using quantification over subsets, whereas FOL cannot express this concept, as it lacks the means to bind over collections of elements. This restriction in FOL prevents paradoxes like Russell's but results in non-categorical theories, where models may vary in or structure, unlike the more definitive axiomatizations possible in higher-order systems. Description logics (DLs) represent a decidable fragment of FOL tailored for knowledge representation and ontologies, trading some of FOL's expressive breadth for computational tractability in reasoning tasks. While FOL supports arbitrary nesting of quantifiers, function symbols, and complex combinations, DLs focus on concept descriptions (unary predicates) and roles ( relations) with restricted constructors like intersections, unions, and limited quantifiers (e.g., ∀R.C for "all R-successors are C"), making them less expressive overall but sufficient for modeling taxonomic hierarchies and . Consequently, FOL can encode full relational structures and arbitrary sentences, enabling broader applications in and , but at the cost of undecidability, whereas DLs ensure efficient automated inference for semantic web standards like , though they falter on problems requiring deep nesting or numerical restrictions beyond basic . Lindström's theorem establishes FOL as the maximal abstract logic satisfying both the —stating that a set of has a model if every finite subset does—and the , which guarantees models of various cardinalities. Specifically, any logic extending FOL that preserves these properties must be equivalent to FOL in expressive power, highlighting its unique balance of generality and desirable model-theoretic features among abstract logics. This characterization, proven in 1969, underscores why extensions like those with generalized quantifiers or infinitary operators lose compactness or the Löwenheim–Skolem property, reinforcing FOL's foundational role despite its limitations relative to more powerful systems.

Variations and extensions

Restricted and many-sorted logics

Restricted logics are fragments of first-order logic with syntactic limitations that simplify certain properties, such as decidability. Monadic first-order logic restricts predicates to (one-argument) relations, excluding higher-arity predicates and function symbols beyond constants. This fragment was shown to be decidable by Löwenheim in 1915, meaning there exists an algorithm to determine the validity of any formula, unlike full first-order logic. Equational logic further restricts the to universal sentences involving only equations between terms, using as the sole and no other connectives or quantifiers beyond ones. As a proper fragment of first-order logic, it supports sound and complete proof systems based on term rewriting and congruence closure, facilitating applications in algebraic specifications. Many-sorted first-order logic extends the standard syntax by incorporating a of sorts, each representing a distinct of objects, along with typed variables, functions, and that operate only within or between specified sorts. For instance, in a with sorts for (e.g., people) and groups (e.g., teams), a like "member_of" might have \langle i, g \rangle, taking an and a group as arguments. Semantically, structures consist of non-empty domains for each sort, with interpretations respecting these type constraints, preserving the Tarski-style from single-sorted logic. A key feature is the conservative translation of many-sorted logic into single-sorted first-order logic, achieved by introducing unary predicates for each sort and relativizing quantifiers. For a \exists x^s \phi(x^s), where s is a sort, the translation becomes \exists x (S(x) \land \phi^*(x)), with S denoting the sort predicate and \phi^* the adjusted subformula; this embedding preserves and validity. Such reductions demonstrate that many-sorted logic has the same expressive power as single-sorted but with added structure. An illustrative example is typed arithmetic, where sorts distinguish integers (\mathbb{Z}) from (\mathbb{Q}), with functions like defined within \mathbb{Z} and restricted to \mathbb{Q}. A might assert \forall x^\mathbb{Z} \forall y^\mathbb{Z} \exists z^\mathbb{Z} (add(x,y) = z^\mathbb{Z}), preventing type mismatches like adding an integer to a rational directly. The primary benefits include error prevention through , which avoids ill-formed expressions, and enhanced efficiency in by pruning invalid search paths. In programming languages, many-sorted logic underpins type systems in object-oriented paradigms, supporting and modular specifications, as seen in languages like EPOS where classes correspond to sorts. This integration facilitates and knowledge representation in systems.

Infinitary logics

Infinitary logics extend logic by permitting formulas of infinite length, thereby increasing expressive power while retaining certain desirable properties such as the existence of semantics and deduction systems under suitable set-theoretic assumptions. These logics are particularly useful in for capturing properties that require infinitely many first-order axioms, such as the standard structure of the natural numbers or rationals. The syntax allows infinite conjunctions and disjunctions, but typically restricts quantifiers to finite lengths to maintain interpretability. The paradigmatic example is L_{\infty,\omega}, which extends the first-order language by allowing conjunctions and disjunctions of length less than \aleph_1 (i.e., at most countable) while keeping quantifiers finite in length. More generally, for infinite cardinals \kappa and \lambda with \lambda \leq \kappa, the logic L_{\kappa,\lambda} permits conjunctions and disjunctions of cardinality less than \kappa and quantifier blocks (sequences of quantifiers) of length less than \lambda. These languages were introduced by and in the late , with significant developments by Richard Karp in the , who proved completeness results for L_{\omega_1,\omega}. Semantics for these logics are defined over structures in a manner analogous to first-order logic, using Tarski-style satisfaction, but requiring the for uncountable cases. A key property distinguishing these logics is their with to . The holds for L_{\infty,\omega}, as established by Jon Barwise using admissible sets, meaning that a has a model if every countable subtheory does; this preserves the finite character of entailment in a countable infinitary setting. However, compactness fails for stronger logics like L_{\omega_1,\omega_1}, where infinite quantifier blocks allow expressing properties such as well-orderings of uncountable length that violate . This limitation highlights the between expressiveness and logical virtues in infinitary extensions. Infinitary logics enable precise characterizations of specific mathematical structures through infinite axioms. For instance, the rational numbers \mathbb{Q} as an can be axiomatized uniquely up to in L_{\omega_1,\omega} by combining first-order axioms for ordered fields with a countable infinitary asserting standard field operations on . This involves a countable over all pairs of natural numbers m, n to enforce that sums and products of "standard" elements (built from 1 via successors and inverses) match the rational arithmetic, ensuring no non-rational elements satisfy the operations in a non-standard way. Such axiomatizations demonstrate how infinitary conjunctions compactly encode infinite families of first-order . Another important result in this framework is the generalization of Łoś's theorem to infinitary logics. In the context of L_{\kappa,\kappa}, Łoś's theorem states that for an ultraproduct of structures taken with respect to a \kappa-complete ultrafilter, a is satisfied in the if and only if it is satisfied in "almost all" factor structures, where "almost all" is defined the ultrafilter. This preserves elementary in the infinitary sense and extends the version, facilitating constructions like saturated models in uncountable cardinalities. The theorem, proved using the standard Łoś argument adapted to infinitary syntax, is central to model-theoretic applications of ultraproducts in these logics.

Non-classical and modal logics

Intuitionistic first-order logic extends the syntax of classical first-order logic with the same connectives and quantifiers but alters the underlying semantics to emphasize constructive proofs, rejecting the (A \lor \neg A) and elimination (\neg\neg A \to A). This rejection stems from the intuitionistic view that truth requires explicit construction, applicable only in finite or decidable cases, as opposed to classical logic's acceptance of these principles for all statements. Heyting formalized intuitionistic logic in 1930, and Kleene provided a Hilbert-style axiomatization for the first-order version in 1952. Kripke semantics provides a model-theoretic foundation for intuitionistic first-order logic using a of worlds (nodes) with a monotonic that non-decreases along accessibility relations. In this framework, a world forces an if it holds in that world, and are forced monotonically, while disjunction and require forcing in some accessible future world, and holds if whenever the antecedent is forced, the consequent is forced in all future worlds. This semantics validates intuitionistic theorems and refutes classical ones like the excluded middle, as demonstrated by Kripke in 1965. Modal first-order logic augments classical first-order logic with unary modal operators \square (necessity) and \Diamond (possibility, defined as \neg\square\neg), interpreted over Kripke frames consisting of possible worlds connected by an relation. Semantics can employ fixed domains, where the quantifier domain remains constant across worlds, or varying (world-relative) domains, where objects exist contingently and may differ between accessible worlds, often incorporating a free logic with an predicate to handle non-denoting terms. In varying domain semantics, the Barcan formula (\forall x \square A(x) \to \square \forall x A(x)) fails, allowing for the creation or destruction of objects across worlds. A representative formula in modal first-order logic is \forall x \square P(x), interpreted as "necessarily, every x satisfies P", meaning that in every accessible world, the property P holds for all objects in that world's domain. This extends classical quantification to modal contexts, enabling reasoning about necessity and possibility over predicates and individuals. Completeness holds for various systems, such as quantified K with the Barcan formula for fixed-domain models, relative to their respective semantics. Temporal logics, such as (LTL), build on logic by incorporating modal operators for linear time structures, like "globally" (G) for always and "eventually" (F) for sometime in the future. LTL extends propositional logic but translates directly into the two-variable fragment of logic over the natural numbers with a successor relation, preserving expressiveness for properties like "every request is eventually granted" (G(\mathsf{request} \to F \mathsf{grant}). Introduced by Pnueli in for program verification, LTL's semantics align with definability, though it lacks full quantifiers over individuals. Unlike classical first-order logic, which enjoys linking provability to truth in all models, intuitionistic and modal variants achieve and only relative to their non-classical semantics, such as Kripke models, without recovering classical completeness for excluded middle-violating formulas.

Higher-order logics

Higher-order logics extend logic by allowing quantification over and functions, thereby increasing expressive power beyond what is possible in systems. In , the simplest such extension, variables range over subsets or relations of the domain, enabling formulas like ∀P φ where P is a and φ is a formula possibly containing P. This allows the expression of properties that first-order logic cannot capture, such as the full induction principle for natural numbers. Full higher-order logics go further by incorporating quantification over functions of arbitrary orders, including functions that take other functions as arguments, organized via a to avoid paradoxes like Russell's. Alonzo Church formalized this in his simple theory of types in 1940, assigning types to objects, predicates, and higher-level functions (e.g., type ι for individuals, o for propositions, and (σ → τ) for functions from type σ to τ), ensuring a that supports lambda abstraction and application. The enhanced expressiveness of higher-order logics enables the definition of and achieves for certain structures, unlike first-order logic which suffers from non- by Löwenheim–Skolem. For instance, second-order Peano arithmetic includes the ∀X (X(0) ∧ ∀y (X(y) → X(y+1))) → ∀y X(y), where X is a second-order over subsets of natural numbers, guaranteeing a unique model up to in standard semantics. Similarly, second-order axioms for the real numbers, including a quantifying over all Dedekind cuts, yield a , uniquely determining the complete of reals. Semantics for higher-order logics differ in their treatment of second-order quantifiers. Standard semantics interprets predicate variables over the full of the , providing maximal expressive power and enabling results like categoricity, but it lacks a complete relative to these models. In contrast, Henkin semantics restricts interpretations to general models where second-order variables range over a selected collection of subsets closed under the logic's axioms, ensuring : a is provable if and only if true in all Henkin models.

Applications

Automated theorem proving

Automated theorem proving (ATP) in first-order logic involves computational systems that attempt to establish the logical entailment of a from a set of axioms or , typically using refutation by showing the unsatisfiability of the of the conjoined with the . Advances in this field trace back to the , when Martin Davis and developed a procedure for propositional logic that was extended to first-order logic through skolemization and Herbrand's theorem, providing a complete but computationally intensive method for checking . This laid the groundwork for more efficient techniques, particularly J.A. Robinson's introduction of in , which enabled practical automated deduction by reducing proofs to clausal form and using inference rules to derive contradictions. Resolution-based provers form the core of modern first-order ATP systems, operating on clausal normal form where formulas are represented as sets of clauses (disjunctions of literals). Central to resolution is unification, an that finds substitutions to make two terms identical, allowing literals from different clauses to be matched during ; Robinson's 1965 unification provided the efficient mechanism for this, enabling the resolution rule to resolve complementary literals after substitution. To manage the of inferences, these provers employ ordering heuristics, such as literal selection strategies that prioritize resolving certain literals (e.g., negative ones) and term orderings like Knuth-Bendix ordering to discard redundant clauses, ensuring termination and efficiency in saturation-based search. Prominent resolution-based provers include Vampire and E, both of which have dominated international competitions like the CADE ATP System Competition (CASC). Vampire, developed by Andrei Voronkov and Laura Kovács, implements an optimized superposition calculus with advanced indexing for literal selection and supports instantiation-based methods for handling quantifiers, achieving high performance on large-scale problems through heuristics like literal superpositions and forward/backward subsumption. E, created by Stephan Schulz, uses a DISCOUNT (DIsjunctive Selection with CONjunctions of Terms) heuristic for literal ordering, combined with a saturation algorithm that dynamically adjusts strategies based on clause length and age, making it particularly effective for equational problems via its rewriting and subsumption mechanisms. For reasoning with equality, which is ubiquitous in first-order logic, the superposition calculus extends by incorporating paramodulation rules to handle equational literals; developed by Leo Bachmair and Harald Ganzinger in the early 1990s, it combines ordered with simplification using rewrite rules, ensuring under fair selection strategies while avoiding irrelevant inferences through constraints like literal maximality. This calculus underpins both and , where equality is treated as a predicate with axioms, and inferences are restricted to maximal positions to focus on non-redundant steps. To address fragments involving decidable theories like linear arithmetic alongside pure first-order reasoning, ATP systems integrate with (SMT) solvers such as Z3, which handles quantifiers through pattern-based and E-matching to instantiate quantifiers efficiently during search, allowing hybrid approaches where ground subproblems are delegated to SMT while first-order saturation continues on the remainder. Performance of these systems is evaluated using the Thousands of Problems for Theorem Provers (TPTP) library, a standardized repository of approximately 25,800 first-order problems across domains like and (as of October 2025), providing benchmarks for unsatisfiability, , and model finding; maintained by Geoff Sutcliffe, TPTP enables reproducible testing with tools like SystemOnTPTP for automated prover invocation and result analysis. A representative example from the TPTP is in the domain (GRP), where provers like or can demonstrate that the s of a group—such as associativity, , and inverses—combined with the commutativity defining an , entail properties like the uniqueness of inverses or cancellation laws; for instance, starting from the abelian group axioms, a prover refutes the of commutativity to confirm its , typically resolving in seconds via superposition inferences on equational clauses.

Formal methods and verification

First-order logic (FOL) plays a central role in for specifying and verifying the correctness of hardware and software systems, enabling precise mathematical descriptions of system behaviors and properties. In this domain, FOL is used to model system states, transitions, and invariants, allowing automated or semi-automated tools to check whether implementations satisfy high-level specifications, particularly in safety-critical applications like and automotive systems. By translating system models into FOL formulas, verifiers can detect errors exhaustively within bounded scopes or prove properties inductively, reducing reliance on testing alone. In model checking, FOL facilitates the verification of temporal properties by reducing complex temporal logics to decidable FOL validity problems. For instance, the Computation Tree Logic (CTL*) fragment for liveness properties, which includes path quantifiers like "exists a path" (E) and "for all paths" (A), can be encoded into FOL to check infinite-state systems without iteration or . This reduction enables efficient validity checking using FOL solvers, as demonstrated in analyses of concurrent systems where temporal operators are translated into first-order predicates over paths and states. Similarly, first-order extensions of CTL allow model checking of systems with infinite data domains by verifying FOL-augmented temporal formulas against large state spaces. Theorem provers leveraging FOL are widely applied in hardware and software verification to establish inductive invariants and functional correctness. The ACL2 system, based on a first-order logic of total recursive functions derived from Common Lisp, has been used industrially to verify microprocessors and cryptographic hardware, proving properties like equivalence between gate-level implementations and high-level specifications through interactive theorem proving. For software, tools like Isabelle support FOL embeddings within higher-order logic frameworks to verify program behaviors, such as type safety and termination in concurrent algorithms, by discharging first-order proof obligations generated from operational semantics. These provers enable rigorous certification of systems where partial correctness is insufficient, ensuring total behavior matches specifications. The Analyzer employs relational FOL to model and analyze software designs, combining first-order predicates with relational operators for and set cardinality to specify structural properties. In verification tasks, models systems as relations between sets (e.g., components and interfaces), then uses bounded SAT solving on translated FOL formulas to detect inconsistencies or counterexamples, such as deadlocks in protocols. This approach is particularly effective for lightweight modeling of database schemas or network topologies, where relational FOL captures multiplicity constraints absent in standard FOL. A representative example of FOL in verification is the proof of algorithms using invariants expressed as first-order predicates. For , an might state that the prefix of the array up to index i is sorted and contains all elements originally in that prefix, formalized as ∀j ≤ i, ∀k ≤ j, a ≤ a ∧ permutation(a[0..i], original[0..i]), where a is the and permutation preserves equality. Automated FOL theorem provers then discharge conditions for each loop iteration, confirming partial correctness and termination under bounded inputs. This method scales to hybrid sorts by combining invariants for merge steps. IEEE standards incorporate FOL subsets to formalize specifications in domains like and . The IEEE Std 1320.2-1998 standard outlines transformations of IDEF1X97 models into equivalent FOL theories, enabling automated consistency checks for entity-relationship diagrams in systems. Similarly, the IEEE 754-2008 floating-point has been given a many-sorted FOL semantics to verify operations, supporting tool-based for numerical computations in embedded systems. These subsets ensure decidability for practical verification while maintaining expressive power for industrial requirements. Despite its strengths, FOL's undecidability poses challenges in , necessitating restrictions to decidable fragments like the Bernays-Schönfinkel-Ramsey (BSR) class, which limits formulas to quantifier prefixes ∃∀ without symbols beyond . The BSR fragment admits complete decision procedures via and , making it suitable for verifying properties in heap-manipulating programs, but it struggles with nested quantifiers common in full system models. Tools exploiting BSR, such as solvers, achieve high efficiency on bounded tasks, yet extending beyond this class often requires heuristics or approximations to handle real-world .