Generally speaking, I'd like to know whether it is possible to reduce using only syntactic means any tautology to some basic tautology, say, for example, the principle of non contradiction. Can this possibility be proved?
More specifically, I'd like to know whether the following transformation of the "modus tollens" law really counts as a proof that this law is a tautology. I think this transformation proves that it has the same form as the tautology ~ (X&~X), but does it actually prove that the modus tollens law is really equivalent to the principle of non-contradiction, and thus , a tautology ?
[ (A--> B) & ~B ] --> ~A
<-> ~ [ (A --> B) & ~B & ~ ~A ]
<-> ~ [ (A --> B) & ~B & A ]
<-> ~ [ ~ (A & ~B) & (A & ~ B) ]
<-> ~ [ (A & ~B ) & ~ (A & ~B) ]
If I set, X = (A& ~B) then the modus ponens law is equivalent to ~ (X & ~ X).
But the equivalence holds apparently under a condition ( namely if X = (A & ~B) ), not absolutely.
Anything of the form $\neg (X \land \neg X)$ is a tautology. That is, $\neg (X \land \neg X)$ is always true, no matter whether $X$ is an atomic variable, or some complex statement like $(A \land \neg B)$. This is because any statement $X$ (atomic or complex) is true or false, and since $\neg X$ has the opposite truth-value, you get that $X \land \neg X$ is always false, and thus $\neg (X \land \neg X)$ is always true, making it a tautology.
So, your method of proving that Modus Ponens is a valid inference principle is correct.... and the proof itself is correct as well. Good job!