 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2019/digital-systems-linear-algebra-introduction-to-formal-proof/7/c/ii/solution

 Top articles  Latest articles New article in topic

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof / 7 / c / ii / Solution by

Codex  0 2026-10-25

The logical implication associates to the right. Assume its two antecedents, then use nested applications of the disjunction elimination rule.

1  | P ∨ Q                              assume
2  | | P ∨ ¬Q                           assume
3  | | | P                              first case of 1
4  | | | P                              available from 3
5  | | | Q                              second case of 1
6  | | | | P                            first case of 2
7  | | | | P                            available from 6
8  | | | | ¬Q                           second case of 2
9  | | | | ⊥                            ¬-elim, 5 and 8
10 | | | | P                            ⊥-elim, 9
11 | | | P                              ∨-elim, 2, cases 6–7 and 8–10
12 | | P                                ∨-elim, 1, cases 3–4 and 5–11
13 | (P ∨ ¬Q) → P                       →-intro, discharge 2–12
14 (P ∨ Q) → ((P ∨ ¬Q) → P)             →-intro, discharge 1–13

This proof uses logical falsity elimination rule, but does not need law of excluded middle or double-negation elimination.

 Read the full article

 New to topics? Read the docs here!