Biconditional elimination

Biconditional elimination is the name of two valid rules of inference of propositional logic. It allows for one to infer a conditional from a biconditional. If $P \leftrightarrow Q$ is true, then one may infer that $P \to Q$ is true, and also that $Q \to P$ is true. For example, if it's true that I'm breathing if and only if I'm alive, then it's true that if I'm breathing, I'm alive; likewise, it's true that if I'm alive, I'm breathing. The rules can be stated formally as:

:$\frac$
and
:$\frac$

where the rule is that wherever an instance of "$P \leftrightarrow Q$" appears on a line of a proof, either "$P \to Q$" or "$Q \to P$" can be placed on a subsequent line;

Formal notation

The ''biconditional elimination'' rule may be written in sequent notation:
:$(P \leftrightarrow Q) \vdash (P \to Q)$
and
:$(P \leftrightarrow Q) \vdash (Q \to P)$

where $\vdash$ is a metalogical symbol meaning that $P \to Q$, in the first case, and $Q \to P$ in the other are syntactic consequences of $P \leftrightarrow Q$ in some logical system;

or as the statement of a truth-functional tautology or theorem of propositional logic:

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

where $P$, and $Q$ are propositions expressed in some formal system.

See also

* Logical biconditional

References

{{DEFAULTSORT:Biconditional Elimination
Rules of inference
Theorems in propositional logic