Herbrand’s theorem (first order logic)
Let $T$ be a firstorder theory consisting of open formulas only. Then:

1.
If $T$ is satisfiable^{}, it has a Herbrand model

2.
If $T$ is not satisfiable, there is a finite subset of the set of ground instances of formulas^{} of $T$ which is unsatisfiable.
Title  Herbrand’s theorem (first order logic) 

Canonical name  HerbrandsTheoremfirstOrderLogic 
Date of creation  20130322 14:33:10 
Last modified on  20130322 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 