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?
Wikipedia explicitly states that
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.