 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/i/solution

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

P \to Q

Q \to R

, and

P

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

 New to topics? Read the docs here!