Equivalence relation using tableaux How can I prove that two formulae are equivalent using analytic tableaux? For example, how can I prove the following theorem?
$$ (p \rightarrow q) \equiv (\neg q \rightarrow \neg p)$$
 A: In using tableaux (I've also heard them called truth-trees (as opposed to truth tables)) to prove a sentence $\phi$, we can start with $\lnot\phi$ and show that every branch (a potential way of satisfying $\lnot\phi$) leads to a contradiction.  If every potential way of satisfying $\lnot\phi$ is a contradiction, then $\phi$ must be true.
I'd suggest that in using the tableaux for equivalences, you replace $\phi \equiv \psi$ with $(\phi \to \psi) \land (\psi \to \phi)$.  I'd also suggest that you allow two “shortcuts” for convenience.  The first is that a conditional $\phi \to \psi$ is equivalent to the disjunction $\lnot\phi \lor \psi$, so when a branch has $\phi \to\psi$, it can split with $\lnot\phi$ on one side, and $\psi$ on the other.  The second shortcut is that a negated conditional $\lnot(\phi\to\psi)$ is logically equivalent to $\phi \land \lnot\psi$, and this can be expanded in place, too.  I will also presume that we can move between $\lnot\lnot\phi$ and $\phi$ without making note of it. Using these shortcuts, we can construct a tree for your formula.  This isn't quite the tree presentation that is usually shown (because I don't know how to render that in MathJax), but it should be close enough that you can see the structure.
$$\frac{
\begin{array}{c}
 \lnot[ (p \to q) \equiv (\lnot q \to \lnot p) ] \\
 \lnot[ ((p \to q) \to (\lnot q \to \lnot p)) \land ((\lnot q \to \lnot p) \to (p \to q))] \\
\lnot((p \to q) \to (\lnot q \to \lnot p)) \lor \lnot((\lnot q \to \lnot p) \to (p \to q)) \end{array}
}{\displaystyle
\frac{
\begin{array}{c}
\lnot((p \to q) \to (\lnot q \to \lnot p)) \\
\lnot(\lnot q \to \lnot p) \\
\lnot q \\
p \\
p \to q
\end{array}}{
\begin{array}{c}
\lnot p \\
\bot
\end{array}
\qquad
\begin{array}{c}
q \\
\bot \\
\end{array}}
\qquad
\frac{
\begin{array}{c}
\lnot((\lnot q \to \lnot p) \to (p \to q)) \\
\lnot(p \to q) \\
p \\
\lnot q \\
\lnot q \to \lnot p
\end{array}
}{
\begin{array}{c}
q \\
\bot
\end{array}
\qquad
\begin{array}{c}
\lnot p \\
\bot
\end{array}
}
}
$$
Since all the branches terminate, $\lnot[ (p \to q) \equiv (\lnot q \to \lnot p) ]$ is unsatisfiable, which means that the following sentence is a theorem.
$$(p \to q) \equiv (\lnot q \to \lnot p)$$
If that notation isn't quite clear, here's a more linear presentation that might help. 


*

*$\lnot[ (p \to q) \equiv (\lnot q \to \lnot p) ]$

*$\lnot[ ((p \to q) \to (\lnot q \to \lnot p)) \land ((\lnot q \to \lnot p) \to (p \to q))]$

*$\lnot((p \to q) \to (\lnot q \to \lnot p)) \lor \lnot((\lnot q \to \lnot p) \to (p \to q))$

*
*

*Branch for $\lnot((p \to q) \to (\lnot q \to \lnot p))$ from 3.


*
*

*$(p \to q)$


*
*

*$\lnot(\lnot q \to \lnot p)$


*
*

*$\lnot q$


*
*

*$p$


*
*

*
*

*Branch for $\lnot p$ from 5.



*
*

*
*

*$\bot$ from $p, \lnot p$, end branch



*
*

*
*

*Branch for $q$ from 5.



*
*

*
*

*$\bot$ from $q, \lnot q$, end branch



*
*

*Branch for $\lnot((\lnot q \to \lnot p) \to (p \to q))$ from 3.


*
*

*$\lnot q \to \lnot p$


*
*

*$\lnot(p \to q)$


*
*

*$p$


*
*

*$\lnot q$


*
*

*
*

*Branch for $q$ from 14.



*
*

*
*

*$\bot$ from $q, \lnot q$, end branch



*
*

*
*

*Branch for $\lnot p$ from 14.



*
*

*
*

*$\bot$ from $p, \lnot p$, end branch



A: Your class probably defines 
$A\equiv B$ as  $(A\to B)\land (B\to A)$, so you can treat it that way for the tableau.  
A: Is this what you need? I don't understand what you want.

