Biconditional Elimination

Give that the biconditional means that if \(P\) is the case, \(Q\) must be the case and if \(Q\) is the case, \(P\) must be the case, if we have \(P \leftrightarrow Q\) and \(P\), we can derive \(Q\) and vice versa.

Strategies for constructing proofs in propositional logic
- Now we just need to get \(D\) from the proposition at line 3. This is easy since we already have access to the consequent of the biconditional at line 1. Therefore we can apply Biconditional Elimination) at line 3 to get \(D\). We are now halfway there:
- Actually, if we look more closely, there is a better approach. The target proposition is contained in the first premise as the consequent to the biconditional (\(\lnot L \leftrightarrow [X \land (\lnot S \lor B)]\)). A better approach is therefore to seek to derive the antecedent (\(\lnot L\)) and then use Biconditional Elimination to extract the target sentence which is the consequent.
Formal proofs in propositional logic
- Biconditional Elimination