Herbrand's theorem (proof theory)

From Wikipedia, the free encyclopedia

In mathematical logic, Herbrand's theorem is a basic result of Jacques Herbrand from the 1920s. It essentially states that in formal first-order logic, all quantifier () rules can be permuted down to the bottom of a proof.

Formally: In predicate logic without equality, a formula A in prenex form (all quantifiers at the front) is provable if and only if a sequent S comprising substitution instances of the quantifier-free subformula of A is propositionally derivable, and A can be obtained from S by structural rules and quantifier rules only.