Equivalence rule for sequent calculus

Question

Why are there no inference rules for equivalence (≡ on the right and ≡ on the left) for the sequent calculus, and if there was, how would they look like?

e.g.

(1) $\cfrac{?}{\Gamma,(A \supset B) ≡ (C \land D), \Delta \rightarrow \Lambda}≡ : l $

(2) $\cfrac{?}{\Gamma \rightarrow \Delta, (A \supset B) ≡ (C \land D), \Lambda}≡ : r $ ?

Answer 1

See :

• Stephen Cole Kleene, Mathematical logic (1967 - Dover reprint), page 289 :

$\cfrac{A, \Gamma \to \Delta, B \quad \quad B, \Gamma \to \Delta, A}{\Gamma \to \Delta, A \equiv B} \equiv \text{: right} $

$\cfrac{A,B, \Gamma \to \Delta \quad \quad \Gamma \to \Delta, A, B}{A \equiv B, \Gamma \to \Delta} \equiv \text{: left} $

---

If we define $A \equiv B$ as an abbreviation for $(A ⊃ B) \land (B ⊃ A)$, the above rules are easily derivable from $⊃$ and $∧$ rules.

For $ \equiv \text{: right} $ :

$\cfrac{A, \Gamma \to \Delta, B \quad \quad B, \Gamma \to \Delta, A}{\Gamma \to \Delta, A ⊃ B, B ⊃ A } ⊃ \text{: right} $ twice

$\cfrac{\Gamma \to \Delta, A ⊃ B, B ⊃ A}{A, \Gamma \to \Delta, A \equiv B } \land \text{: right} $

For $ \equiv \text{: left} $ :

$\cfrac{A,B, \Gamma \to \Delta \quad \quad \Gamma \to \Delta, A, B}{A ⊃ B, B ⊃ A, \Gamma \to \Delta} ⊃ \text{: left} $ twice

$\cfrac{A ⊃ B, B ⊃ A, \Gamma \to \Delta}{A \equiv B, \Gamma \to \Delta} \land \text{: left} $