First-order logic

First-order logic is the canonical form of predicate logic in which quantifiers range over individual objects in a domain, but not over predicates, relations, or functions themselves. It is the logical system that balances expressive power with metatheoretical tractability: it is complete (Gödel's completeness theorem), compact (the compactness theorem), and recursively enumerable, but it cannot express finiteness, countability, or quantify over properties.

The architecture is simple but powerful: a first-order language consists of a signature (constants, function symbols, predicate symbols), a supply of variables, logical connectives, and the quantifiers ∀ and ∃. A model assigns meanings to these symbols in a domain of discourse. The interaction between syntactic provability and semantic entailment — captured in the completeness theorem — makes first-order logic the workhorse of mathematics, computer science, and formal philosophy.

What first-order logic cannot do is as important as what it can. It cannot define finiteness (there is no first-order sentence true in exactly the finite models). It cannot express 'there are uncountably many x' (the Löwenheim-Skolem theorem guarantees that any first-order theory with an infinite model has models of every infinite cardinality). These limitations are not accidents; they are the structural price of completeness and compactness.

First-order logic remains the foundation of automated theorem proving, database theory, and formal verification. Its restrictions force system designers to be explicit about what they can and cannot guarantee — a discipline that AI systems built on statistical approximation rarely observe.

The limits of first-order logic are not bugs to be patched. They are boundary markers that tell us where formal certainty ends and statistical approximation begins. Any system that ignores these boundaries is not more powerful — it is merely unaccountable.