Herbrand's theorem

Herbrand's theorem states that a first-order formula is valid if and only if some finite set of its ground instances is propositionally valid. It connects first-order validity with finite propositional reasoning over terms built from the formula's symbols.

Herbrand universe: The set of ground terms formed from a language's constants and function symbols. Its terms supply the substitutions used to build the theorem's ground instances.
First-order logic: A formal logic with variables, predicates, functions, and quantifiers over objects. Herbrand's theorem links its quantified formulas to propositional reasoning.
Jacques Herbrand: A French mathematician and logician whose work on proof theory and algebra shaped mathematical logic. His 1930 thesis developed the result now bearing his name.
Resolution (logic): A refutation rule that derives clauses by eliminating complementary literals. First-order resolution uses ground instances to connect symbolic clauses with propositional refutation.
Herbrand expansion: A disjunction or conjunction formed from ground instances of a first-order formula's matrix. Finite expansions express the propositional side of Herbrand's equivalence.
Universal quantification: A quantifier asserting that a predicate holds for every object in a domain. Ground instances replace universally quantified variables with specific terms.
Proof theory: The study of formal proofs as mathematical objects and of the structure of derivations. Herbrand's theorem became a central bridge between proofs and semantic validity.
Automated theorem proving: The use of algorithms to find formal proofs or refutations of mathematical statements. Herbrand's theorem underlies methods that search finite ground evidence.
Skolemization: A transformation that replaces existential quantifiers with function symbols while preserving satisfiability. Skolem functions make quantified existence compatible with reasoning over ground terms.
Existential quantification: A quantifier asserting that a predicate holds for at least one object in a domain. Skolemization handles existential quantifiers before ground instances are constructed.

Linked from 2 pages