Database: Biconditional introduction

Theorem 77: Biconditional introduction (inference rule)

Given that \phi entails \psi and \psi entails \phi , we may infer the equivalence \phi \Leftrightarrow \psi holds: \cfrac{\phi \vdash \psi \quad \psi \vdash \phi}{\vdash (\phi \Leftrightarrow \psi)}.

Proof: By conditional introduction, the implications \phi \Rightarrow \psi and \psi \Rightarrow \phi both hold. By conjunction introduction, we then infer that the conjunction \big( (\phi \Rightarrow \psi) \wedge (\phi \Rightarrow \psi) \big) holds. But \phi \Leftrightarrow \psi is shorthand for precisely this statement. \square

This database entry builds on the following:

  1. Definition: Conjunction
  2. Definition: Implication
  3. Definition: Equivalence
  4. Terminology: Entailment
  5. Terminology: Inference rule
  6. Inference rule: Conjunction introduction
  7. Theorem: Conditional introduction