Herbrand’s theorem (first order logic)

Let $T$ be a first-order 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	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