 Solution

ID: 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/solution

Write the new exclusive or connective as

\oplus

. Give it the two introduction rules

\frac{P \neg Q}{P \oplus Q} \oplus I_{1}, \frac{\neg P Q}{P \oplus Q} \oplus I_{2},

and the elimination rule

\frac{P \oplus Q Γ , P , \neg Q ⊢ K Γ , \neg P , Q ⊢ K}{Γ ⊢ K} \oplus E .

In elimination, discharge the two pairs of case assumptions; retain the assumptions needed for the major premise and the shared context

Γ

. 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

\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.

 New to topics? Read the docs here!