# Equivalence rule for sequent calculus

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$ ?

See :

$\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}$

• Perhaps you could expand how you derived at these formulae so that people can refer to it? – Marcel Oct 2 '15 at 20:32
• @Marcel . you can compare them with the rules for $\to$ (or $\supset$) and you will see that they are intuitively "obvious". – Mauro ALLEGRANZA Oct 2 '15 at 21:15
• When I do it for the left rule, I obtain: $\cfrac{\Gamma \Delta \rightarrow A,B,\Lambda \qquad \Gamma, A, B, \Delta \rightarrow \Lambda}{...}≡: left$ – Marcel Oct 3 '15 at 11:30
• No; consider the two top sequents and apply $⊃$-left first with $A$ of the top right seq and $B$ of the top left seq, getting $A ⊃ B, \Gamma \to \Delta$ in the bottom seq. Applying the rule again with $A$ of the top left and $B$ of the top right seq, we get : $A ⊃ B, B ⊃ A, \Gamma \to \Delta$ as bottom seq. Now apply $\land$-left and you conclude with : $A≡B,Γ→Δ$. – Mauro ALLEGRANZA Oct 3 '15 at 11:39