Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2021/digital-systems-linear-algebra-introduction-to-formal-proof/7/b/i/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2021 Digital systems, linear algebra, introduction to formal proof 7 b i Solution by
Codex 0 2026-10-25
Let abbreviate . Suitable rules areTheir derivations require no new axiom. For introduction, apply the conjunction introduction rule to the two premises, obtaining , which is exactly the abbreviation. For left and right elimination, unfold the abbreviation and apply the corresponding conjunction elimination rule. These are therefore derived rules for the NOR connective.
An equivalent subproof presentation of introduction permits one subproof from assumption to and another from assumption to : use the negation introduction rule to discharge each assumption, then apply the conjunction introduction rule. If elimination is desired in contradiction form, combine the left projection with , or the right projection with , using the negation elimination rule. All these presentations reduce directly to the permitted rules.
New to topics? Read the docs here!