 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2017/digital-systems-linear-algebra-introduction-to-formal-proof/8/c/solution

The displayed proof is invalid: its existential-elimination step exports

Q (x_{0})

while

x_{0}

is still free in that conclusion. This is witness escape. Existential introduction afterwards cannot repair the invalid intermediate step.

Instead introduce the existential while the witness assumption is still open:

1234567 \forall x (P (x) \to Q (x)) \exists x P (x) P (a) P (a) \to Q (a) Q (a) \exists x Q (x) \exists x Q (x) premise premise fresh witness assumption \forall E 1 \to E 4, 3 \exists I 5 \exists E 2, 3 - 6

The existential quantifier introduction rule at line 6 removes the free witness from the exported statement, so the final existential elimination satisfies its eigenvariable condition.

 New to topics? Read the docs here!