Can any proof by contrapositive be rephrased into a proof by contradiction?

From my understanding,

Proof by contrapositive: Prove $$P \implies Q$$, by proving that $$\neg Q \implies \neg P$$ since they are logically equivalent.

Proof by contradiction: Prove $$P \implies Q$$ by showing that $$P \wedge \neg Q$$ yields an absurdity and hence false. So $$\neg (P \wedge \neg Q)$$ is equivalent to $$\neg (\neg (P \implies Q))$$ and $$P \implies Q$$ by double negation so showing that $$\neg (P \wedge \neg Q)$$ proves $$P \implies Q$$.

If the absurdity derived during the procedure for a proof by contradiction is $$P \wedge \neg Q \implies\neg P$$, we have essentially already proven $$P \implies Q$$ by contrapositive since $$\neg Q \implies \neg P$$ is precisely the required condition for proof by contrapositive. But $$(P \wedge \neg Q) \implies \neg P$$ is also a contradictory statement which means that $$P \implies Q$$ must be true.

Now the question is this. Is this proof by contradiction still a valid form of proof even though its a proof by contrapositive in disguise? To me, this proof by contradiction also seems to be a valid proof as it does seem to satisfy the conditions(if they are correct) for proof by contradiction.

Additionally, if you have a contrapositive proof, so you have shown that $$\neg Q \implies \neg P$$, is it possible to rephrase this in a proof by contradiction by supposing that $$P \wedge \neg Q$$ instead of just $$\neg Q$$.

If this is the case, what is the point in distinguishing proof by contradiction from proof by contrapositive?

edit: My thought is that proof by contrapositive is a direct proof while proof by contradiction, in this case, depends on the validity of the double negation law which apparently isn't valid in intuitionistic logic.

• The $(\neg Q\implies\neg P)\implies(P\implies Q)$ direction of the equivalence also requires something like double negation elimination assuming you are starting from a reasonably typical constructive logic. – Derek Elkins Dec 26 '18 at 0:25
• If every proof by contrapositive can be rephrased into a proof by contradiction, why do so many mathematicians prefer proof by contrapositive when it can be shown that way? – Sei Sakata Dec 26 '18 at 0:29
• @SeiSakata sometimes rephrasing the problem in the contrapositive form makes the proof easier or adds some intuition to the statement. Sometimes it's merely a matter of preference. – CyclotomicField Dec 26 '18 at 0:33
• @spaceisdarkgreen But what we are discussing here is only in one direction. The statement that every proof by contrapositive can be rephrased into a proof by contradiction is seemingly true but the converse doesn't necessarily hold. I am not sure if you were referring to this in your comment" any proof by contradiction “can be rephrased” as a direct proof". BTW I said seemingly true since the line of reasoning that a proof by contrapositive can be rephrased into a proof by contradiction seems to be general enough to account for all cases. But I might be mistaken and not true at all. – Sei Sakata Dec 26 '18 at 1:33
• Sorry, I didn't read your definition of what you're calling a proof by contradiction carefully... you are right that contrapositive is a special case of contradiction here (coincidentally, I wrote an answer about precisely this a couple days ago math.stackexchange.com/questions/3050738/…). – spaceisdarkgreen Dec 26 '18 at 7:40

Yes it is valid... it doesn't really matter if it's something else 'in disguise', just that is it correct. And deriving $$\lnot P$$ from $$P\land\lnot Q$$ is certainly leads to a contradiction that implies $$\lnot (P\land \lnot Q)$$ is true, which implies that $$P\to Q$$ is true. One thing to note (that I think you have noticed based on your second question) is that you have an additional assumption of $$P$$ open and available for use when you derive $$\lnot P,$$ unlike in the case of just deriving $$\lnot Q\to \lnot P$$ by assuming $$\lnot Q$$ and deriving $$\lnot P.$$
So the second question amounts to whether it is admissible to assume $$P$$ in a proof of $$\lnot Q\to \lnot P.$$ It is, and the easiest way to see this is reasoning semantically and using the completeness/soundness theorem. If $$P\vdash \lnot Q\to \lnot P$$ then every interpretation in which $$P$$ is true has $$Q$$ true, which means precisely the same thing as $$\vdash P\to Q,$$ so we have $$\vdash \lnot Q\to \lnot P.$$
As a result, proof by contrapositive is essentially a special case of what you're calling proof by contradiction, where the contradiction takes the special form $$\lnot P$$ contradicting with $$P.$$
I think the reason you might have seen framing contrapositive proofs as proofs by contradiction discouraged is for style reasons. Unless the outstanding assumption of $$P$$ is used (unnecessarily), the part of the proof outside the inner proof of $$\lnot Q\to \lnot P$$ is just boilerplate that can be omitted. It is also more informative to call it a proof by contrapositive since that is a special case of contradiction.