Using a statement to prove its converse

Question

Suppose that we use $P\implies Q$ in a proof of its converse $Q\implies P$. If we can then establish by other means that $P\implies Q$ is true, does this mean that we have proved $P\iff Q$? Or is the first proof faulty in some regard for having used an implication in the proof of its own converse?

Answer 1

To assume the converse of an implication when trying to prove the implication is not only not faulty, it is actually an admissible proof technique: if you have proved $(P \implies Q) \implies (Q \implies P)$, then you can prove $Q \implies P$ regardless of whether $P \implies Q$ is provable or not. To see this, either reason thus in natural deduction style:

1. $(P \implies Q) \implies (Q \implies P)$ (assumption)
2. $Q$ (assumption)
3. $P \implies Q$ (2, $\implies$-introduction discharging the (non-existent) assumption $P$)
4. $Q \implies P$ (1, 3, $\implies$-elimination)
5. $P$ (2, 4, $\implies$-elimination)
6. $Q \implies P$ (5, $\implies$-introduction discharging assumption 2)
7. $((P \implies Q) \implies (Q \implies P)) \implies (Q \implies P)$ (6, $\implies$-introduction discharging assumption 1).

or draw up the truth table for the formula in step 7.

So at the end of your first proof, you can conclude that $Q \implies P$ with no assumption. Then if you can prove $P \implies Q$, you have proved $P \iff Q$.