Sei
F
{\displaystyle F}
Skolemform . Das Herbrand-Universum zu
F
{\displaystyle F}
H
F
{\displaystyle H_{F}}
Termen , die folgende Bedingungen erfüllt:
Ist
c
{\displaystyle c}
F
{\displaystyle F}
Konstante , dann ist
c
∈
H
0
{\displaystyle c\in H_{0}}
Kommt in
F
{\displaystyle F}
a
{\displaystyle a}
H
0
{\displaystyle H_{0}}
H
k
+
1
{\displaystyle H_{k+1}}
induktiv definiert durch
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}}
Daraus ergibt sich das Herbrand-Universum zu
F
{\displaystyle F}
H
F
=
⋃
k
≥
0
H
k
{\displaystyle H_{F}=\bigcup _{k\geq 0}H_{k}}
F bezeichne eine prädikatenlogische Formel mit
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\}}
Man sieht, dass bereits ein Funktionssymbol in
F
{\displaystyle F}
F bezeichne eine prädikatenlogische Formel mit
F
:=
∀
x
∀
y
(
f
(
x
)
∨
g
(
y
)
)
{\displaystyle F:=\forall x\forall y\left(f(x)\vee g(y)\right)}
Die jeweiligen Teilmengen sehen wie folgt aus:
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}}
F bezeichne eine prädikatenlogische Formel mit
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 }
![{\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)
