Herbrand domain
From Maths
Stub grade: A
This page is a stub
This page is a stub, so it contains little or minimal information and is on a to-do list for being expanded.The message provided is:
Being created at the moment
TODO: Create redirects to this page, eg Hebrand universe, Herbrand terms, possibly term domain and ground terms
Contents
Definition
Let [ilmath]\mathscr{L} [/ilmath] be a first order language. We define the set [ilmath]H[/ilmath] (this will be the Herbrand domain of [ilmath]\mathscr{L} [/ilmath]), a subset of all the terms of a FOL, [ilmath]\mathscr{L}_T[/ilmath], inductively using the following two rules[1]:
- If [ilmath]c\in\mathscr{L}_c[/ilmath] ([ilmath]c[/ilmath] is a constant symbol of [ilmath]\mathscr{L} [/ilmath]) then [ilmath]c\in H[/ilmath]
- If [ilmath]f\in\mathscr{L}_f[/ilmath] is an [ilmath]n[/ilmath]-ary function symbol of [ilmath]\mathscr{L} [/ilmath] and the terms [ilmath]t_1,\ldots,t_n\in H[/ilmath] then [ilmath]ft_1\cdots t_n\in H[/ilmath]
The resulting [ilmath]H[/ilmath] is the Herbrand domain[1] (AKA: Hebrand universe[1] or term domain[1]) of [ilmath]\mathscr{L} [/ilmath]. The elements of [ilmath]H[/ilmath] are called Herbrand terms[1] (AKA: ground terms[1])
See next
- Hintikka set - where this definition is actually used
