This is an old revision of the document!
Ground Terms as Domain of Interpretation
Recall syntax of first-order logic terms in First-Order Logic Syntax.
Ground term is a term without variables, i.e.
, i.e. given by grammar:
\[
GT ::= f(GT,\ldots,GT)
\] i.e. built from constants using function symbols.
Example
If has no constants then
is empty. In that case, we add a fresh constant
into the language and consider
that has a non-empty
. We call the set
Herbrand Universe.
Goal: show that if a formula without equality (for now) has a model, then it has a model whose domain is Herbrand universe, that is, a model of the form .
How to define ?
Term Algebra Interpretation for Function Symbols
Let . Then
This defines . How to define
to ensure that elements of a set are true, i.e. that
?
Partition in two sets, one over which
is true and the other over which it is false.
Example
Consider a set that is not satisfiable :
Ground Atoms
If ,
and
, we call
an Herbrand Atom. HA is the set of all Herbrand atoms:
\[
HA = \{ R(t_1,\ldots,t_n) \mid R \in {\cal L}\ \land \ t_1,\ldots,t_n \in GT \}
\]
We order elements of in sequence (e.g. sorted by length) and establish a bijection
with propositional variables
\[
p : HA \to V
\]
We will write .
Example
We define p such that :