Biconditional elimination

From HandWiki
Short description: Inference in propositional logic
Biconditional elimination
TypeRule of inference
FieldPropositional calculus
StatementIf [math]\displaystyle{ P \leftrightarrow Q }[/math] is true, then one may infer that [math]\displaystyle{ P \to Q }[/math] is true, and also that [math]\displaystyle{ Q \to P }[/math] 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 [math]\displaystyle{ P \leftrightarrow Q }[/math] is true, then one may infer that [math]\displaystyle{ P \to Q }[/math] is true, and also that [math]\displaystyle{ Q \to P }[/math] 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:

[math]\displaystyle{ \frac{P \leftrightarrow Q}{\therefore P \to Q} }[/math]


[math]\displaystyle{ \frac{P \leftrightarrow Q}{\therefore Q \to P} }[/math]

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

Formal notation

The biconditional elimination rule may be written in sequent notation:

[math]\displaystyle{ (P \leftrightarrow Q) \vdash (P \to Q) }[/math]


[math]\displaystyle{ (P \leftrightarrow Q) \vdash (Q \to P) }[/math]

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

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

[math]\displaystyle{ (P \leftrightarrow Q) \to (P \to Q) }[/math]
[math]\displaystyle{ (P \leftrightarrow Q) \to (Q \to P) }[/math]

where [math]\displaystyle{ P }[/math], and [math]\displaystyle{ Q }[/math] are propositions expressed in some formal system.

See also