How do we can conclude that two first order logic formulas are equivalent. As long as this problem should be undecidable I would like to know is there any semi-decidable technique? Does Tableau Method or Resolution work in here?

As an example $\exists x P(x) \rightarrow \forall x \exists y R(x,y)$ is equivalent to $\forall z \forall x \exists y (R(z,y) \lor \neg P(x))$ , Where this $z$ came from?


As Mauro ALLEGRANZA pointed out in the comments, $\phi$ and $\psi$ are equivalent if $\neg(\phi \leftrightarrow \psi)$ is inconsistent. in other words

$$ \begin{align} &\neg(\phi \leftrightarrow \psi)\\ &=\neg((\phi \rightarrow\psi) \land (\psi \rightarrow\phi))\\ &=(\neg(\phi \rightarrow\psi) \vee \neg(\psi \rightarrow\phi))\\ &=(\phi \land \neg\psi) \vee (\psi\land\neg\phi)\\ \end{align} $$

if we conclude that for any $\phi$ and $\psi$ the formula $(\phi \land \neg\psi) \vee (\psi\land\neg\phi)$ is inconsistent then $\phi$ and $\psi$ are equivalent. Using Tableau Method it creates to branches one for $(\phi \land \neg\psi)$ in the left side and one for $(\psi\land\neg\phi)$ in the right side.

I tried the left side in the following way but it didn't lead to a closed tree, is there something wrong?

$1. \exists x P(x) \rightarrow \forall x \exists y R(x,y)$

$2. \neg \forall z \forall x \exists y (R(z,y) \lor \neg P(x))$

$3. \exists z \exists x \forall y \neg (R(z,y) \lor \neg P(x))$ --- from 2

$4. \forall y \neg (R(a,y) \lor \neg P(b))$ --- from 3, eliminating z and x (a,b are new)

$5. \forall y (\neg R(a,y) \land P(b))$ --- from 4

$6. P(c) \rightarrow \forall x R(x,d)$ --- from 1, eliminating x,y (c,d are new)

$6L. \neg P(c)$

$6R. \forall x R(x,d)$

$6R1. R(a,d)$

$6R2. \neg R(a,d) \land P(b)$ -- from 5

$6R3. \neg R(a,d)$ -- from 6R2

$6R4. P(b)$ -- from 6R2

$6R \bigotimes\bigotimes$ $R(a,d)$ and $\neg R(a,d)$ appeared in right side so it is closed

But in the left side (I mean $6L$) we have $\neg P(c)$ since there is no universal quantifier on $P$, there is no way to get $P(c)$ so the left side is not closed, it means the tree is not closed so the two original formulas are not equivalent! while Mauro ALLEGRANZA proved they are equivalent.

Is there anything wrong with my reasoning?!!

  • 2
    $\begingroup$ Step 6 is wrong; first you have to apply the $\to$ rule, because the main connective is $\to$ separating the two branches, and then apply the quantifier rules : one at the time, i.e. first on the branch with $\lnot \exists P(x)$ and then on the other branch with ∀x∃yR(x,y) that has ∀x as outer quantifier and you cannot skip it... $\endgroup$ – Mauro ALLEGRANZA Mar 1 '15 at 14:56
  • $\begingroup$ If I do what you said, then it results $\forall \neg P(x)$ and there will be a contradiction with line number $4$ so this branch is a contradiction as well. I didn't know that we must apply the connective first, then applying the quantifier rules, that works.thanks a lot. $\endgroup$ – No one Mar 1 '15 at 15:03
  • 1
    $\begingroup$ When you "unpack" 1) you have to branch for $\to$; on the left you will find $\lnot ∃xP(x)$ and you have to apply the rule for $\lnot \exists$ that do not need a new variable. $\endgroup$ – Mauro ALLEGRANZA Mar 1 '15 at 15:10

Yes, you can prove it with "usual" proof systems : Resolution, Tableaux or with Natural Deduction :

1) $∀z∀x∃y(R(z,y)∨¬P(x))$ --- premise

2) $∃xP(x)$ --- assumed [a]

3) $P(w)$ --- assumed [b] for $\exists$-elimination

4) $∃y(R(z,y)∨¬P(w))$ --- from 1) by $\forall$-elimination twice

5) $R(z,y)∨¬P(w)$ --- assumed [c] for $\exists$-elimination

6) $P(w) \to R(z,y)$ --- from 5) by tautological equivalence : $(p \to q) \leftrightarrow (\lnot p \lor q)$

7) $R(z,y)$ --- from 3) and 6) by $\to$-elimination

8) $\exists yR(z,y)$ --- from 7) by $\exists$-introduction

9) $\forall x \exists yR(x,y)$ --- from 8) by $\forall$-introduction : $x$ is not free in any "open" assumptions

$y$ is not free in 9); thus, we can apply $\exists$-elimination with 4), 5) and 9) and conclude with :

10) $\forall x \exists yR(x,y)$, discharging assumption [c].

