Biconditional elimination

Inference in propositional logic

Biconditional elimination
Type	Rule of inference
Field	Propositional calculus
Statement	If $P\leftrightarrow Q$ is true, then one may infer that $P\to Q$ is true, and also that $Q\to P$ is true.
Symbolic statement	${\frac {P\leftrightarrow Q}{\therefore P\to Q}}$ ${\frac {P\leftrightarrow Q}{\therefore Q\to P}}$

Transformation rules
Propositional calculus
Rules of inference
Implication introduction / elimination (modus ponens) Biconditional introduction / elimination Conjunction introduction / elimination Disjunction introduction / elimination Disjunctive / hypothetical syllogism Constructive / destructive dilemma Absorption / modus tollens / modus ponendo tollens Negation introduction
Rules of replacement
Associativity Commutativity Distributivity Double negation De Morgan's laws Transposition Material implication Exportation Tautology
Predicate logic
Rules of inference
Universal generalization / instantiation Existential generalization / instantiation

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.^[1] 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 {P\leftrightarrow Q}{\therefore P\to Q}}

and

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

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.

References

^ Cohen, S. Marc. "Chapter 8: The Logic of Conditionals" (PDF). University of Washington. Archived (PDF) from the original on 2022-10-09. Retrieved 8 October 2013.