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

Introduce the three logical implications from the outside in. Under assumptions

P \to Q

Q \to R

, and

P

, apply the implication elimination rule twice, then use assumption discharge in reverse order:

Line	Context	Formula	Justification
1	${1}$	$P \to Q$	Temporary assumption
2	${1, 2}$	$Q \to R$	Temporary assumption
3	${1, 2, 3}$	$P$	Temporary assumption
4	${1, 2, 3}$	$Q$	implication elimination rule $\to -elim$ on 1, 3
5	${1, 2, 3}$	$R$	implication elimination rule $\to -elim$ on 2, 4
6	${1, 2}$	$P \to R$	implication introduction rule $\to -intro$ on 5; discharge 3
7	${1}$	$(Q \to R) \to (P \to R)$	implication introduction rule $\to -intro$ on 6; discharge 2
8	$\emptyset$	$(P \to Q) \to ((Q \to R) \to (P \to R))$	implication introduction rule $\to -intro$ on 7; discharge 1

Thus

⊢ (P \to Q) \to ((Q \to R) \to (P \to R)) .

(1)

ii

 0  0

Solution

 0  0

Under

P

, the first assumption yields

Q \to R

, while the second yields

Q

. Apply the implication elimination rule once more to obtain

R

, and discharge the three temporary assumptions:

Line	Context	Formula	Justification
1	${1}$	$P \to (Q \to R)$	Temporary assumption
2	${1, 2}$	$P \to Q$	Temporary assumption
3	${1, 2, 3}$	$P$	Temporary assumption
4	${1, 2, 3}$	$Q \to R$	implication elimination rule $\to -elim$ on 1, 3
5	${1, 2, 3}$	$Q$	implication elimination rule $\to -elim$ on 2, 3
6	${1, 2, 3}$	$R$	implication elimination rule $\to -elim$ on 4, 5
7	${1, 2}$	$P \to R$	implication introduction rule $\to -intro$ on 6; discharge 3
8	${1}$	$(P \to Q) \to (P \to R)$	implication introduction rule $\to -intro$ on 7; discharge 2
9	$\emptyset$	$(P \to (Q \to R)) \to ((P \to Q) \to (P \to R))$	implication introduction rule $\to -intro$ on 8; discharge 1

The two uses of

P

are permitted in ordinary natural deduction. Therefore

⊢ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) .

(1)

iii

 0  0

Solution

 0  0

The premise turns an assumed

\neg P

into a contradiction. Use the negation introduction rule to obtain

\neg\neg P

, then the supplied classical double-negation elimination rule:

Line	Context	Formula	Justification
1	${1}$	$\neg P \to ⊥$	Premise
2	${1, 2}$	$\neg P$	Temporary assumption
3	${1, 2}$	$⊥$	implication elimination rule $\to -elim$ on 1, 2
4	${1}$	$\neg\neg P$	negation introduction rule $\neg -intro$ on 3; discharge 2
5	${1}$	$P$	double-negation elimination $\neg\neg -elim$ on 4

Hence

(\neg P \to ⊥) ⊢ P

. The final classical rule is essential: deriving

\neg\neg P

alone is not yet a proof of

P

in Intuitionistic propositional logic.

iv

 0  0

Solution

 0  0

Assuming

\neg P

lets the disjunction introduction rule produce the logical disjunction excluded by the premise. This gives a contradiction, so conclude by negation introduction and double-negation elimination:

Line	Context	Formula	Justification
1	${1}$	$\neg (\neg P \lor \neg Q)$	Premise
2	${1, 2}$	$\neg P$	Temporary assumption
3	${1, 2}$	$\neg P \lor \neg Q$	disjunction introduction rule $\lor -intro-L$ on 2
4	${1, 2}$	$⊥$	negation elimination rule $\neg -elim$ on 3, 1
5	${1}$	$\neg\neg P$	negation introduction rule $\neg -intro$ on 4; discharge 2
6	${1}$	$P$	double-negation elimination $\neg\neg -elim$ on 5

Thus

\neg (\neg P \lor \neg Q) ⊢ P .

(1)

No separate result about

Q

or use of a derived De Morgan rule is needed.

 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

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

 Discussion (0)  Subscribe (1) New discussion

 Discussion (0) New discussion