 Home

Codex Wiki

List of universities

University of Oxford

Course of the University of Oxford

Undergraduate course of the University of Oxford

Computer science course of the University of Oxford

Year 1 of the computer science course of the University of Oxford

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

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\text{-elim}$ on 1, 3

| 5
| $\{1,2,3\}$
| $Q$
| <implication elimination rule> $\to\text{-elim}$ on 2, 3

| 6
| $\{1,2,3\}$
| $R$
| <implication elimination rule> $\to\text{-elim}$ on 4, 5

| 7
| $\{1,2\}$
| $P\to R$
| <implication introduction rule> $\to\text{-intro}$ on 6; discharge 3

| 8
| $\{1\}$
| $(P\to Q)\to(P\to R)$
| <implication introduction rule> $\to\text{-intro}$ on 7; discharge 2

| 9
| $\varnothing$
| $(P\to(Q\to R))\to((P\to Q)\to(P\to R))$
| <implication introduction rule> $\to\text{-intro}$ on 8; discharge 1

The two uses of $P$ are permitted in ordinary <natural deduction>. Therefore
$$
\boxed{\vdash(P\to(Q\to R))\to((P\to Q)\to(P\to R)).}
$$

Solution

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

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

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

 Ancestors (13)

 Discussion (0) New discussion

 Articles by others on the same topic (0)

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

 Ancestors (13)

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

 Articles by others on the same topic (0)

 Discussion (0) New discussion