Reductio ad Absurdum/Proof Rule
Proof Rule
The reductio ad absurdum is a valid deduction sequent in propositional logic.
As a proof rule it is expressed in the form:
- If, by making an assumption $\neg \phi$, we can infer a contradiction as a consequence, then we may infer $\phi$.
- The conclusion does not depend upon the assumption $\neg \phi$.
It can be written:
- $\displaystyle {\begin{array}{|c|} \hline \neg \phi \\ \vdots \\ \bot \\ \hline \end{array} \over \phi} \textrm{RAA}$
Tableau Form
Let $\phi$ be a propositional formula in a tableau proof.
The Reductio ad Absurdum is invoked for $\neg \phi \vdash \bot$ in the following manner:
Pool: | The pooled assumptions of $\bot$ | |||||||
Formula: | $\phi$ | |||||||
Description: | Reductio ad Absurdum | |||||||
Depends on: | The series of lines from where the assumption $\neg \phi$ was made to where $\bot$ was deduced | |||||||
Discharged Assumptions: | The assumption $\neg \phi$ is discharged | |||||||
Abbreviation: | $\text{RAA}$ |
Explanation
Reductio ad Absurdum can be expressed in natural language as:
- If, by making an assumption that a statement is false , a contradiction can be deduced, that statement must in fact be true.
Linguistic Note
Reductio ad Absurdum is Latin for reduction to an absurdity.
Technical Note
When invoking Reductio ad Absurdum in a tableau proof, use the Reductio template:
{{Reductio|line|pool|statement|start|end}}
where:
line
is the number of the line on the tableau proof where the Reductio ad Absurdum is to be invokedpool
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$ ... $
delimitersstart
is the start of the block of the tableau proof upon which this line directly dependsend
is the end of the block of the tableau proof upon which this line directly depends
Sources
- 1964: Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning ... (previous) ... (next): $\text{I}$: 'NOT' and 'IF': $\S 3$
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.2.2$: Derived rules