Biconditional introduction: Difference between revisions

Revision as of 09:29, 8 September 2008

Latest revision as of 12:38, 1 August 2023

(31 intermediate revisions by 22 users not shown)

Line 1:

{{Short description|Inference in propositional logic}}

In [[mathematical logic]], '''biconditional introduction''' is the [[rule of inference]] that, if B follows from A, and A follows from B, then A [[if and only if]] B.

{{Infobox mathematical statement

| name = Biconditional introduction

| type = [[Category:RulesRule of inference]]

| field = [[Propositional calculus]]

| statement = If <math>P \to Q</math> is true, and if <math>Q \to P</math> is true, then one may infer that <math>P \leftrightarrow Q</math> is true.

| symbolic statement = <math>\frac{P \to Q, Q \to P}{\therefore P \leftrightarrow Q}</math>

}}

{{Transformation rules}}

In [[propositional calculus|propositional logic]], '''biconditional introduction'''<ref>Hurley</ref><ref>Moore and Parker</ref><ref>Copi and Cohen</ref> is a [[Validity (logic)|valid]] [[rule of inference]]. It allows for one to [[inference|infer]] a [[Logical biconditional|biconditional]] from two [[Material conditional|conditional statements]]. The rule makes it possible to introduce a biconditional statement into a [[formal proof|logical proof]]. If <math>P \to Q</math> is true, and if <math>Q \to P</math> is true, then one may infer that <math>P \leftrightarrow Q</math> is true. For example, from the statements "if I'm breathing, then I'm alive" and "if I'm alive, then I'm breathing", it can be inferred that "I'm breathing [[if and only if]] I'm alive". Biconditional introduction is the [[Converse (logic)|converse]] of [[biconditional elimination]]. The rule can be stated formally as:

For example, from the statements "if I'm breathing, then I'm alive" and "if I'm alive, then I'm breathing", it can be inferred that "I'm breathing if and only if I'm alive".

:<math>\frac{P \to Q, Q \to P}{\therefore P \leftrightarrow Q}</math>

Formally, biconditional introduction is the rule schema

where the rule is that wherever instances of "<math>P \to Q</math>" and "<math>Q \to P</math>" appear on lines of a proof, "<math>P \leftrightarrow Q</math>" can validly be placed on a subsequent line.

:<math> A \to B \, </math>

:<math> \underline{B \to A} </math>

:<math> A \leftrightarrow B </math>

==See alsoFormal notation ==

The ''biconditional introduction'' rule may be written in [[sequent]] notation:

:<math>(P \to Q), (Q \to P) \vdash (P \leftrightarrow Q)</math>

where <math>\vdash</math> is a [[metalogic]]al symbol meaning that <math>P \leftrightarrow Q</math> is a [[logical consequence|syntactic consequence]] when <math>P \to Q</math> and <math>Q \to P</math> are both in a proof;

*[[Logical biconditional]]

or as the statement of a truth-functional [[Tautology (logic)|tautology]] or [[theorem]] of propositional logic:

{{logic-stub}}

:<math>((P \to Q) \land (Q \to P)) \to (P \leftrightarrow Q)</math>

[[Category:Logic]]

[[Category:Rules of inference]]

where <math>P</math>, and <math>Q</math> are propositions expressed in some [[formal system]].

[[eo:Dukondiĉa enkonduko]]

==References==

{{Reflist}}

{{DEFAULTSORT:Biconditional Introduction}}

[[Category:LogicRules of inference]]

[[Category:Theorems in propositional logic]]