Biconditional Elimination/Proof Rule/Tableau Form

From ProofWiki
Jump to navigation Jump to search

Proof Rule

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

Biconditional Elimination is invoked for $\phi \iff \psi$ in either of the two forms:


Form 1
Pool:    The pooled assumptions of $\phi \iff \psi$      
Formula:    $\phi \implies \psi$      
Description:    Biconditional Elimination      
Depends on:    The line containing $\phi \iff \psi$      
Abbreviation:    $\mathrm {BE}_1$ or $\iff \EE_1$      


Form 2
Pool:    The pooled assumptions of $\phi \iff \psi$      
Formula:    $\psi \implies \phi$      
Description:    Biconditional Elimination      
Depends on:    The line containing $\phi \iff \psi$      
Abbreviation:    $\mathrm {BE}_2$ or $\iff \EE_2$      


Also denoted as

Sources which refer to this rule as the biconditional-conditional rule may as a consequence give the abbreviation $\mathrm {BC}$.