Biconditional introduction: Difference between revisions

Revision as of 21:21, 22 February 2012

Latest revision as of 12:38, 1 August 2023

(17 intermediate revisions by 12 users not shown)

Line 1:

{{Short description|Inference in propositional logic}}

{{Infobox mathematical statement

| name = Biconditional introduction

| type = [[Rule of inference]]

| field = [[Category: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 [[validityValidity (logic)|valid]] [[rule of inference]]. It makesallows itfor possibleone to introduce[[inference|infer]] a [[logicalLogical 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 the<math>P statement\to Q</math> is true, and if <math>Q \to P</math> is true, then one may infer that ''A<math>P implies\leftrightarrow B''Q</math> andis alsotrue. For example, from the statementstatements that"if I''Bm impliesbreathing, A'then 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 Bthe [[Converse (logic)''|converse]] of [[biconditional elimination]]. The rule can be stated formally as:

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

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

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.

Formally, biconditional introduction is the rule schema.

== Formal notation ==

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

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

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

:<math>(P A\to Q), (Q \leftrightarrowto BP) \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:MathematicalTheorems in propositional logic]]

[[Category:Propositional calculus]]

[[eo:Dukondiĉa enkonduko]]