= Solution
Write the new <exclusive or> connective as $\oplus$. Give it the two introduction rules
$$
\frac{P\quad\neg Q}{P\oplus Q}\ \oplus I_1,\qquad
\frac{\neg P\quad Q}{P\oplus Q}\ \oplus I_2,
$$
and the elimination rule
$$
\frac{P\oplus Q\qquad\Gamma,P,\neg Q\vdash K\qquad\Gamma,\neg P,Q\vdash K}{\Gamma\vdash K}\ \oplus E.
$$
In elimination, discharge the two pairs of case assumptions; retain the assumptions needed for the major premise and the shared context $\Gamma$. These are <natural deduction> rules for exactly one of $P,Q$, not merely at least one.
For a syntactic check, derive $(P\land\neg Q)\lor(\neg P\land Q)$ from $P\oplus Q$ by $\oplus E$: in the first case introduce $P\land\neg Q$ and then the left disjunct; in the second case introduce $\neg P\land Q$ and then the right disjunct. Conversely, from that disjunction use <disjunction elimination>; <conjunction elimination> extracts $P,\neg Q$ in the first branch and $\neg P,Q$ in the second, so the respective introduction rule yields $P\oplus Q$ in both. This proves equivalence to the ordinary truth-functional specification and explains both the introduction and elimination rules.
Back to article page
