First-order logic, also known as first-order predicate calculus or predicate logic, is a formal deductive system used in mathematics, philosophy, linguistics, and computer science to express statements about objects and their relations.^[1][2] It employs a syntax comprising constants, variables, predicates, functions, logical connectives, and quantifiers restricted to ranging over individual objects (first-order), excluding quantification over predicates or sets of individuals, which distinguishes it from higher-order logics.^[1] This restriction enables key metatheoretic results, including Gödel's completeness theorem, which establishes that every logically valid formula is provable within the system, and the compactness theorem, affirming that a set of sentences has a model if every finite subset does. First-order logic underpins much of modern mathematical foundations, automated theorem proving, and database query languages, though its expressive limitations—such as the inability to fully capture arithmetic truths via Löwenheim–Skolem theorems leading to non-standard models—highlight ongoing debates in logic regarding expressive power versus decidability.^[2][1]

Mathematics

Differential equations

A first-order differential equation is an equation containing an unknown function and its first derivative but no higher-order derivatives. In the case of ordinary differential equations, the general form is dy/dt = f(t, y), where y = y(t) is the unknown function and f is a given function of t and y.^{[3] [4]} More generally, it can be expressed as F(t, y, dy/dt) = 0, where F is a function incorporating the derivative.^[4] First-order equations are classified as linear or nonlinear. A linear first-order ordinary differential equation (ODE) has the standard form dy/dt + P(t)y = Q(t), where P(t) and Q(t) are continuous functions of t; here, the dependent variable y and its first derivative appear to the first power with no products or nonlinear functions of y.^[5] Nonlinear equations include forms like dy/dt = y^2 or dy/dt = t sin(y), which do not fit the linear structure.^[3] Unlike higher-order equations, first-order ODEs lack a universal closed-form solution formula; solutions depend on the specific type and require tailored methods.^[3] Common solution techniques for first-order ODEs include separation of variables, applicable when the equation can be rewritten as g(y) dy = h(t) dt for integration. For instance, integrating both sides yields the implicit solution ∫ g(y) dy = ∫ h(t) dt + C, where C is the constant of integration.^[3] Linear equations are solved using an integrating factor μ(t) = exp(∫ P(t) dt), which, when multiplied through the equation, renders the left side exact: d/dt [μ(t) y] = μ(t) Q(t), integrable to y(t) = (1/μ(t)) [∫ μ(t) Q(t) dt + C].^{[5] [6]} Exact equations, of the form M(t, y) + N(t, y) dy/dt = 0 where ∂M/∂y = ∂N/∂t, integrate directly to a potential function whose total derivative matches the equation.^[7] Homogeneous equations, where f(t, y) = g(y/t), substitute v = y/t to reduce to separable form dv/dt = (g(v) - v)/t.^[3] Bernoulli equations, dy/dt + P(t)y = Q(t) y^n with n ≠ 0,1, transform via u = y^{1-n} to linear form.^[8] Existence and uniqueness of solutions, under Lipschitz continuity of f in y, follow from the Picard-Lindelöf theorem, ensuring a unique solution in some interval around an initial condition y(t_0) = y_0.^[9] Applications span modeling exponential growth (dy/dt = ky, solved as y = y_0 e^{kt}) and decay processes, with solutions verified by substitution into the original equation. Numerical methods like Euler's are used when analytical solutions fail, approximating y(t + h) ≈ y(t) + h f(t, y(t)) iteratively.^[10]

Logic

