# Herbrand expansion

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??

• What textbook are you using, if any ? Apr 30, 2014 at 21:32
• im using the book "logic for computer scientists" this textbook is good but it has too little examples. i think i can get the point of the concept but i have nothing to watch and learn.. May 1, 2014 at 1:41
• is herbrand disjunction the same thing like herbrand expansion? this is what i mentioned. de.wikipedia.org/wiki/Herbrand-Expansion May 1, 2014 at 1:44
• I'm not able to read german ... I think that H-expansion is the final step in the process : Start with the formula; the clausal form of a formula in first-order logic is obtained by transforming the formula into an equivalent formula in prenex conjunctive normal form (PCNF) and then replacing existential quantifiers by Skolem functions. A formula in clausal form is satisfiable iff it has an Herbrand model, which is a model whose domain is the set of ground terms built from the function and constant symbols that appear in the formula. (see M.Ben-Ari, page 182). May 1, 2014 at 8:20

## 1 Answer

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.

• i know i have to convert it into skolem form. but i dont know what i gon do after that May 1, 2014 at 10:24
• i don't understand "what does it mean to assign a truth value" May 1, 2014 at 10:28
• @user146955 - see again page 74 : You have to convert your formula $(∀x(Px∨Qx)∧∀x∃y(Px⇔¬Py))$ into Skolem form : it will be something like : $(∀x∀z∃y(Px∨Qx)∧ ---$. Start building the Herbrand expansion $E(F) = \{ Pa \lor Qa ... \}$. By Herbrand's Theorem [page 75] : A closed formula in Skolem form is unsatisfiable if and only if there is a finite subset of $E(F)$ which is unsatisfiable (in the sense of propositional logic). Thus, if during the building of the H-expansion, we find two formulae like $P(a)$ and $\lnot P(a)$, we have proved that $E(F)$ is unsatisfiable ... 1/2 May 1, 2014 at 12:09
• ... because there is no way to assign truth-values to the members of the set $E(F)$ of formulae in such a way that all become true (if $P(a)$ is true, we have that $\lnot P(a)$ is false, and vice versa). 2/2 May 1, 2014 at 12:10