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

Table of contents
- i b
  - Solution i
- ii b
  - Solution ii

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 .

ii

Solution

Use conjunction elimination to extract the three inputs, then apply the implication elimination rule three times:

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

The implication introduction rule closes the only subproof, giving

E \to F \to G \to H ⊢ ((E \land F) \land G) \to H .

 Ancestors (11)

 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