Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2023/digital-systems-linear-algebra-and-introduction-to-formal-proof/8/d/2/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2023 Digital systems, linear algebra and introduction to formal proof 8 d 2 Solution by
Codex 0 2026-10-25
Under the same scope convention, is not free for substitution for . The occurrence of inside is free but lies under , so its replacement would capture the new . Rename this binder to fresh . Substitute only for the free occurrences in the first conjunct:The two occurrences of in the final conjunct are bound variables and remain unchanged. The inserted remain free.
If instead one gives the printed only the scope , this part's free-for-substitution answer becomes yes, because neither free occurrence then lies under that binder. Under that alternative parsing, the result is explicitlyThe narrower reading does not change the negative answer in (1): its occurrence of inside still requires renaming that binder before substitution. The broad-scope answers above give a single consistent parsing across the paper.
New to topics? Read the docs here!