First-order logic, also termed first-order predicate logic or predicate calculus, formalizes reasoning about objects within a domain through predicates, functions, and quantifiers restricted to individual variables, distinguishing it from higher-order logics that quantify over predicates or sets.^[11] Its syntax comprises an alphabet of logical symbols (e.g., connectives ¬, ∧, ∨, →, ↔; quantifiers ∀, ∃; variables), non-logical symbols (constants, function symbols, predicate symbols of specified arities), and formation rules yielding terms (variables, constants, or f(t1,...,tn) where f is n-ary) and well-formed formulas (atomic predicates P(t1,...,tn), negated formulas ¬φ, conjoined/disjoined/implicated/equated φ ψ, or quantified ∀x φ, ∃x φ with x a variable).^[12] Free and bound variable occurrences are defined recursively, with sentences as formulas lacking free variables, enabling precise expression of mathematical statements like "for all natural numbers x, there exists y such that y = x + 1."^[13] Semantically, first-order logic employs structures or models consisting of a non-empty domain D and interpretations assigning constants to domain elements, n-ary functions to domain-to-domain mappings, and n-ary predicates to subsets of D^n (or equivalently, relations).^[11] Satisfaction is defined inductively via variable assignments σ: for atomic P(t1,...,tn), true if interpretations yield true; extended to connectives (e.g., ¬φ true if φ false; φ ∧ ψ true if both true) and quantifiers (∀x φ true if φ true under all σ' agreeing with σ except possibly on x; ∃x φ true if true under some such σ').^[12] A sentence φ is valid if satisfied in every structure, satisfiable if in some, and a theory T (set of sentences) is consistent if no contradiction is derivable, with models as structures satisfying all of T; validity equates to unsatisfiability of negation.^[11] Key metatheorems underpin its foundations: Gödel's completeness theorem (1930) establishes that every consistent set of first-order sentences has a model, and semantic entailment (φ follows from Γ if every model of Γ satisfies φ) coincides with syntactic provability in standard Hilbert-style or sequent calculi, yielding soundness and completeness.^[14] Compactness follows, stating infinite theories are satisfiable if every finite subset is.^[14] However, Church (1936) and Turing (1936) proved the entailment problem undecidable: no algorithm exists to determine, for arbitrary sentences, whether one follows from others or if a sentence is valid, linking to the halting problem via reductions showing first-order logic captures Turing-complete computation when including arithmetic.^[15] Subclasses like monadic logic or Presburger arithmetic (first-order theory of addition) are decidable, but full first-order logic over Peano arithmetic encodes undecidable Diophantine problems.^[15] In mathematics, first-order logic axiomatizes theories like Zermelo-Fraenkel set theory (ZFC), enabling proofs of relative consistency (e.g., Gödel's constructible universe models ZFC) and independence (e.g., continuum hypothesis via Cohen forcing), though expressiveness limits capture only "first-order" properties, excluding full second-order concepts like infinity or choice directly.^[14] Löwenheim-Skolem theorems imply countable models for countable theories, with Skolem normal form reducing quantifiers for automated reasoning, while Herbrand's theorem supports resolution-based theorem proving by grounding to Herbrand universes.^[12] These properties affirm first-order logic's balance of expressivity for formalizing much of mathematics against undecidability, contrasting decidable fragments like propositional logic.^[11]

Physical sciences

Chemical kinetics

