Modus Tollens - Formal Notation

Formal Notation

The modus tollens rule may be written in sequent notation:

where is a metalogical symbol meaning that is a syntactic consequence of and in some logical system;

or as the statement of a functional tautology or theorem of propositional logic:

where, and are propositions expressed in some logical system;

or including assumptions:

though since the rule does not change the set of assumptions, this is not strictly necessary.

More complex rewritings involving modus tollens are often seen, for instance in set theory:

("P is a subset of Q. x is not in Q. Therefore, x is not in P.")

Also in first-order predicate logic:

("For all x if x is P then x is Q. There exists some x that is not Q. Therefore, there exists some x that is not P.")

Strictly speaking these are not instances of modus tollens, but they may be derived using modus tollens using a few extra steps.