Biconditional elimination: Difference between revisions
m Task 18 (cosmetic): eval 1 template: hyphenate params (1×); |
|||
Line 1: | Line 1: | ||
{{Infobox mathematical statement |
|||
| name = Biconditional elimination |
|||
| type = [[Rule of inference]] |
|||
| field = [[Propositional calculus]] |
|||
| statement = 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. |
|||
| symbolic statement = {{plainlist| |
|||
* <math>\frac{P \leftrightarrow Q}{\therefore P \to Q}</math> |
|||
* <math>\frac{P \leftrightarrow Q}{\therefore Q \to P}</math> |
|||
}} |
|||
}} |
|||
{{Transformation rules}} |
{{Transformation rules}} |
||
Revision as of 17:32, 13 June 2022
Type | Rule of inference |
---|---|
Field | Propositional calculus |
Statement | If is true, then one may infer that is true, and also that is true. |
Symbolic statement |
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 is true, then one may infer that is true, and also that 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:
and
where the rule is that wherever an instance of "" appears on a line of a proof, either "" or "" can be placed on a subsequent line;
Formal notation
The biconditional elimination rule may be written in sequent notation:
and
where is a metalogical symbol meaning that , in the first case, and in the other are syntactic consequences of in some logical system;
or as the statement of a truth-functional tautology or theorem of propositional logic:
where , and are propositions expressed in some formal system.
See also
References
- ^ Cohen, S. Marc. "Chapter 8: The Logic of Conditionals" (PDF). University of Washington. Retrieved 8 October 2013.