The Herbrand universe is a set in predicate logic that is used as a basic set to define the Herbrand structure . Both terms are part of the Herbrand theorem , named after Jacques Herbrand .
definition Let be a (closed) formula in adjusted Skolem form . The Herbrand universe , denoted by , is the smallest set of terms that meets the following conditions:
F.
{\ displaystyle F}
F.
{\ displaystyle F}
H
F.
{\ displaystyle H_ {F}}
If is a constant occurring in , then is .
c
{\ displaystyle c}
F.
{\ displaystyle F}
c
∈
H
0
{\ displaystyle c \ in H_ {0}}
If no constant occurs in , a new constant is introduced and included in.
F.
{\ displaystyle F}
a
{\ displaystyle a}
H
0
{\ displaystyle H_ {0}}
H
k
+
1
{\ displaystyle H_ {k + 1}}
inductively defined by . There is a set of terms that can be formed using the function symbols occurring in and the terms that have already been constructed . Let, for example, be such an n-place function symbol and let terms be off , then is . Every term that can be formed from function symbols and terms is an element of .
H
k
∪
G
{\ displaystyle H_ {k} \ cup G}
G
{\ displaystyle G}
F.
{\ displaystyle F}
H
k
{\ displaystyle H_ {k}}
G
{\ displaystyle g}
t
1
,
t
2
,
.
.
.
,
t
n
{\ displaystyle t_ {1}, t_ {2}, ..., t_ {n}}
H
k
{\ displaystyle H_ {k}}
G
(
t
1
,
t
2
,
.
.
.
,
t
n
)
∈
H
k
+
1
{\ displaystyle g (t_ {1}, t_ {2}, ..., t_ {n}) \ in H_ {k + 1}}
F.
{\ displaystyle F}
H
k
{\ displaystyle H_ {k}}
H
k
+
1
{\ displaystyle H_ {k + 1}}
The Herbrand universe results from this :
F.
{\ displaystyle F}
H
F.
=
⋃
k
≥
0
H
k
{\ displaystyle H_ {F} = \ bigcup _ {k \ geq 0} H_ {k}}
example F denote a predicate logic formula with
F.
: =
∀
x
∀
y
(
P
(
x
,
a
)
∨
Q
(
x
,
f
(
y
)
)
)
{\ displaystyle F: = \ forall x \ forall y \ left (P \ left (x, a \ right) \ vee Q \ left (x, f \ left (y \ right) \ right) \ right)}
H
F.
{\ displaystyle H_ {F}}
H
F.
=
{
a
,
f
(
a
)
,
f
(
f
(
a
)
)
,
...
}
{\ displaystyle H_ {F} = \ left \ {a, f \ left (a \ right), f \ left (f \ left (a \ right) \ right), \ ldots \ right \}}
One can see that just one function symbol in leads to an infinite number of terms.
F.
{\ displaystyle F}
Example 2 F denote a predicate logic formula with
F.
: =
∀
x
∀
y
(
f
(
x
)
∨
G
(
y
)
)
{\ displaystyle F: = \ forall x \ forall y \ left (f (x) \ vee g (y) \ right)}
The respective subsets look like this:
H
0
=
{
a
}
{\ displaystyle H_ {0} = \ {a \}}
H
0
{\ displaystyle H_ {0}}
H
1
=
{
a
,
f
(
a
)
,
G
(
a
)
}
{\ displaystyle H_ {1} = \ {a, f (a), g (a) \}}
H
2
=
{
a
,
f
(
a
)
,
G
(
a
)
,
f
(
f
(
a
)
)
,
f
(
G
(
a
)
)
,
G
(
f
(
a
)
)
,
G
(
G
(
a
)
)
}
{\ displaystyle H_ {2} = \ {a, f (a), g (a), f (f (a)), f (g (a)), g (f (a)), g (g ( a)) \}}
H
3
=
H
2
∪
...
{\ displaystyle H_ {3} = H_ {2} \ cup \ dots}
H
F.
=
lim
n
→
∞
H
n
{\ displaystyle H_ {F} = \ lim _ {n \ to \ infty} H_ {n}}
Example 3 F denote a predicate logic formula with
F.
: =
∀
x
∀
y
[
F.
(
x
,
a
)
∨
¬
G
(
b
,
f
(
y
)
)
]
{\ displaystyle F: = \ forall x \ forall y \ left [F (x, a) \ vee \ neg G (b, f (y)) \ right]}
H
0
=
{
a
,
b
}
{\ displaystyle H_ {0} = \ {a, b \}}
H
1
=
{
a
,
b
,
f
(
a
)
,
f
(
b
)
}
{\ displaystyle H_ {1} = \ {a, b, f (a), f (b) \}}
H
2
=
{
a
,
b
,
f
(
a
)
,
f
(
b
)
,
f
(
f
(
a
)
)
,
f
(
f
(
b
)
)
,
...
}
{\ displaystyle H_ {2} = \ {a, b, f (a), f (b), f (f (a)), f (f (b)), \ dots \}}
...
{\ displaystyle \ dots}
H
F.
=
lim
n
→
∞
H
n
=
H
0
∪
H
1
∪
H
2
∪
...
{\ displaystyle H_ {F} = \ lim _ {n \ to \ infty} H_ {n} = H_ {0} \ cup H_ {1} \ cup H_ {2} \ cup {} \ dots}
See also
<img src="https://de.wikipedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" title="" width="1" height="1" style="border: none; position: absolute;">
![{\ displaystyle F: = \ forall x \ forall y \ left [F (x, a) \ vee \ neg G (b, f (y)) \ right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/084f220e29cdfbe3b04c45532255f2b76c3c269c)
