Biconditional elimination

☆ Save On Wikipedia ↗
Biconditional elimination
TypeRule of inference
FieldPropositional calculus
StatementIf P ↔ Q {\displaystyle P\leftrightarrow Q} {\displaystyle P\leftrightarrow Q} is true, then one may infer that P → Q {\displaystyle P\to Q} {\displaystyle P\to Q} is true, and also that Q → P {\displaystyle Q\to P} {\displaystyle Q\to P} is true.
Symbolic statement
  • P ↔ Q ∴ P → Q {\displaystyle {\frac {P\leftrightarrow Q}{\therefore P\to Q}}} {\displaystyle {\frac {P\leftrightarrow Q}{\therefore P\to Q}}}
  • P ↔ Q ∴ Q → P {\displaystyle {\frac {P\leftrightarrow Q}{\therefore Q\to P}}} {\displaystyle {\frac {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 ↔ Q {\displaystyle P\leftrightarrow Q} {\displaystyle P\leftrightarrow Q} is true, then one may infer that P → Q {\displaystyle P\to Q} {\displaystyle P\to Q} is true, and also that Q → P {\displaystyle Q\to P} {\displaystyle 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 ↔ Q ∴ P → Q {\displaystyle {\frac {P\leftrightarrow Q}{\therefore P\to Q}}} {\displaystyle {\frac {P\leftrightarrow Q}{\therefore P\to Q}}} and P ↔ Q ∴ Q → P {\displaystyle {\frac {P\leftrightarrow Q}{\therefore Q\to P}}} {\displaystyle {\frac {P\leftrightarrow Q}{\therefore Q\to P}}} where the rule is that wherever an instance of " P ↔ Q {\displaystyle P\leftrightarrow Q} {\displaystyle P\leftrightarrow Q}" appears on a line of a proof, either " P → Q {\displaystyle P\to Q} {\displaystyle P\to Q}" or " Q → P {\displaystyle Q\to P} {\displaystyle Q\to P}" can be placed on a subsequent line.

Formal notation

The biconditional elimination rule may be written in sequent notation: ( P ↔ Q ) ⊢ ( P → Q ) {\displaystyle (P\leftrightarrow Q)\vdash (P\to Q)} {\displaystyle (P\leftrightarrow Q)\vdash (P\to Q)} and ( P ↔ Q ) ⊢ ( Q → P ) {\displaystyle (P\leftrightarrow Q)\vdash (Q\to P)} {\displaystyle (P\leftrightarrow Q)\vdash (Q\to P)}

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

or as the statement of a truth-functional tautology or theorem of propositional logic: ( P ↔ Q ) → ( P → Q ) ( P ↔ Q ) → ( Q → P ) {\displaystyle {\begin{aligned}(P\leftrightarrow Q)&\to (P\to Q)\\(P\leftrightarrow Q)&\to (Q\to P)\end{aligned}}} {\displaystyle {\begin{aligned}(P\leftrightarrow Q)&\to (P\to Q)\\(P\leftrightarrow Q)&\to (Q\to P)\end{aligned}}} where P {\displaystyle P} {\displaystyle P}, and Q {\displaystyle Q} {\displaystyle Q} are propositions expressed in some formal system.

See also

References

  1. 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.