Biconditional Elimination/Proof Rule/Tableau Form

From ProofWiki
Jump to navigation Jump to search

Proof Rule

Let $\phi \iff \psi$ be a propositional 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}$.