Herbrand's Theorem

Mathematical Logic · Axiom Academy

Bridging infinite first-order logic to finite ground instances Mathematical Logic • Unit 4 - First-Order Logic The Challenge of First-Order Logic In first-order logic, formulas can quantify over infinite domains. How do we determine if a formula is unsatisfiable when there are infinitely many possible interpretations? Given a first-order formula , can we reduce the question of satisfiability over an infinite domain to a finite problem? Herbrand's Theorem provides the answer: For formulas in a certain form, we only need to check ground instances (formulas with no variables). The Herbrand Universe is the set of all ground terms that can be built from the constants and function symbols in a formula. For a first-order language , the Herbrand Universe is constructed as follows: Level 0: All constants in . If none exist, add a special constant . Level n+1: All terms where is a function symbol and each is from level or earlier. Example: Building a Herbrand Universe Language: Constants: , Function: The Herbrand Base is the set of all ground atoms that can be formed using predicates from the language and terms from the Herbrand Universe. The Herbrand Base consists of all atoms of the form: where is an n-ary predicate and are ground terms from . Example: Herbrand Base Construction Language: Predicate: , Constants: , Function: ... (infinitely many ground atoms)

This is the written version of the interactive lesson above. See the full Mathematical Logic course.