Herbrand’s theorem (first order logic)


Let T be a first-order theory consisting of open formulas only. Then:

  1. 1.

    If T is satisfiableMathworldPlanetmath, it has a Herbrand model

  2. 2.

    If T is not satisfiable, there is a finite subset of the set of ground instances of formulasMathworldPlanetmathPlanetmath of T which is unsatisfiable.

Title Herbrand’s theorem (first order logic)
Canonical name HerbrandsTheoremfirstOrderLogic
Date of creation 2013-03-22 14:33:10
Last modified on 2013-03-22 14:33:10
Owner iwnbap (1760)
Last modified by iwnbap (1760)
Numerical id 6
Author iwnbap (1760)
Entry type Theorem
Classification msc 03B10
Related topic HerbrandStructure