Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Digital systems, linear algebra, introduction to formal proof / 7 / d / i

Write the new exclusive or connective as $\oplus$. Give it the two introduction rulesand the elimination ruleIn 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\wedge \neg Q)\vee (\neg P\wedge Q)$ from $P\oplus Q$ by $\oplus E$: in the first case introduce $P\wedge \neg Q$ and then the left disjunct; in the second case introduce $\neg P\wedge 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.