Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Digital systems, linear algebra, introduction to formal proof / 7 / a / iii

Table of contents
- Solution iii

Solution

Put

H = \neg (P \to \neg Q)

. First derive

Q

, then

P

, using the derived proof by contradiction rule. Indentation records the subproofs:

123456789101112131415 H \neg Q P \neg Q P \to \neg Q ⊥ Q \neg P P ⊥ \neg Q P \to \neg Q ⊥ P Q \land P premise assumption assumption reiterate 2 \to I 3 - 4 \neg E 1, 5 RAA 2 - 6 assumption assumption \neg E 9, 8 ⊥ E 10 \to I 9 - 11 \neg E 1, 12 RAA 8 - 13 \land I 7, 14

Line 11 uses explosion; lines 5 and 12 discharge only their inner assumptions. Each RAA step can be expanded into negation introduction followed by double-negation elimination, as in part (ii).

 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