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

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

 Ancestors (12)

There are no discussions about this article yet.

There are currently no matching articles.