Proof by Contradiction/Proof Rule
Proof Rule
Proof by Contradiction is a valid deduction sequent in propositional logic.
As a proof rule it is expressed in the form:
- If, by making an assumption $\phi$, we can infer a contradiction as a consequence, then we may infer $\neg \phi$.
- The conclusion does not depend upon the assumption $\phi$.
It can be written:
- $\displaystyle{\begin{array}{|c|} \hline \phi \\ \vdots \\ \bot \\ \hline \end{array} \over \neg \phi} \ \textrm{PBC}$
Tableau Form
Let $\phi$ be a propositional formula in a tableau proof.
The Proof by Contradiction is invoked for $\phi \vdash \bot$ in the following manner:
Pool: | The pooled assumptions of $\bot$ | |||||||
Formula: | $\neg \phi$ | |||||||
Description: | Proof by Contradiction | |||||||
Depends on: | The series of lines from where the assumption $\phi$ was made to where $\bot$ was deduced | |||||||
Discharged Assumptions: | The assumption $\phi$ is discharged | |||||||
Abbreviation: | $\text{PBC}$ or $\neg \mathcal I$ |
Explanation
Proof by Contradiction can be expressed in natural language as follows:
If we know that by making an assumption $\phi$ we can deduce a contradiction, then it must be the case that $\phi$ cannot be true.
Thus it provides a means of introducing a negation into a sequent.
Also known as
Proof by Contradiction is also known as not-introduction, and can be seen abbreviated as $\neg \mathcal I$ or $\neg_i$.
However, there are technical reasons why this form of abbreviation are suboptimal on this website, and PBC (if abbreviation is needed at all) is to be preferred.
It is also known as proof of negation, i.e., proof that some (positive!) assumption is not true.
Some sources do not explicitly distinguish between Proof by Contradiction and Reductio ad Absurdum, which starts with a negative assumption ($\neg \phi$).
Both can be referred to as indirect proof, but Reductio ad Absurdum is rejected by the intuitionistic school.
Technical Note
When invoking Proof by Contradiction in a tableau proof, use the Contradiction template:
{{Contradiction|line|pool|statement|start|end}}
where:
line
is the number of the line on the tableau proof where the Proof by Contradiction 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$
- 1980: D.J. O'Connor and Betty Powell: Elementary Logic ... (previous) ... (next): $\S \text{II}$: The Logic of Statements $(2): \ 8$: Indirect proof
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.2.1$: Rules for natural deduction