# Modus Tollendo Tollens/Proof Rule

## Proof Rule

The Modus Tollendo Tollens is a valid deduction sequent in propositional logic.

As a proof rule it is expressed in the form:

If we can conclude $\phi \implies \psi$, and we can also conclude $\neg \psi$, then we may infer $\neg \phi$.

It can be written:

$\displaystyle {\phi \implies \psi \quad \neg \psi \over \neg \phi} \text{MTT}$

### Tableau Form

Let $\phi \implies \psi$ be a propositional formula in a tableau proof whose main connective is the implication operator.

The Modus Tollendo Tollens is invoked for $\phi \implies \psi$ and $\neg \psi$ as follows:

 Pool: The pooled assumptions of $\phi \implies \psi$ The pooled assumptions of $\neg \psi$ Formula: $\neg \phi$ Description: Modus Tollendo Tollens Depends on: The line containing the instance of $\phi \implies \psi$ The line containing the instance of $\neg \psi$ Abbreviation: $\text{MTT}$

## Explanation

The Modus Tollendo Tollens can be expressed in natural language as:

If the truth of one statement implies the truth of a second, and the second is shown not to be true, then neither can the first be true.

## Also known as

Modus Tollendo Tollens is also known as:

• Modus tollens
• Denying the consequent.

## Linguistic Note

Modus Tollendo Tollens is Latin for mode that by denying, denies.

The shorter form Modus Tollens means mode that denies.

## Technical Note

When invoking Modus Tollendo Tollens in a tableau proof, use the {{ModusTollens}} template:

{{ModusTollens|line|pool|statement|first|second}}

or:

{{ModusTollens|line|pool|statement|first|second|comment}}

where:

line is the number of the line on the tableau proof where Modus Tollendo Tollens is to be invoked
pool is the pool of assumptions (comma-separated list)
statement is the statement of logic that is to be displayed in the Formula column, without the $...$ delimiters
first is the first of the two lines of the tableau proof upon which this line directly depends, the one in the form $\phi \implies \psi$
second is the second of the two lines of the tableau proof upon which this line directly depends, the one in the form $\phi$
comment is the (optional) comment that is to be displayed in the Notes column.