Chemical kinetics is the branch of physical chemistry that quantifies the rates of chemical reactions and elucidates the factors influencing those rates.^[16] It distinguishes itself from chemical thermodynamics by focusing on the dynamics of how reactions proceed over time, rather than merely whether they are feasible.^[17] The field emerged in the 19th century with foundational experiments by chemists such as Ludwig Wilhelmy, who in 1850 measured the hydrolysis of sucrose and derived a rate proportional to sugar concentration.^[18] The rate of a chemical reaction is defined as the change in concentration of a reactant or product per unit time, often expressed as $-\frac{d[\ce{A}]}{dt}$ for a reactant A disappearing.^[16] For stoichiometric consistency in reactions like $\ce{aA + bB -> products}$, the rate is $\frac{1}{a}\frac{d[\ce{A}]}{dt} = \frac{1}{b}\frac{d[\ce{B}]}{dt}$.^[18] Instantaneous rates capture variability over short intervals, while average rates approximate over longer periods; initial rates, measured at t=0, minimize product interference and are common in experiments.^[19] Rate laws mathematically relate reaction rate to reactant concentrations, typically in the form rate = $k[\ce{A}]^m[\ce{B}]^n$, where k is the rate constant, and m, n are reaction orders reflecting concentration dependencies.^[20] The overall order is m + n, determined experimentally via methods like initial rates or isolation, not from stoichiometry.^[16] Zero-order reactions (rate independent of concentration) occur in saturated catalysis; first-order (linear dependence) in unimolecular decompositions; higher orders indicate multi-step mechanisms.^[21] Molecularity describes elementary step involvement (unimolecular, bimolecular), contrasting with empirical order.^[22] Integrated rate laws derive from differential forms for concentration-time profiles: for first-order, $[\ce{A}] = [\ce{A}]_0 e^{-kt}$; half-life $t_{1/2} = \frac{\ln 2}{k}$, independent of initial concentration.^[21] Second-order (e.g., $\ce{2A -> products}$) yields $\frac{1}{[\ce{A}]} = \frac{1}{[\ce{A}]_0} + kt$, with concentration-dependent half-life.^[20] These enable order determination by linearity in plots like ln[A] vs. t or 1/[A] vs. t. Factors influencing rates include reactant concentration (per rate law exponents), physical state (gaseous or solution phases react faster than solids due to mobility), and surface area (finer particles increase heterogeneous rates).^[23] Catalysts accelerate via alternative low-energy pathways without net consumption, as in enzyme kinetics following Michaelis-Menten models.^[24] Chemical nature dictates intrinsic reactivity, with ionic reactions often faster than covalent in solution. Temperature profoundly affects rates, typically doubling every 10°C rise for many reactions. The Arrhenius equation, $k = A e^{-E_a / RT}$, quantifies this, where A is the pre-exponential factor (collision frequency proxy), $E_a$ activation energy (minimum for reaction), R gas constant, T absolute temperature.^[25] Plotting ln k vs. 1/T yields straight line with slope $-E_a / R$; experimentally, $E_a$ ranges from near-zero (diffusion-limited) to over 100 kJ/mol.^[26] Collision theory posits reactions require effective collisions with sufficient energy (> $E_a$) and proper orientation, predicting A ≈ collision frequency times steric factor.^[24] Transition state theory refines this, viewing the transition state as a fleeting high-energy intermediate at the potential energy maximum; rate = $\frac{kT}{h} e^{\Delta S^\ddagger / R} e^{-\Delta H^\ddagger / RT}$, linking to activation entropy $\Delta S^\ddagger$ and enthalpy $\Delta H^\ddagger$.^[27] This theory better accommodates complex mechanisms, underpinning enzyme and surface catalysis models. Experimental methods include spectrophotometry for concentration tracking, stopped-flow for fast reactions (<1 ms), and flash photolysis for transients.^[28] Applications span combustion modeling (e.g., ignition delays in engines), pharmacokinetics (drug decay rates), and atmospheric chemistry (ozone depletion via Cl• + O3 rates).^[29] Mechanisms are inferred by rate law matching to elementary steps, with steady-state approximations for intermediates.^[22]

Phase transitions

