Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Digital systems, linear algebra, introduction to formal proof / 7 / d / ii

Temporarily deny the desired logical disjunction. If

\neg P

held, it would introduce that very logical disjunction, producing logical falsity; double-negation elimination therefore gives

P

. The same argument gives

Q

, contradicting the premise. The complete natural deduction derivation is:

Classical derivation of the disjunction of negations

Line	Open assumptions	Formula	Justification
1	1	$\neg (P \land Q)$	Premise
2	1, 2	$\neg (\neg P \lor \neg Q)$	Temporary assumption
3	1, 2, 3	$\neg P$	Temporary assumption
4	1, 2, 3	$\neg P \lor \neg Q$	disjunction introduction L 3
5	1, 2, 3	$⊥$	negation elimination rule 4, 2
6	1, 2	$\neg\neg P$	negation introduction 3, 5
7	1, 2	$P$	double-negation elimination 6
8	1, 2, 8	$\neg Q$	Temporary assumption
9	1, 2, 8	$\neg P \lor \neg Q$	disjunction introduction R 8
10	1, 2, 8	$⊥$	negation elimination rule 9, 2
11	1, 2	$\neg\neg Q$	negation introduction 8, 10
12	1, 2	$Q$	double-negation elimination 11
13	1, 2	$P \land Q$	conjunction introduction 7, 12
14	1, 2	$⊥$	negation elimination rule 13, 1
15	1	$\neg\neg (\neg P \lor \neg Q)$	negation introduction 2, 14
16	1	$\neg P \lor \neg Q$	double-negation elimination 15

Consequently

\neg P \lor \neg Q .

The uses of double-negation elimination are justified by the supplied rules. This distinguishes the proof from the preceding constructive direction of De Morgan's laws.

 Ancestors (12)

There are no discussions about this article yet.

There are currently no matching articles.