 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/d/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 / d / Solution by

Codex  0 2026-10-25

For implication creation rule, keep

ψ

available and discharge an otherwise unused antecedent:

1  ψ                         given
2  | φ                       assume
3  | ψ                       available from 1
4  φ → ψ                     →-intro, discharge 2–3

For implication distribution rule, write

H = ϕ \to (ψ \to ρ)

. The logical derivation below keeps

H

available and discharges exactly the two temporary assumptions:

1  φ → (ψ → ρ)                          given
2  | φ → ψ                              assume
3  | | φ                                assume
4  | | ψ                                →-elim, 3 and 2
5  | | ψ → ρ                            →-elim, 3 and 1
6  | | ρ                                →-elim, 4 and 5
7  | φ → ρ                              →-intro, discharge 3–6
8  (φ → ψ) → (φ → ρ)                    →-intro, discharge 2–7

These justify both derived inference rules using Figure 2 primitives. Their rule forms retain any other surrounding assumptions; they are not unconditionally asserted conclusions after the displayed numerator is forgotten.

 Read the full article

 New to topics? Read the docs here!