# Modus Ponendo Tollens/Proof Rule

## Proof Rule

Modus ponendo tollens is a valid argument in types of logic dealing with conjunctions $\land$ and negation $\neg$.

This includes propositional logic and predicate logic, and in particular natural deduction.

As a proof rule it is expressed in either of the two forms:

$(1): \quad$ If we can conclude $\map \neg {\phi \land \psi}$, and we can also conclude $\phi$, then we may infer $\neg \psi$.
$(2): \quad$ If we can conclude $\map \neg {\phi \land \psi}$, and we can also conclude $\psi$, then we may infer $\neg \phi$.

It can be written:

$\ds {\map \neg {\phi \land \psi} \quad \phi \over \neg \psi} \textrm{MPT}_1 \qquad \text{or} \qquad {\map \neg {\phi \land \psi} \quad \psi \over \neg \phi} \textrm{MPT}_2$

### Tableau Form

Let $\phi \land \psi$ be a well-formed formula in a tableau proof whose main connective is the conjunction operator.

The Modus Ponendo Tollens is invoked for $\neg \left({\phi \land \psi}\right)$ in either of the two forms:

Form 1
 Pool: The pooled assumptions of $\neg \left({\phi \land \psi}\right)$ The pooled assumptions of $\phi$ Formula: $\neg \psi$ Description: Modus Ponendo Tollens Depends on: The line containing the instance of $\neg \left({\phi \land \psi}\right)$ The line containing the instance of $\phi$ Abbreviation: $\text{MPT}_1$

Form 2
 Pool: The pooled assumptions of $\neg \left({\phi \land \psi}\right)$ The pooled assumptions of $\psi$ Formula: $\neg \phi$ Description: Modus Ponendo Tollens Depends on: The line containing the instance of $\neg \left({\phi \land \psi}\right)$ The line containing the instance of $\psi$ Abbreviation: $\text{MPT}_2$

### Explanation

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

If two statements cannot both be true, and one of them is true, it follows that the other one is not true.

## Linguistic Note

Modus Ponendo Tollens is Latin for mode that by affirming, denies.

## Technical Note

When invoking Modus Ponendo Tollens in a tableau proof, use the {{ModusPonendoTollens}} template:

{{ModusPonendoTollens|line|pool|statement|first|second|1 or 2}}

or:

{{ModusPonendoTollens|line|pool|statement|first|second|1 or 2|comment}}

where:

line is the number of the line on the tableau proof where Modus Ponendo 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 $\neg \left({\phi \land \psi}\right)$
second is the second of the two lines of the tableau proof upon which this line directly depends, the one in the form $\phi$ or $\psi$
1 or 2 should hold 1 for ModusPonendoTollens_1, and 2 for ModusPonendoTollens_2
comment is the (optional) comment that is to be displayed in the Notes column.