Inference in propositional logic
Biconditional eliminationType | Rule of inference |
---|
Field | Propositional calculus |
---|
Statement | If is true, then one may infer that is true, and also that is true. |
---|
Symbolic statement | ![{\displaystyle {\frac {P\leftrightarrow Q}{\therefore P\to Q}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a04e9dc54240cdb74a2667a260cd142abf9a3821) ![{\displaystyle {\frac {P\leftrightarrow Q}{\therefore Q\to P}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7b034e9a46f9b06279d2b2a05b98b48931d8211e) |
---|
Transformation rules |
---|
Propositional calculus |
---|
Rules of inference |
---|
- Implication introduction / elimination (modus ponens)
- Biconditional introduction / elimination
- Conjunction introduction / elimination
- Disjunction introduction / elimination
- Disjunctive / hypothetical syllogism
- Constructive / destructive dilemma
- Absorption / modus tollens / modus ponendo tollens
- Negation introduction
|
Rules of replacement |
---|
- Associativity
- Commutativity
- Distributivity
- Double negation
- De Morgan's laws
- Transposition
- Material implication
- Exportation
- Tautology
|
Predicate logic |
---|
Rules of inference |
---|
- Universal generalization / instantiation
- Existential generalization / instantiation
|
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:
![{\displaystyle {\frac {P\leftrightarrow Q}{\therefore P\to Q}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a04e9dc54240cdb74a2667a260cd142abf9a3821)
and
![{\displaystyle {\frac {P\leftrightarrow Q}{\therefore Q\to P}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7b034e9a46f9b06279d2b2a05b98b48931d8211e)
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.
The biconditional elimination rule may be written in sequent notation:
![{\displaystyle (P\leftrightarrow Q)\vdash (P\to Q)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d9f7f7b09cdb8fe66b8a370d5ce130c7f70db9a7)
and
![{\displaystyle (P\leftrightarrow Q)\vdash (Q\to P)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/871bc3f35d872ea4a6ec18f5748311cf00043bdd)
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:
![{\displaystyle (P\leftrightarrow Q)\to (P\to Q)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3b49d545115caa4faa64695f891258ca41e0349b)
![{\displaystyle (P\leftrightarrow Q)\to (Q\to P)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/652b0d3bb4b025cf6d9e3c68184ff17527bf3f36)
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. Archived (PDF) from the original on 2022-10-09. Retrieved 8 October 2013.