In the same way, from 2), 3) and 10), discharging assumption [b] and concluding with :

11) $\forall x \exists yR(x,y)$.

Finally :

$∃xP(x) \to \forall x \exists yR(x,y)$ --- from 2) and 11) by $\to$-introduction, discharging assumption [a].

With a final application of $\to$-introduction we conclude with : $∀z∀x∃y(R(z,y)∨¬P(x)) \to (∃xP(x) \to ∀x∃yR(x,y))$.

  • $\begingroup$ Thanks you very much, From what I know Tableaux Method is used to show whether a set of formulas are inconsistent then we are looking for closed paths. if the tree is closed then the formulas are inconsistent. I would like to know how closed paths are relevant to equivalence of formulas? $\endgroup$ – No one Mar 1 '15 at 8:25
  • 1
    $\begingroup$ @Drupalist - $\phi \leftrightarrow \psi$ is simply : $(\phi \to \psi) \land (\psi \to \phi)$. Thus apply Tableaux to negation of the last formula and if all paths will close then the original formula is valid. $\endgroup$ – Mauro ALLEGRANZA Mar 1 '15 at 8:37
  • $\begingroup$ So $\phi$ and $\psi$ are equivalent if $\phi \rightarrow \psi$ and $\neg (\psi \rightarrow \phi)$ are inconsistent, right? $\endgroup$ – No one Mar 1 '15 at 8:44
  • 1
    $\begingroup$ @Drupalist - YES. $\endgroup$ – Mauro ALLEGRANZA Mar 1 '15 at 9:22
  • $\begingroup$ Thank you very much, your useful comments and answers are very helpful for me. $\endgroup$ – No one Mar 1 '15 at 9:27

I'll try to write down the tree :

$1. \exists x P(x) \rightarrow \forall x \exists y R(x,y)$ --- premise

$2. \neg \forall z \forall x \exists y (R(z,y) \lor \neg P(x))$ --- the negation of the conclusion

$3. \exists z \exists x \forall y \neg (R(z,y) \lor \neg P(x))$ --- from 2

$4. \forall y \neg (R(a,y) \lor \neg P(b))$ --- from 3, by rule for $\exists$, with $a,b$ new

$5. \forall y (\neg R(a,y) \land P(b))$ --- from 4

$6_L. \neg \exists xP(x)$ --- from 1, by rule for $\to$

$6_R. \forall x \exists yR(x,y)$ --- from 1, by rule for $\to$

Now I'll expand the left branch :

$7. \neg P(a)$ --- from $6_L$, by the rule for $\neg \exists$

$8. \neg P(b)$ --- from $6_L$, by the rule for $\neg \exists$ : we have to use all the constants already introduced

$9. \neg R(a,a) \land P(b)$ --- from 5, by the rule for $\forall$

$10. \neg R(a,b) \land P(b)$ --- from 5, by the rule for $\forall$ : : we have to use all the constants already introduced

Now, applying the $\land$ rule to both $9, 10$ we have :

$11. \neg R(a,a)$

$12. \neg R(a,b)$

$13. P(b)$

and the path closes by $8$ and $13$.

Now I'll expand the right branch :

$14. \exists yR(a,y)$ --- from $6_R$, by the rule for $\forall$

$15. \exists yR(b,y)$ --- from $6_R$, by the rule for $\forall$ : we have to use all the constants already introduced

$16. R(a,c)$ --- from 14, $c$ new

$17. R(a,d)$ --- from 15, $d$ new

Now, as in the left branch, we have to analyze 5 : as above the rule for $\forall$ must be applied to all the constants already introduced : $a,b,c,d$. Thus, the path will contain :

$18. P(b)$

$19. \neg R(a,a)$

$20. \neg R(a,b)$

$21. \neg R(a,c)$

$22. \neg R(a,d)$

and also this path closes.

Both paths are closed, showing that the premise and the negation of the conclusion are inconsistent, i.e. that:

$$(\exists x P(x) \rightarrow \forall x \exists y R(x,y)) \to (\forall z \forall x \exists y (R(z,y) \lor \neg P(x)))$$

is valid.

  • $\begingroup$ Thank you very much, I missed to use all the constants already introduced. $\endgroup$ – No one Mar 1 '15 at 17:56
  • $\begingroup$ In a first order logic formula there are formulas which they have no $\exists$ quantifier, all we have is $\forall$. Since we have to replace $\forall$ quantifiers with already defined constant (via eliminating $\exists$), when there is no $\exists$ then what constant should be replaced with $\forall$? $\endgroup$ – No one Mar 3 '15 at 7:12
  • 1
    $\begingroup$ @Drupalist - if you have to apply the $\forall$ rule first and no constants are already available, you are licensed to introduced a new one. This is consistent with the "standard" assumption of first-order logic semantics that the doamin of interpretation is not-empty, i.e. there is always at least one objcet in it. $\endgroup$ – Mauro ALLEGRANZA Mar 3 '15 at 7:15

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.