Biconditional elimination explained

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:	(P \leftrightarrow Q)/(\therefore P \to Q) (P \leftrightarrow Q)/(\therefore Q \to P)

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:(P \leftrightarrow Q)/(\therefore P \to Q) and(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.

See also

• Logical biconditional

Notes and References

1. Web site: Cohen. S. Marc. Chapter 8: The Logic of Conditionals. https://ghostarchive.org/archive/20221009/http://faculty.washington.edu/smcohen/120/Chapter8.pdf . 2022-10-09 . live. University of Washington. 8 October 2013.