Herbrand's Theorem gives a way to reduce the question of whether a formula of first-order logic is provable to a question about a finite disjunction of substitution instances of that formula, built from terms drawn from a fixed domain called the Herbrand universe. Named for Jacques Herbrand, it is a foundational result of proof theory that underlies automated theorem-proving methods such as resolution.
Facts
StatementA first-order formula in prenex form with only existential quantifiers is provable if and only if some finite disjunction of ground substitution instances of its quantifier-free part, built from terms of the Herbrand universe, is a tautology of propositional logic, reducing first-order provability to a propositional question. Obtained by Jacques Herbrand in 1930. 1 Connections
Sources
1. Herbrand's Theorem (Wikipedia)
Wikimedia Foundationlead paragraph, first two sentencesQuote, lead paragraph, first two sentences
Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic.
Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.