First-order phase transitions occur when a system passes between two thermodynamic phases with discontinuities in the first derivatives of the Gibbs free energy $G$ with respect to temperature and pressure, specifically entropy $S = -\left(\frac{\partial G}{\partial T}\right)_P$ and volume $V = \left(\frac{\partial G}{\partial P}\right)_T$.^[30][31] This classification, proposed by Paul Ehrenfest in 1933, distinguishes them from higher-order transitions where higher derivatives are discontinuous.^[32] At the transition point, the two phases coexist with equal Gibbs free energies, but exhibit abrupt changes in density, specific heat capacity, and other extensive properties.^[31] A hallmark of first-order transitions is the release or absorption of latent heat $\Lambda$, the enthalpy difference required to complete the phase change at constant temperature and pressure without altering the system's temperature.^[32] This is quantified as $\Lambda = T(S_2 - S_1)$, where $T$ is the transition temperature and $S_2$, $S_1$ are the entropies of the respective phases.^[30] The phase boundary in the pressure-temperature plane follows the Clausius-Clapeyron equation: $\frac{dP}{dT} = \frac{\Lambda}{T(V_2 - V_1)}$, linking the boundary slope to the volume change $\Delta V = V_2 - V_1$.^[32][31] Below the critical point, mechanical instability arises, with $\left(\frac{\partial P}{\partial V}\right)_T > 0$ in metastable regions, resolved by the Maxwell equal-area rule for equilibrium: $\int (P - P_0(T)) dV = 0$.^[32] Common examples include the solid-liquid transition for water at its triple point of 273.16 K and 0.612 kPa, where ice, liquid water, and vapor coexist.^[32] The melting of ice at 1 atm absorbs a latent heat of fusion of approximately 6.0 kJ/mol, while boiling water at 373.15 K and 1 atm requires 44 kJ/mol for vaporization.^[30] Sublimation of dry ice (solid CO₂) to gas at 1 atm also exemplifies this, bypassing the liquid phase.^[30] In the van der Waals equation of state, the liquid-gas transition below the critical temperature models these discontinuities, with phase coexistence enforced by equal chemical potentials.^[32] These transitions typically proceed via nucleation and growth, where a new phase forms seeds in the parent phase, potentially leading to supercooling (e.g., liquid below freezing point) or superheating due to kinetic barriers and lack of nucleation sites.^[31] Hysteresis can occur, with the transition path depending on the direction of change, reflecting metastable states.^[32] In finite systems or under rapid quenching, the sharpness of the discontinuity may blur, but macroscopic systems exhibit the characteristic jumps.^[32]

Computer science

Formal methods

Formal methods in computer science employ first-order logic (FOL) as a foundational tool for specifying, modeling, and verifying the behavior of software and hardware systems, enabling rigorous proofs of correctness properties such as safety and termination.^[33] FOL extends propositional logic by incorporating quantifiers (universal ∀ and existential ∃) over variables ranging over domain objects, predicates to express relations, and functions, allowing concise representation of infinite-state systems and complex invariants that propositional logic cannot capture.^[34] This capability is particularly valuable in deductive verification, where system models and desired properties are encoded as FOL formulas, and theorem provers attempt to establish entailment or refute counterexamples.^[35] In software verification, FOL underpins automated theorem proving for functional programs and heap-manipulating code, with techniques like resolution and superposition enabling efficient refutation of invalid formulas in first-order settings.^[36] For instance, tools such as Z3 integrate FOL with satisfiability modulo theories (SMT) to discharge verification conditions arising from program annotations, supporting decidable fragments like linear arithmetic or arrays while approximating general cases.^[37] A key application involves translating iterative programs into FOL axioms for reasoning about loop invariants and postconditions, as demonstrated in frameworks that formalize procedural languages with discrete linear orderings to prove termination and equivalence.^[38] Similarly, in distributed systems verification, FOL reductions transform liveness properties (e.g., eventual progress) into safety checks, facilitating analysis of infinite-state behaviors via bounded model checking extensions.^[39] FOL's role extends to relational modeling in tools like Alloy, which uses bounded FOL quantification to analyze system designs for errors such as deadlocks or security vulnerabilities, though scalability limits analyses to small scopes due to the logic's undecidability.^[40] In hardware verification, FOL specifies circuit behaviors and proves equivalence against high-level designs, often combined with decision procedures for theories like bit-vectors.^[41] Despite these advances, practical use requires restricting to fragments with complete proof systems or heuristics, as full FOL validity is only semi-decidable, prompting hybrid approaches with higher-order logics for expressive power in complex proofs.^[42] Empirical evaluations show FOL-based provers succeeding on benchmarks from verification competitions, with success rates exceeding 70% for first-order problems in superposition calculi as of 2023.^[36]

Artificial intelligence applications

