Английская Википедия:Biconditional elimination
Шаблон:Short description Шаблон:Infobox mathematical statement Шаблон:Transformation rules
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>P \leftrightarrow Q</math> is true, then one may infer that <math>P \to Q</math> is true, and also that <math>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>\frac{P \leftrightarrow Q}{\therefore P \to Q}</math>
and
- <math>\frac{P \leftrightarrow Q}{\therefore Q \to P}</math>
where the rule is that wherever an instance of "<math>P \leftrightarrow Q</math>" appears on a line of a proof, either "<math>P \to Q</math>" or "<math>Q \to P</math>" can be placed on a subsequent line.
Formal notation
The biconditional elimination rule may be written in sequent notation:
- <math>(P \leftrightarrow Q) \vdash (P \to Q)</math>
and
- <math>(P \leftrightarrow Q) \vdash (Q \to P)</math>
where <math>\vdash</math> is a metalogical symbol meaning that <math>P \to Q</math>, in the first case, and <math>Q \to P</math> in the other are syntactic consequences of <math>P \leftrightarrow Q</math> in some logical system;
or as the statement of a truth-functional tautology or theorem of propositional logic:
- <math>(P \leftrightarrow Q) \to (P \to Q)</math>
- <math>(P \leftrightarrow Q) \to (Q \to P)</math>
where <math>P</math>, and <math>Q</math> are propositions expressed in some formal system.
See also
References
