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?!!
Best Answer
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 :
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))$.