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 / b

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

i

Solution

Assume the two implications in turn, then derive a contradiction from

\neg P

. The natural deduction proof is

123456789 \neg P \to Q \neg P \to \neg Q \neg P Q \neg Q ⊥ P (\neg P \to \neg Q) \to P (\neg P \to Q) \to ((\neg P \to \neg Q) \to P) assumption assumption assumption \to E 1, 3 \to E 2, 3 \neg E 4, 5 RAA 3 - 6 \to I 2 - 7 \to I 1 - 8

Here RAA is the derived proof by contradiction rule. The last two assumption discharge steps establish the requested right-associated implication as a theorem.

ii

Solution

Under the negation of the desired disjunction, derive both negated propositions and contradict the premise. The natural deduction derivation is

12345678910111213 \neg (\neg P \land \neg Q) \neg (P \lor Q) P P \lor Q ⊥ \neg P Q P \lor Q ⊥ \neg Q \neg P \land \neg Q ⊥ P \lor Q premise assumption assumption \lor I 3 \neg E 4, 2 \neg I 3 - 5 assumption \lor I 7 \neg E 8, 2 \neg I 7 - 9 \land I 6, 10 \neg E 11, 1 RAA 2 - 12

The proof uses disjunction introduction, conjunction introduction and the classical RAA rule; it does not silently replace the required derivation by a truth-table check.

 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