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 $t$ without variables, i.e. $FV(t)=\emptyset$ , i.e. given by grammar: \[

  GT ::= f(GT,\ldots,GT)

\] i.e. built from constants using function symbols.

Example

If ${\cal L}$ has no constants then $GT$ is empty. In that case, we add a fresh constant $a_0$ into the language and consider ${\cal L} \cup \{a_0\}$ that has a non-empty $GT$ . We call the set $GT$ 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 $I_H = (HU,\alpha_H)$ .

How to define $\alpha_H$ ?

Term Algebra Interpretation for Function Symbols

Let $ar(f)=n$ . Then $f : GT^n \to GT$

$\alpha_H(f)(t_1,\ldots,t_n) =$ $f(t_1,\ldots,t_n)$

This defines $\alpha_H(f)$ . How to define $\alpha_H(R)$ to ensure that elements of a set are true, i.e. that $e_S(S)(I_H) = {\it true}$ ?

is this possible for arbitrary set?

Example

Ground Atoms

If $R \in {\cal L}$ , $ar(R)=n$ and $t_1,\ldots,t_n \in GT$ , we call $R(t_1,\ldots,t_n)$ 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 $HA$ in sequence (e.g. sorted by length) and establish a bijection $p$ with propositional variables \[

 p : HA \to V

\] We will write $p(A)$ .

Example