1
$\begingroup$

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

$\endgroup$
5
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Perhaps you could expand how you derived at these formulae so that people can refer to it? $\endgroup$ – Marcel Oct 2 '15 at 20:32
  • $\begingroup$ @Marcel . you can compare them with the rules for $\to$ (or $\supset$) and you will see that they are intuitively "obvious". $\endgroup$ – Mauro ALLEGRANZA Oct 2 '15 at 21:15
  • $\begingroup$ 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$ $\endgroup$ – Marcel Oct 3 '15 at 11:30
  • $\begingroup$ 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,Γ→Δ$. $\endgroup$ – Mauro ALLEGRANZA Oct 3 '15 at 11:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.