First-order logic serves as a foundational formalism in artificial intelligence for knowledge representation and automated reasoning, enabling the expression of complex relationships between objects through predicates, functions, and quantifiers. Unlike propositional logic, which is limited to fixed propositions, first-order logic accommodates variables and quantification over domains, allowing AI systems to generalize facts and infer new knowledge from incomplete descriptions. This expressiveness supports applications in domains requiring symbolic manipulation of structured information, such as expert systems and planning algorithms.^[43][44] In knowledge representation, first-order logic facilitates the encoding of domain-specific facts and rules in a compact, human-readable form that supports deductive inference. For instance, predicates like "CausesBreeze(Pit, Square)" can model causal relationships in environments such as the Wumpus world, where agents infer hidden states from observations. This approach underpins early AI systems for commonsense reasoning, where axioms define object properties and relations, enabling queries via unification and resolution. Academic implementations, such as those in logic programming languages like Prolog, demonstrate FOL's utility in representing hierarchical knowledge bases for tasks like semantic networks or ontologies.^[43][45][46] Automated theorem proving represents a core application, where first-order logic formalizes conjectures as theorems to be mechanically verified or refuted using resolution-based provers. Systems like Vampire and E employ saturation algorithms to explore proof spaces efficiently, achieving successes in verifying hardware designs and software correctness; for example, Vampire has dominated annual CADE ATP System Competitions since 2002 by resolving first-order clauses through indexing and literal selection. Integration with machine learning has enhanced premise selection and heuristic guidance, as in deep reinforcement learning models that learn proof strategies from large corpora, outperforming traditional methods on benchmarks like TPTP by up to 20% in proof length reduction. These tools apply to AI safety verification, where FOL encodes invariants for neural network behaviors.^[47][48][49] In AI planning and robotics, first-order logic models state transitions and goals via action preconditions and effects, supporting domain-independent planners like STRIPS derivatives. Quantified axioms describe general rules, such as "∀x ∀y Adjacent(x,y) → PossibleMove(x,y)", enabling hierarchical task decomposition in uncertain environments. Limitations arise in scalability for large domains, prompting hybrid approaches combining FOL with probabilistic extensions, though pure first-order inference remains intractable for NP-complete unification problems in worst cases. Empirical evaluations show FOL-based planners solving blocks-world problems with thousands of objects via forward chaining, but real-world deployment often requires approximations.^[43][45][44] Natural language processing leverages first-order logic for semantic parsing, translating sentences into logical forms for question answering and inference. For example, systems convert queries like "Every dog chases some cat" into ∀x (Dog(x) → ∃y (Cat(y) ∧ Chases(x,y))), enabling entailment checks against knowledge bases. This application persists in semantic web technologies like OWL, where first-order fragments underpin ontology reasoning for information retrieval. Despite advances in neural methods, FOL provides interpretable baselines, with hybrid neuro-symbolic models using it to ground embeddings in verifiable logic.^[50][44]

Engineering and systems theory

Control systems

