How do I formulate a natural deduction rule such that the conclusion is for example; a ∨ b (∨ being exclusive OR)


Here's a structural presentation. I'll write $\lor$ for the usual, inclusive disjunction and $\oplus$ for exclusive-or.

The main idea will be to view $A\oplus B$ as $(A\lor B)\land \neg(A\land B)$ and then expressing the rules that definition would entail without referring to $\lor$, $\land$, or $\neg$. I'll be using the framework of a multi-succedent sequent calculus like LK. One downside of this particular approach is that it doesn't immediately lend itself to a constructively valid rule, though it can be transformed similarly as how we go from LK to LJ. I'll suppress the extra contexts that are just carried around, i.e. when I write $P\vdash Q$, I mean $\Gamma,P\vdash Q,\Delta$ and consistently on the top and bottom of the rules.

If we didn't mind mixing multiple connectives into a rule, the right or introduction rule for $\oplus$ could be written: $$\dfrac{\vdash P\lor Q\qquad \vdash \neg(P\land Q)}{\vdash P\oplus Q}$$ Luckily, all the following rules are invertible in LK: $$\dfrac{P\vdash}{\vdash \neg P}\qquad\dfrac{\vdash P}{\neg P\vdash}\qquad \dfrac{P,Q\vdash}{P\land Q\vdash}\qquad\dfrac{\vdash P,Q}{\vdash P\lor Q}$$ Applying these rules bottom-up from the premises gives a nice form for a $\oplus$ right/introduction rule:$$\dfrac{\vdash P,Q\qquad P,Q\vdash}{\vdash P\oplus Q}{\oplus} R$$

The left rule is a bit more subtle. First, there is two of them. The idea is that to show $A\oplus B$ we need to either show $A$ and $\neg B$, or show $B$ and $\neg A$. We just need to get rid of the $\neg$ on the left which is easily done producing the following two left rules: $$\dfrac{P\vdash Q}{P\oplus Q\vdash}{\oplus}L_1\qquad\dfrac{Q\vdash P}{P\oplus Q\vdash}{\oplus}L_2$$

At this point, we'd want to perform some checks to make sure these rules are well-behaved. For natural deduction, these checks are called local soundness and local completeness. For the sequent calculus, they are verifying that Cutting on $\oplus$ and Id (aka Axiom) for $\oplus$ are admissible. That is, $$\dfrac{\dfrac{\vdash P,Q\qquad P,Q\vdash}{\vdash P\oplus Q}{\oplus}R\qquad\dfrac{P\vdash Q}{P\oplus Q\vdash}{\oplus}L_1}{\vdash}$$ (and similarly for $\oplus L_2$) should mean that $$\dfrac{\vdash P,Q\qquad P,Q\vdash\qquad P\vdash Q}{\vdash}$$ and we should be able to derive $$\dfrac{}{P\oplus Q\vdash P\oplus Q}$$ using only structural rules (with Id restricted to atomic formulas) and the left and right rules of $\oplus$. The former constraint ensures that we can't get out any more information from $\oplus$ than we put in, and the latter ensures that we don't lose any information by using $\oplus$. These are easy to derive.

  • $\begingroup$ Another perspective on how to arrive at these rules is to view $P\oplus Q$ as $P\leftrightarrow \neg Q$. $\endgroup$ – Derek Elkins May 21 at 2:13

Let's use the symbol : w for exclusive OR

and the symbol : v for inclusive OR.

The definition of A w B is :

    AwB  <-->  (AvB) & ~ (A&B) 

So, rigorously, the only " w-intro" rule should be :

From (AvB) and ~ (A&B) , infer : AwB .

Or, if you prefer :

(1) (AvB)

(2) ~ (A&B)


(3) (AwB)

Now, if you have already proved a theorem stating another equivalence for (A wB), you can use it as a rule.

For example, it can be proved that : from (AwB) one can derive : ~ ( A <-->B ), and reciprocally.

So you can coin a rule like this :

from (AwB) , infer ~ (A<-->B)

and from ~ (A<-->B), infer (AwB).

enter image description here


There are many possibilities here. A straightforward one is:


$\neg B$

$\therefore A \oplus B$

(the $\oplus$ is typically used as the symbol for exclusive disjunction)

This rule, however, requires you to know exactly which of the two statements is true and which is false. So, an alternative rule, where you do not know that, but where you can still show that exactly one of the two is true, would be something akin to the biconditional introduction rule, where you do two subproofs: one that assumes $A$, and concludes $\neg B$, and one that assumes $\neg B$, and concludes $A$; from those two subproofs you can then infer $A \oplus B$


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.