Biconditional Elimination/Proof Rule/Tableau Form
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}$.