Biconditional introduction: Difference between revisions

Revision as of 01:45, 4 March 2012

Revision as of 04:27, 4 March 2012

Line 1:

{{Transformation rules}}

In [[propositional calculus|propositional logic]], '''biconditional introduction''' is a [[validity|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 [[logical biconditional|biconditional]] into a [[formal proof|logical proof]]. If the<math>(P statement\to Q)</math> is true, and <math>(Q \to P)</math> then one may infer that ''A<math>(P implies\leftrightarrow B''Q)</math> andis true. For example, alsofrom the statementstatements that"if I''Bm impliesbreathing, then A'I'm bothalive" appearand in"if aI'm proofalive, then oneI'm maybreathing", introduceit thecan statementbe inferred that "I''Am breathing [[if and only if]] B'I'm oralive". formally,Biconditional ''(Aintroduction ↔is B)''the [[converse]] of [[biconditional elimination]].

== Formal notation ==

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".

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>(P \to Q)</math> are both in a proof; or in [[inference rule|rule form]]:

Formally, biconditional introduction is the rule schema.

:<math>\frac{(P A\to Q),(Q \to BP)}{\therefore (P \,leftrightarrow Q)}</math>

:<math> \underline{B \to A} </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 be placed on a subsequent line; or as the statement of a truth-functional [[Tautology (logic)|tautology]] or [[theorem]] of propositional logic:

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

:<math>((P \to Q) \and (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:Mathematical logic]]

[[Category:Propositional calculus]]

[[Category:Theorems in propositional logic]]