Proof by Contradiction/Proof Rule/Tableau Form

From ProofWiki
Jump to navigation Jump to search

Proof Rule

Let $\phi$ be a well-formed 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 \II$