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.