A first-order system in control theory consists of a single energy storage element, resulting in dynamics described by a first-order ordinary differential equation of the form $\tau \frac{dy(t)}{dt} + y(t) = Ku(t)$, where $\tau$ represents the time constant, $K$ the steady-state gain, $y(t)$ the output, and $u(t)$ the input.^{[51] [52]} This form arises in linear time-invariant systems across domains, with the time constant $\tau$ quantifying the speed of response—specifically, the time for the output to reach 63.2% of its final value following a step change in input.^[51] The corresponding transfer function in the Laplace domain is $G(s) = \frac{K}{\tau s + 1}$, which captures the input-output relationship for analysis in frequency or time domains.^{[51] [52]} The step response of a first-order system to a unit step input $u(t) = 1$ (assuming zero initial conditions) is $y(t) = K(1 - e^{-t/\tau})$, exhibiting monotonic exponential rise without overshoot or oscillations.^{[51] [53]} Key transient specifications include rise time (approximately $2.2\tau$), settling time to within 2% of steady state (about $4\tau$), and no peak time due to the absence of overshoot.^[52] For impulse inputs, the response is bounded and decays exponentially, confirming inherent stability for bounded inputs in open-loop configurations.^[54] These characteristics make first-order models foundational for understanding higher-order approximations and controller design, as they highlight pure lag behavior without resonant effects. Examples of first-order systems span multiple engineering fields. In electrical systems, a series RC circuit models voltage across the capacitor with $\tau = RC$, where $R$ is resistance and $C$ capacitance.^[51] Mechanically, a mass $m$ subject to viscous friction $b$ follows $\tau = m/[b](/page/B)$, as in dashpot arrangements without springs.^[51] Thermal systems, such as a heated room with insulation, yield $\tau = R_w C_r$ (thermal resistance times heat capacity), while fluid level control in a tank draining through a valve gives $\tau = R_l C_h$ (flow resistance times hydraulic capacitance).^[51] In control applications, these models approximate processes like liquid level regulation or simple actuator dynamics, enabling proportional-integral-derivative (PID) tuning where integral action compensates for steady-state error in closed-loop setups.^[55] First-order approximations facilitate root locus or Bode plot analysis for stability margins in feedback systems.^[54]

Other applications

Economics and optimization

First-order logic has been employed in theoretical economics to formalize agent-based models, particularly through logicist approaches that integrate cognitive calculi with extensional first-order fragments for verifiable simulations. In such frameworks, predicates and quantifiers represent agents' beliefs, perceptions, and actions, enabling proofs of economic phenomena like the chain-store paradox, where backward induction yields "enter and acquiesce" outcomes for rational agents, and forward induction predicts deterrence after multiple stages. This method, detailed in Bringsjord et al. (2015), uses dynamic cognitive event calculus implemented via denotational proof languages to model fine-grained cognition, surpassing traditional game theory by capturing verifiable predictions in scenarios such as Ponzi schemes, where schemer intent is proven to sustain operations until collapse thresholds.^[56][56] Logical compactness, a property derivable in propositional extensions of first-order logic, facilitates scaling economic theories from finite to infinite domains by ensuring satisfiability of infinite formula sets if finite subsets hold, thus reproving results like the existence of stable matchings in infinite markets (extending Gale and Shapley, 1962) and strategy-proofness in man-optimal mechanisms. Gonczarowski, Kominers, and Shorrer (2020) apply this to infinite trading networks, confirming Walrasian equilibria existence (building on Hatfield et al., 2013), and to consumer demand rationalization under generalized axiom of revealed preference (GARP) for infinite datasets, constructing quasiconcave utilities where finite approximations suffice. These applications, while theoretical, address limitations in finiteness assumptions prevalent in empirical economic modeling.^[57][57] In optimization, first-order logic serves as a foundation for constraint satisfaction problems (CSPs), where satisfiability of quantified predicates over variables and domains encodes optimization constraints, though undecidability limits direct computation for complex cases. This interpretation, analyzed by Arias et al. (2021), treats FOL formulas as CSP instances, linking to algorithmic solvers in constraint programming that exploit unification—substitution of variables to equate formula instances—for solving logical constraints akin to optimization objectives. Hooker (2023) highlights synergies in hybrid systems combining logic programming with optimization, where first-order unification aids in generating feasible solutions for problems like scheduling or resource allocation, often integrated with integer programming for practical efficiency. Such uses prioritize decidable fragments, as full FOL expressiveness precludes polynomial-time optimization.^[58][59][59] Mechanized reasoning tools leveraging first-order logic have been applied to verify economic models, such as auction bidder properties, by encoding objects (e.g., "bidder b1") and relations in theorem provers, though adoption remains niche due to economics' reliance on probabilistic and calculus-based methods over pure logical deduction.^[60] Overall, while first-order logic provides rigorous formalization for deductive validity in economic inferences, its direct role in mainstream optimization or empirical economics is constrained by computational intractability, favoring specialized numerical techniques.^[61]