 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/7/b/i/solution

Read chained logical implications as right-associative. Use the following natural deduction derivation; indentation bars mark nested subproofs and the last column records rules and discharged line ranges:

12345678910 E \to (F \to (G \to H)) ∣ G ∣ ∣ F ∣ ∣ ∣ E ∣ ∣ ∣ F \to (G \to H) ∣ ∣ ∣ G \to H ∣ ∣ ∣ H ∣ ∣ E \to H ∣ F \to (E \to H) G \to (F \to (E \to H)) premise assumption assumption assumption \to -elim 1, 4 \to -elim 5, 3 \to -elim 6, 2 \to -intro 4 - 7 \to -intro 3 - 8 \to -intro 2 - 9

E \to F \to G \to H ⊢ G \to F \to E \to H .

 New to topics? Read the docs here!