Biconditional introduction: Difference between revisions

Revision as of 15:08, 20 January 2007

Latest revision as of 12:38, 1 August 2023

(43 intermediate revisions by 26 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 = [[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

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

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

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

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.

{{mathlogic stub}}

== Formal 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;

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:Rules of inference]]

[[Category:Theorems in propositional logic]]