I'm a little confused about the difference between these two types of proof. As I have been taught them, it seems like proofs by contrapositive are just a subset of proofs by contradiction.
Say we want to prove $P \implies Q$. Here is how I've been taught to use both proofs:
Contrapositive: We assume $\lnot Q$ and from this we try to conclude $\lnot P$.
Contradiction: We assume $P$ and $\lnot Q$ and from this we try to deduce a contradiction.
My question is, let say we proved $P \implies Q$ by contrapositive, so we proved $\lnot Q \implies \lnot P$. Wouldn't this be equivalent to assuming $P$ and $\lnot Q$ and then use $\lnot Q$ to prove $\lnot P$, so we would deduce the contradiction $P \land \lnot P$?
Best Answer
The two approaches are not equivalent, even if they are quite similar and related. More precisely, proofs by contrapositive are a proper subset of proofs by contradiction.
Every proof by contraposition can be reformulated as a proof by contradiction, as you correctly noticed. Indeed, suppose you have a proof $\pi$ of $\lnot Q \implies \lnot P$; then you can prove $P \implies Q$ by contradiction, by assuming $P$ and $\lnot Q$, which yields a proof of $\lnot P$ (via modus ponens between the assumption $\lnot Q$ and the conclusion $\lnot Q \implies \lnot P$ of $\pi$) and then you get the contradiction $P \land \lnot P$.
But not every proof by contradiction can be reformulated as a proof by contraposition, as well explained in the accepted answer of this question. Indeed, proofs by contradiction are "more general" (i.e. they can be applied to a wider set of propositions to prove) because you can stop when you find any contradiction, not only a contradiction directly involving the hypotheses. More precisely, in a proof by contradiction of $P \implies Q$, we assume $P$ and $\lnot Q$ and we deduce a contradiction $R \land \lnot R$; in the particular case where $R = P$ then (usually) you can reformulate your proof as a proof by contraposition, otherwise you cannot.
Remark. Both proofs by contraposition and proofs by contradiction are valid in classical logic, but in general they are not valid in intuitionistic logic (roughly speaking, a constructive logic that does not admit the excluded middle law). For a more detailed analysis of the validity of these kinds of proofs, see for instance here.