Herbrand structure: Difference between revisions

→‎Definition: corrected grammar
(→‎Definition: corrected grammar)
 
===Definition===
 
The ''Herbrand universe'' will serveserves as the universe in the ''Herbrand structure''.
 
(1) The ''Herbrand universe'' of a first-order language ''L''<sup>&sigma;</sup>, is the set of all [[Ground_term|ground terms]] of ''L''<sup>&sigma;</sup>. If the language has no constants, then the language is extended by adding an arbitrary new constant.
 
* ItThe Herbrand universe is countably infinite if &sigma; is countable and a function symbol of arity greater than 0 exists.
* In the context of first-order languages we also speak simply of the ''Herbrand universe'' of the vocabulary &sigma;.
 
(2) The ''Herbrand universe''' of a closed formula in [[Skolem normal form]] ''F'', is the set of all terms without variables, that can be constructed using the function symbols and constants of ''F''. If ''F'' has no constants, then ''F'' is extended by adding an arbitrary new constant.
 
* This second definition is important in the context of [[Resolution_(logic)|computational resolution]].