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

 Ancestors (13)

 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