Herbrand expansion

1k Views Asked by At

this is about herbrand expansion of predicate logic

Q: exhibit truth-assignment verifying the Herbrand expansion of the following formula:

$$(\forall x(Px \vee Qx) \wedge \forall x \exists y(Px \Leftrightarrow \neg Py))$$

dont really understand what my teacher want me to do here i thought after the herbrand expansion there will be infinite propositional formulas how can i exhibit the truth value on it. can somebody help me to answer this question??

1

There are 1 best solutions below

4
On

According to your book : Uwe Schöning, Logic for computer scientists (1989), page 70 :

The Herbrand universe $D(F)$ of a closed formula $F$ in Skolem form is the set of all variable-free terms that can be built from the components of $F$.

See page 74 :

Let $F=∀y_1∀y_2F^*$ be a closed formula in Skolem form. Then the Herbrand expansion, is defined as $E(F) = \{ F^*[y_1/t_1][y_2/t_2] : t_1,t_2 \in D(F) \}$. That is, the formulas in $E(F)$ are obtained by substituting the terms in $D(F)$ in every possible way for the variables occurring in $F^*$.

Please, note page 70 :

Every constant occurring in $F$ is in $D(F)$. If $F$ does not contain a constant [and this is the case with your formula], then $a$ is in $D(F)$.

Thus, the first step is to convert your formula in Skolem form : see page 57.