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?
$\endgroup$ 101 Answer
$\begingroup$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:
- $(P \implies Q) \implies (Q \implies P)$ (assumption)
- $Q$ (assumption)
- $P \implies Q$ (2, $\implies$-introduction discharging the (non-existent) assumption $P$)
- $Q \implies P$ (1, 3, $\implies$-elimination)
- $P$ (2, 4, $\implies$-elimination)
- $Q \implies P$ (5, $\implies$-introduction discharging assumption 2)
- $((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$.
$\endgroup$ 4
