 Solution

ID: 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/ii/solution

Under

P

, the first assumption yields

Q \to R

, while the second yields

Q

. Apply the implication elimination rule once more to obtain

R

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

 New to topics? Read the docs here!