Biconditional elimination
| Type | Rule of inference |
|---|---|
| Field | Propositional calculus |
| Statement | 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. |
| Transformation rules |
|---|
| Propositional calculus |
| Rules of inference |
| Rules of replacement |
| Predicate logic |
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]
and
- [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]
and
- [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
References
- ↑ Cohen, S. Marc. "Chapter 8: The Logic of Conditionals". University of Washington. http://faculty.washington.edu/smcohen/120/Chapter8.pdf.
 |  |
