Biconditional elimination

Biconditional elimination is a valid rule of inference in propositional logic that allows one to infer a conditional statement from a biconditional statement. Specifically, it dictates that if a biconditional $P \leftrightarrow Q$ is true, then both of the corresponding conditionals, $P \to Q$ and $Q \to P$, must also be true. This rule is fundamental in formal proofs and logical deductions, serving as the converse to biconditional introduction.

Formal Notation

The biconditional elimination rule can be expressed in two distinct forms, often referred to as left elimination and right elimination, depending on which conditional is being derived.

In rule form, the two variations are written as:

$$ \frac{P \leftrightarrow Q}{P \to Q} $$

and

$$ \frac{P \leftrightarrow Q}{Q \to P} $$

where the presence of $P \leftrightarrow Q$ on the top line indicates that it is a premise, and the bottom line represents the logical conclusion that can be derived from it.

In sequent notation, the rules are expressed as:

$$ (P \leftrightarrow Q) \vdash (P \to Q) $$

and

$$ (P \leftrightarrow Q) \vdash (Q \to P) $$

where $\vdash$ is the metalogical symbol meaning that the expression on the right is a syntactic consequence of the expression on the left within a given logical system.

Truth Table Justification

The validity of biconditional elimination can be easily verified using a truth table. A biconditional statement $P \leftrightarrow Q$ is true if and only if both $P$ and $Q$ have the same truth value (both true or both false).

| $P$ | $Q$ | $P \leftrightarrow Q$ | $P \to Q$ | $Q \to P$ |
|---|---|---|---|---|
| T | T | T | T | T |
| T | F | F | F | T |
| F | T | F | T | F |
| F | F | T | T | T |

By examining the rows where the premise $P \leftrightarrow Q$ is true (the first and fourth rows), it is evident that both $P \to Q$ and $Q \to P$ are also true in those exact same rows. Therefore, whenever the biconditional is true, the derived conditionals are guaranteed to be true, confirming the soundness of the elimination rules.

Application in Natural Deduction

In natural deduction systems, biconditional elimination is frequently used to break down complex logical equivalences into simpler, directional implications. When a proof establishes that two propositions are materially equivalent, a logician can apply this rule to utilize the forward implication ($P \to Q$) for modus ponens or the backward implication ($Q \to P$) for further deductions.

Because a biconditional is logically equivalent to the conjunction of two conditionals, $(P \to Q) \land (Q \to P)$, biconditional elimination is essentially a specialized application of conjunction elimination following the expansion of the biconditional.

Relationship to Biconditional Introduction

Biconditional elimination is the exact inverse of biconditional introduction. While biconditional elimination extracts individual conditionals from a biconditional, biconditional introduction combines two conditionals ($P \to Q$ and $Q \to P$) to form a single biconditional ($P \leftrightarrow Q$). Together, these rules establish the interdefinability of the biconditional connective and the conjunction of conditionals, highlighting the symmetric nature of logical equivalence in classical propositional logic.