Biconditional introduction: Difference between revisions

Revision as of 20:08, 6 March 2012

Latest revision as of 12:38, 1 August 2023

(14 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 = [[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 allows for one to [[inference|infer]] a [[Logical biconditional|biconditional]] from two [[Material conditional|conditional statements]]. The rule makes it possible to introduce a [[logicalbiconditional biconditional|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:

:<math>((\frac{P \to Q), \and (Q \to P)) }{\totherefore (P \leftrightarrow Q)}</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; or as the statement of a truth-functional [[Tautology (logic)|tautology]] or [[theorem]] of propositional logic:.

== Formal notation ==

Line 7 ⟶ 19:

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

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

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

:<math>((P \to Q) \land (Q \to P)) \to (P \leftrightarrow Q)</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>((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]].

Line 23 ⟶ 33:

[[Category:Rules of inference]]

[[Category:Theorems in propositional logic]]

[[eo:Dukondiĉa enkonduko]]