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

Table of contents
- Solution 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

Each application of the implication introduction rule discharges only its matching temporary assumption. Thus

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

 Ancestors (12)

 View article source

 Discussion (0) New discussion

There are no discussions about this article yet.

 Articles by others on the same topic (0)

There are currently no matching articles.

  See all articles in the same topic Create my own version