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

Work backwards from the outermost available logical connective. One strategy applies the disjunction elimination rule to the premise first, constructs the whole target in each case, and then closes the cases. In the tables, a context such as

{1, 2}

means that assumptions on lines 1 and 2 remain open. A range in a discharge rule denotes the entire local subproof.

Line	Context	Formula	Justification
1	${1}$	$(P \land Q) \lor (P \land R)$	Premise
2	${1, 2}$	$P \land Q$	Temporary assumption
3	${1, 2}$	$P$	conjunction elimination rule $\land -elim-L$ on 2
4	${1, 2}$	$Q$	conjunction elimination rule $\land -elim-R$ on 2
5	${1, 2}$	$Q \lor R$	disjunction introduction rule $\lor -intro-L$ on 4
6	${1, 2}$	$P \land (Q \lor R)$	conjunction introduction rule $\land -intro$ on 3, 5
7	${1, 7}$	$P \land R$	Temporary assumption
8	${1, 7}$	$P$	conjunction elimination rule $\land -elim-L$ on 7
9	${1, 7}$	$R$	conjunction elimination rule $\land -elim-R$ on 7
10	${1, 7}$	$Q \lor R$	disjunction introduction rule $\lor -intro-R$ on 9
11	${1, 7}$	$P \land (Q \lor R)$	conjunction introduction rule $\land -intro$ on 8, 10
12	${1}$	$P \land (Q \lor R)$	disjunction elimination rule $\lor -elim$ on 1, 6, 11; discharge 2, 7

P

and

Q \lor R

separately, each by the disjunction elimination rule on the premise, and combine them:

Line	Context	Formula	Justification
1	${1}$	$(P \land Q) \lor (P \land R)$	Premise
2	${1, 2}$	$P \land Q$	Temporary assumption
3	${1, 2}$	$P$	conjunction elimination rule $\land -elim-L$ on 2
4	${1, 4}$	$P \land R$	Temporary assumption
5	${1, 4}$	$P$	conjunction elimination rule $\land -elim-L$ on 4
6	${1}$	$P$	disjunction elimination rule $\lor -elim$ on 1, 3, 5; discharge 2, 4
7	${1, 7}$	$P \land Q$	Temporary assumption
8	${1, 7}$	$Q$	conjunction elimination rule $\land -elim-R$ on 7
9	${1, 7}$	$Q \lor R$	disjunction introduction rule $\lor -intro-L$ on 8
10	${1, 10}$	$P \land R$	Temporary assumption
11	${1, 10}$	$R$	conjunction elimination rule $\land -elim-R$ on 10
12	${1, 10}$	$Q \lor R$	disjunction introduction rule $\lor -intro-R$ on 11
13	${1}$	$Q \lor R$	disjunction elimination rule $\lor -elim$ on 1, 9, 12; discharge 7, 10
14	${1}$	$P \land (Q \lor R)$	conjunction introduction rule $\land -intro$ on 6, 13

Both derivations establish

((P \land Q) \lor (P \land R)) ⊢ P \land (Q \lor R) .

Counting only applications of inference rules, each proof has nine steps: four conjunction elimination rule applications, two disjunction introduction rule applications, and three remaining applications. The first uses two conjunction introduction rule applications and one disjunction elimination rule; the second uses one and two, respectively. The second has two additional temporary-assumption lines, giving 14 displayed lines instead of 12, but assumptions are not additional inference applications. Its duplicated case analysis is exchanged for avoiding construction of the complete logical conjunction separately in both cases. In a proof tree it also repeats the use of the original premise.

 New to topics? Read the docs here!