2
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ What textbook are you using, if any ? $\endgroup$
    – Mauro ALLEGRANZA
    Apr 30, 2014 at 21:32
  • $\begingroup$ 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.. $\endgroup$
    – Pawan Hsu
    May 1, 2014 at 1:41
  • $\begingroup$ is herbrand disjunction the same thing like herbrand expansion? this is what i mentioned. de.wikipedia.org/wiki/Herbrand-Expansion $\endgroup$
    – Pawan Hsu
    May 1, 2014 at 1:44
  • $\begingroup$ 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). $\endgroup$
    – Mauro ALLEGRANZA
    May 1, 2014 at 8:20

1 Answer 1

Reset to default
2
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ i know i have to convert it into skolem form. but i dont know what i gon do after that $\endgroup$
    – Pawan Hsu
    May 1, 2014 at 10:24
  • $\begingroup$ i don't understand "what does it mean to assign a truth value" $\endgroup$
    – Pawan Hsu
    May 1, 2014 at 10:28
  • $\begingroup$ @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 $\endgroup$
    – Mauro ALLEGRANZA
    May 1, 2014 at 12:09
  • $\begingroup$ ... 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 $\endgroup$
    – Mauro ALLEGRANZA
    May 1, 2014 at 12:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.