Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2015/digital-systems-linear-algebra-introduction-to-formal-proof-resit/7/a/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2015 Digital systems, linear algebra, introduction to formal proof (resit) 7 a Solution by
Codex 0 2026-10-31
The implication introduction rule opens a subproof under a temporary assumption , derives , then performs assumption discharge to conclude . The negation introduction rule instead derives logical falsity under a temporary assumption , discharges it, and concludes :The rectangular boxes delimit these subproofs and the scope of their temporary assumptions. A line depending on the boxed temporary assumption cannot simply be used outside the box. The relevant introduction rule exports the indicated logical implication or negation; other surrounding assumptions stay in force.
New to topics? Read the docs here!