Is Modus Tollens just an implied Modus Ponens on the Contrapositive? In propositional logic, you must explicitly state each transformation even when they are obvious, like resolving double negatives.
Insufficient
1 P -> Q   Hypothesis
2 --P      Hypothesis
∴ Q        Modus Ponens 1,2 # <- this implicitly relies on --P == P

Sufficient
1 P -> Q  Hypothesis
2 --P     Hypothesis
3 P       Double Negation 2 # <- explicitly resolve the double negation before using it
∴ Q       Modus Ponens 1,3

However, it seems like we might be allowing an implicit step in the case of Modus Tollens. Modus Tollens can be seen as simply Modus Ponens applied on the contrapositive.
Standard Modus Tollens
1 P -> Q   Hypothesis
2 -Q       Hypothesis
∴ -P       Modus Tollens 1,2

But is this not implicitly relying on the fact that P -> Q == -Q -> -P in the same way that the double negative example implicitly relied on the fact that --P == P? We can express the argument purely in terms of Modus Ponens by explicitly stating the contrapositive.
1 P -> Q   Hypothesis
2 -Q -> -P Contrapositive 1
3 -Q       Hypothesis
∴ -P       Modus Ponens 2,3

Is this more explicit? Is Modus Tollens simply a derivation of Modus Ponens and Contrapositive, or do they merely happen to correspond? (identity-vs-value equality distinction). Does Modus Ponens have a more fundamental ontological status, or are they equally derivable in terms of each other?
 A: It is good to recognize the close connections that different inference patterns have to each other as it deepens one's understanding of logical concepts and principles. However, I would discourage you from seeing certain rules as 'just an applied application' of some other rule.
Yes, Modus Ponens and Modus Tollens are closely related, but they are also each their own distinct pattern. And why would I see Modus Tollens as just an implied Modus Ponens, if I can regard Modus Ponens as just an implied Modus Tollens?  Or maybe I should regard both rules as just implied versions of Disjunction Syllogism:
Modus Ponens is just implied Disjunctive Syllogism:
$1. P \to Q \text{ given}$
$2. P \text{ given}$
$3. \neg P \lor Q \text{ Implication } 1$
$4. \neg \neg P \text{ Double Negation } 2$
$5. Q \text{ Disjunctive Syllogism } 3,4$
Modus Tollens is just implied Disjunctive Syllogism:
$1. P \to Q \text{ given}$
$2. \neg Q \text{ given}$
$3. \neg P \lor Q \text{ Implication } 1$
$4. \neg P \text{ Disjunctive Syllogism } 2,3$
Or maybe I should regard Disjunctive Syllogism as just implied Modus Ponens?
$1. P \lor Q \text{ given}$
$2. \neg P \text{ given}$
$3. \neg \neg P \lor Q \text{ Double Negation }12$
$4. \neg P \to Q \text{ Implication } 3$
$5. Q \text{ Modus Ponens } 3,4$
The point is: once you go down this road as seeing certain rules as 'just implied' applications of other rules, you find that you can play that game in many, many different ways, and there seems little reason to prefer to do it one way or the other.  So, it's best to just recognize the connections as they exist, and leave it at that.
A: Wikipedia explicitly states that

*

*modus tollens can always be rewritten as modus ponens plus contrapositive (it calls the latter transposition)

*modus ponens can always be rewritten as modus tollens plus contrapositive

Thus if you treat modus ponens and contrapositive as axioms, then modus tollens is a derived rule. We write it in one step for the sake of conciseness, and expanding it would make the proof less explicit and more obscure.
But if you treat modus tollens and contrapositive as axioms, modus ponens is a derived rule. Hence modus ponens and tollens are equally derivable in a pure sense — the reason modus ponens is often listed first is because its implication aligns with the "arrow of time", our natural train of thought.
