So, I have troubles grasping the tableaux method. Could someone please show me how to prove this?
Assumptions: $$(∃X)(s(a)\to p(X)),\qquad (∃X)(p(X)\to s(A)) $$
Prove using the tableaux method that $$(∃X)(s(a)\leftrightarrow p(X))$$
I know I should get rid of the implications and equivalence, but I am lost after that.
1) $∃x \ (s(a) \to p(x))$ --- 1st premise
2) $∃x \ (p(x) \to s(a))$ --- 2nd premise
3) $\lnot ∃x \ (s(a) \leftrightarrow p(x))$ --- negation of conclusion
4) $s(a) \to p(b)$ --- from 1)
5) $p(c) \to s(a)$ --- from 2)
6) $\lnot (s(a) \leftrightarrow p(b))$ --- from 3)
7) $\lnot (s(a) \leftrightarrow p(c))$ --- from 3)
Now we have to start unpacking the bi-conditionals:
From 6), left branch:
8) $s(a)$
9) $\lnot p(b)$.
From 6), right branch:
10) $\lnot s(a)$
11) $p(b)$.
and so on...