= Exclusive-or natural deduction rules
{title2=$P\oplus Q\iff(P\land\neg Q)\lor(\neg P\land 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.
Back to article page
