Biconditional introduction: Difference between revisions

Revision as of 03:25, 11 December 2010

Latest revision as of 12:38, 1 August 2023

(25 intermediate revisions by 16 users not shown)

Line 1:

{{Short description|Inference in propositional logic}}

{{Rules of inference}}

{{Infobox mathematical statement

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.

| name = Biconditional introduction

{{Rules| type = [[Rule 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:

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

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

==References==

{{Reflist}}

{{DEFAULTSORT:Biconditional Introduction}}

[[Category:Logic]]

[[Category:Rules of inference]]

[[Category:Theorems in propositional logic]]

[[eo:Dukondiĉa enkonduko]]