# Biconditional elimination

Short description: Inference in propositional logic
Type Rule of inference Propositional calculus If $\displaystyle{ P \leftrightarrow Q }$ is true, then one may infer that $\displaystyle{ P \to Q }$ is true, and also that $\displaystyle{ Q \to P }$ is true.

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 $\displaystyle{ P \leftrightarrow Q }$ is true, then one may infer that $\displaystyle{ P \to Q }$ is true, and also that $\displaystyle{ 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:

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

and

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

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

## Formal notation

The biconditional elimination rule may be written in sequent notation:

$\displaystyle{ (P \leftrightarrow Q) \vdash (P \to Q) }$

and

$\displaystyle{ (P \leftrightarrow Q) \vdash (Q \to P) }$

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

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

$\displaystyle{ (P \leftrightarrow Q) \to (P \to Q) }$
$\displaystyle{ (P \leftrightarrow Q) \to (Q \to P) }$

where $\displaystyle{ P }$, and $\displaystyle{ Q }$ are propositions expressed in some formal system.