Now we use T7 to justify the following rule.
- Modus Tollens (MT)
Modus Tollens is also sometimes known as 'Denying the Consequent'. Note that the following is not an instance of Modus Tollens, at least as defined above.
The premise lines of Modus Tollens are a conditional and the negation of its consequent. The premise lines of this inference are a conditional and the opposite of its consequent, but not the negation of its consequent. The desired inference here needs to be derived as below.
Of course, it is possible to prove as a theorem:
Then you can add a new inference rule—or, more likeley, a new form of Modus Tollens—on the basis of this theorem. However, we won't do that here.