Exclusive-or natural deduction rules ($P\oplus Q⟺(P\wedge \neg Q)\vee (\neg P\wedge Q)$)

Introduce exclusive or from either $P,\neg Q$ or $\neg P,Q$. To eliminate $P\oplus Q$, derive the same conclusion $K$ in two subproofs, one under $P,\neg Q$ and the other under $\neg P,Q$, then discharge both pairs of case assumptions. These rules express exactly the two disjuncts of the displayed disjunctive normal form. Conjunction introduction and disjunction introduction derive that formula in each elimination branch; conversely disjunction elimination and conjunction elimination supply the two introduction cases. This proves equivalence without adding an unproved truth-table inference to a formal derivation.