The language mathematicians use for foundations cannot pin down the ordinary counting numbers
First-order logic became the standard language for writing mathematics as axioms by the 1940s. It is powerful enough that every statement true in all its models can be proved. Yet no first-order theory can describe the natural numbers or the real line so precisely that only one structure fits.
First-order logic, also called predicate logic or quantificational logic, extends propositional logic by adding variables, predicates and quantifiers. Propositional logic treats Socrates is a philosopher and Plato is a philosopher as two unrelated true-or-false statements. First-order logic sees a shared pattern: one predicate, is a philosopher, applied to two different individuals. It can also say things like for every x, if x is human then x is mortal, where for every is a quantifier ranging over a domain of objects.
The name separates it from higher-order logic, where one may quantify over predicates or functions themselves, or feed predicates into other predicates. A first-order theory, such as a theory of groups or of arithmetic, pairs the logic with a domain, finitely many functions and predicates, and a set of axioms. Peano arithmetic and Zermelo–Fraenkel set theory are the classic first-order formalisations of number theory and set theory.
Its technical virtues explain its dominance. Many proof systems for it are sound, proving only statements true in every model, and complete, proving every such statement. It satisfies powerful results including the compactness theorem and the Löwenheim–Skolem theorem, and while logical consequence is only semidecidable, automated theorem proving in first-order logic has advanced a great deal. The flip side is limited expressive power: axiom systems that capture infinite structures uniquely, called categorical systems, require stronger tools such as second-order logic.
Gottlob Frege and Charles Sanders Peirce independently laid its foundations in the 1880s. The boundary between first-order and higher-order reasoning stayed blurry until metalogical results such as Gödel's completeness theorem of 1929 clarified it. Within little more than a decade after that it had won out as the preferred framework for foundational work, and it remains central in philosophy, linguistics and computer science.
Source: First-order logic
