Biconditional introduction

<h2 id="formal-notation">Formal notation</h2>
<p>The <i>biconditional introduction</i> rule may be written in <a href="/facts/Sequent/7YoB2hYb">sequent</a> notation:
</p>

(
        P
        →
        Q
        )
        ,
        (
        Q
        →
        P
        )
        ⊢
        (
        P
        ↔
        Q
        )
      
    
    {\displaystyle (P\to Q),(Q\to P)\vdash (P\leftrightarrow Q)}

<p>where 
  
    
      
        ⊢
      
    
    {\displaystyle \vdash }
  
 is a <a href="/facts/Metalogic/zfooQjCo">metalogical</a> symbol meaning that 
  
    
      
        P
        ↔
        Q
      
    
    {\displaystyle P\leftrightarrow Q}
  
 is a <a href="/facts/Logical_consequence/AyDXp4dn">syntactic consequence</a> when 
  
    
      
        P
        →
        Q
      
    
    {\displaystyle P\to Q}
  
 and 
  
    
      
        Q
        →
        P
      
    
    {\displaystyle Q\to P}
  
 are both in a proof;
</p><p>or as the statement of a truth-functional <a href="/facts/Tautology_(logic)/p82wWMaN">tautology</a> or <a href="/facts/Theorem/f2Pe1FMD">theorem</a> of propositional logic:
</p>

(
        (
        P
        →
        Q
        )
        ∧
        (
        Q
        →
        P
        )
        )
        →
        (
        P
        ↔
        Q
        )
      
    
    {\displaystyle ((P\to Q)\land (Q\to P))\to (P\leftrightarrow Q)}

<p>where 
  
    
      
        P
      
    
    {\displaystyle P}
  
, and 
  
    
      
        Q
      
    
    {\displaystyle Q}
  
 are propositions expressed in some <a href="/facts/Formal_system/KaeDAjK7">formal system</a>.
</p>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>Hurley <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>Moore and Parker <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>Copi and Cohen <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
</ol>

Biconditional introduction open-in-new

Biconditional introduction