# Herbrand’s theorem (first order logic)

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

1. 1.

If $T$ is satisfiable, it has a Herbrand model

2. 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) HerbrandsTheoremfirstOrderLogic 2013-03-22 14:33:10 2013-03-22 14:33:10 iwnbap (1760) iwnbap (1760) 6 iwnbap (1760) Theorem msc 03B10 HerbrandStructure