Write the new exclusive or connective as . 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 . These are natural deduction rules for exactly one of , not merely at least one.
For a syntactic check, derive from by : in the first case introduce and then the left disjunct; in the second case introduce and then the right disjunct. Conversely, from that disjunction use disjunction elimination; conjunction elimination extracts in the first branch and in the second, so the respective introduction rule yields in both. This proves equivalence to the ordinary truth-functional specification and explains both the introduction and elimination rules.
Use the exclusive-or natural deduction rules defined in part (i). The only extra lemma needed is double-negation introduction, derived from the given rules by assuming under , obtaining contradiction, and discharging that assumption. The full proof incorporates that derivation:In the first case the second introduction rule is instantiated with right operand . In the second case the first introduction rule requires , which is exactly the derived line 10.
1. ¬P ⊕ Q premise
2. ¬P first ⊕E case assumption [i]
3. ¬Q first ⊕E case assumption [j]
4. P ⊕ ¬Q ⊕I₂, 2, 3
5. ¬¬P second ⊕E case assumption [k]
6. Q second ⊕E case assumption [l]
7. P ¬¬E, 5
8. ¬Q assumption [m]
9. ⊥ ¬E, 6, 8
10. ¬¬Q ¬I, 8–9, discharging [m]
11. P ⊕ ¬Q ⊕I₁, 7, 10
12. P ⊕ ¬Q ⊕E, 1, 2–4, 5–11,
discharging [i], [j], [k], [l] Articles by others on the same topic
There are currently no matching articles.