View source for Herbrand domain

{{Stub page|grade=A|msg=Being created at the moment}}
{{Todo|Create redirects to this page, eg [[Hebrand universe]], [[Herbrand terms]], possibly [[term domain]] and [[ground terms]]}}
__TOC__
==Definition==
Let {{M|\mathscr{L} }} be a [[first order language]]. We define the set {{M|H}} (this will be the ''Herbrand domain'' of {{M|\mathscr{L} }}), a subset of all the [[terms (FOL)|terms of a FOL]], {{M|\mathscr{L}_T}}, [[inductive definition|inductively]] using the following two rules{{rMLFFISWL}}:
# If {{M|c\in\mathscr{L}_c}} ({{M|c}} is a {{link|constant symbol|FOL}} of {{M|\mathscr{L} }}) then  {{M|c\in H}}
# If {{M|f\in\mathscr{L}_f}} is an {{n|''[[arity|ary]]''}} {{link|function symbol|FOL}} of {{M|\mathscr{L} }} and the {{link|terms|FOL}} {{M|t_1,\ldots,t_n\in H}} then {{M|ft_1\cdots t_n\in H}}
The resulting {{M|H}} is the ''Herbrand domain''<ref name="MLFFISWL"/> ({{AKA}}: ''Hebrand universe''<ref name="MLFFISWL"/> or ''term domain''<ref name="MLFFISWL"/>) of {{M|\mathscr{L} }}. The elements of {{M|H}} are called ''Herbrand terms''<ref name="MLFFISWL"/> ({{AKA}}: ''ground terms''<ref name="MLFFISWL"/>)
==See next==
* [[Hintikka set]] - where this definition is actually used
==References==
<references/>
{{Formal logic navbox|plain}}
{{Definition|Formal Logic}}