6 added 2 characters in body

They are trivially equivalent. The contrapositive of (P → Q) is (¬Q → ¬P). This is equivalent to (¬Q → (P → ⊥)), which is a curried form of (¬Q ∧ P) → ⊥.

Edit: I'm not sure about your added comment. Reductio seems the more general proof technique to me (as Anweshi mentions, it works for statements which are not implications); contraposition seems less useful unless the contrapositive form ¬Q → ¬P is especially natural or intuitive.

Edit 2: These transformations would seem to be intuitionistically valid, with the proviso that a "proof by contradiction of (P → Q)" is only a proof of (P → ¬¬Q). Hence, the contrapositive (¬Q → ¬P) is strictly weaker than (P → Q).

On a further note, it is often the case that the antecedent P can be naturally seen as a negative statement (¬P'). In these cases, we may be able to provide a proof of (¬Q → P'). This may be the case of a proof by contrapositive which is a "direct proof", possibly accounting for J. Polak's remarks.

Edit 4: JD Hamkins points out that direct proofs often provide useful proofs of intermediate statements, while whereas proofs by contradictions do not. But this technique can be generalized by pushing contradictory "contexts" to the very end of the proof: i.e. one can say: "We will prove a contradiction by assuming P, Q, R and S. From P, R and S we obtain the following lemmas..." It's not clear that all such proofs can be naturally stated as proofs by contrapositive.

5 added 471 characters in body

They are trivially equivalent. The contrapositive of (P → Q) is (¬Q → ¬P). This is equivalent to (¬Q → (P → ⊥)), which is a curried form of (¬Q ∧ P) → ⊥.

Edit: I'm not sure about your added comment. Reductio seems the more general proof technique to me (as Anweshi mentions, it works for statements which are not implications); contraposition seems less useful unless the contrapositive form ¬Q → ¬P is especially natural or intuitive.

Edit 2: These transformations would seem to be intuitionistically valid, with the proviso that a "proof by contradiction of (P → Q)" is only a proof of (P → ¬¬Q). Hence, the contrapositive (¬Q → ¬P) is strictly weaker than (P → Q).

On a further note, it is often the case that the antecedent P can be naturally seen as a negative statement (¬P'). In these cases, we may be able to provide a proof of (¬Q → P'). This may be the case of a proof by contrapositive which is a "direct proof", possibly accounting for J. Polak's remarks.

Edit 4: JD Hamkins points out that direct proofs often provide useful proofs of intermediate statements, while proofs by contradictions do not. But this technique can be generalized by pushing contradictory "contexts" to the very end of the proof: i.e. one can say: "We will prove a contradiction by assuming P, Q, R and S. From P, R and S we obtain the following lemmas..." It's not clear that all such proofs can be naturally stated as proofs by contrapositive.

4 added 313 characters in body

They are trivially equivalent. The contrapositive of (P → Q) is (¬Q → ¬P). This is equivalent to (¬Q → (P → ⊥)), which is a curried form of (¬Q ∧ P) → ⊥.

Edit: I'm not sure about your added comment. Reductio seems the more general proof technique to me (as Anweshi mentions, it works for statements which are not implications); contraposition seems less useful unless the contrapositive form ¬Q → ¬P is especially natural or intuitive.

Edit 2: These transformations would seem to be intuitionistically valid, with the proviso that a "proof by contradiction of (P → Q)" is only a proof of (P → ¬¬Q). Hence, the contrapositive (¬Q → ¬P) is strictly weaker than (P → Q).

On a further note, it is often the case that the antecedent P can be naturally seen as a negative statement (¬P'). In these cases, we may be able to provide a proof of (¬Q P'). This may be the case of a proof by contrapositive which is a "direct proof", possibly accounting for J. Polak's remarks.

3 added 257 characters in body
2 added 292 characters in body
1