Equivalence of first order logic formulas

Question

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?

---

UPDATE:

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

Answer 1

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))$.

Answer 2

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.