Rules of inference for exclusive disjunction and logical biconditional

Question

Here are the rules of inference in natural calculus of propositions. I'd like to extend this calculus (conservatively) adding exclusive disjunction $\oplus$ and logical biconditional $\sim$ and obtain a complete system. There are many ways to describe their 'behavior', for instance, 2 rules:

$$\cfrac{\Gamma,\neg A\vdash B;\quad \Gamma,\neg B\vdash A}{\Gamma\vdash A\oplus B};\qquad\cfrac{\Gamma\vdash A\oplus B}{\Gamma,A,B\vdash}$$

would be enough for strict disjunction.

My question is: which way is traditional (if there is such a tradition) and most convinient?

Answer 1

For bi-conditional, I would suggest:

$\dfrac {\Gamma, A \vdash B \ \ \ \ \Gamma, B \vdash A}{\Gamma \vdash A \leftrightarrow B} \text { for }(\leftrightarrow \text I)$

and the pair:

$\dfrac {\Gamma \vdash A \leftrightarrow B}{\Gamma, A \vdash B} \ \ \ \dfrac {\Gamma \vdash A \leftrightarrow B}{\Gamma, B \vdash A} \text { for }(\leftrightarrow \text E)$

---

For exclusive or, the pair:

$\dfrac {\Gamma, A \vdash \ \ \ \ \Gamma \vdash B}{\Gamma \vdash A \oplus B} \ \ \ \dfrac {\Gamma, \vdash A \ \ \ \ \Gamma, B \vdash}{\Gamma \vdash A \oplus B} \text { for }(\oplus \text I)$

and the corresponding for $(\oplus \text E)$, based on the fact that an $\oplus$ True formula can produce cases: either $A$ False and $B$ True or the symmetric one:

$\dfrac {\Gamma, A \vdash \ \ \ \ \Gamma \vdash A \oplus B}{ \Gamma \vdash B} \ \ \ \dfrac {\Gamma, \vdash A \ \ \ \ \Gamma \vdash A \oplus B}{\Gamma, B \vdash}$