Biconditional elimination

From Infogalactic: the planetary knowledge core
Jump to: navigation, search

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)}


\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)


(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


  1. Cohen, S. Marc. "Chapter 8: The Logic of Conditionals" (PDF). University of Washington. Retrieved 8 October 2013.<templatestyles src="Module:Citation/CS1/styles.css"></templatestyles>