Principle of Non-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 Principle of Non-Contradiction is invoked for $\phi$ and $\neg \phi$ in the following manner:

Pool:    The pooled assumptions of $\phi$      
The pooled assumptions of $\neg \phi$      
Formula:    $\bot$      
Description:    Principle of Non-Contradiction      
Depends on:    The line containing the instance of $\phi$      
The line containing the instance of $\neg \phi$      
Abbreviation:    $\operatorname {PNC}$ or $\neg \EE$