Biconditional elimination

{{Short description|Inference in propositional logic}}

{{Infobox mathematical statement

| name = Biconditional elimination

| type = Rule of inference

| field = Propositional calculus

| statement = If $P\; \backslash leftrightarrow\; Q$ is true, then one may infer that $P\; \backslash to\; Q$ is true, and also that $Q\; \backslash to\; P$ is true.

| symbolic statement = {{plainlist|

• $\backslash frac\{P\; \backslash leftrightarrow\; Q\}\{\backslash therefore\; P\; \backslash to\; Q\}$
• $\backslash frac\{P\; \backslash leftrightarrow\; Q\}\{\backslash therefore\; Q\; \backslash to\; P\}$

}}

}}

{{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 $P\; \backslash leftrightarrow\; Q$ is true, then one may infer that $P\; \backslash to\; Q$ is true, and also that $Q\; \backslash to\; P$ is true.{{cite web|last=Cohen|first=S. Marc|title=Chapter 8: The Logic of Conditionals|url=http://faculty.washington.edu/smcohen/120/Chapter8.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://faculty.washington.edu/smcohen/120/Chapter8.pdf |archive-date=2022-10-09 |url-status=live|publisher=University of Washington|access-date=8 October 2013}} 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:

:$\backslash frac\{P\; \backslash leftrightarrow\; Q\}\{\backslash therefore\; P\; \backslash to\; Q\}$

and

:$\backslash frac\{P\; \backslash leftrightarrow\; Q\}\{\backslash therefore\; Q\; \backslash to\; P\}$

where the rule is that wherever an instance of "$P\; \backslash leftrightarrow\; Q$" appears on a line of a proof, either "$P\; \backslash to\; Q$" or "$Q\; \backslash to\; P$" can be placed on a subsequent line.