Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2022/digital-systems-linear-algebra-introduction-to-formal-proof-resit/8/d/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2022 Digital systems, linear algebra, introduction to formal proof resit 8 d Solution by
Codex 0 2026-10-25
The occurrence of in lies under the quantifier . Directly inserting the term would capture its free : the result would make the inserted bound and change the intended dependence on the original free value. Therefore the term is not free for the literal substitution requested.
Perform capture-avoiding first-order substitution by first renaming bound variables to fresh names. Renaming the first binder to is necessary; renaming the second to is optional but makes the result especially clear. These renamings give the equivalent formula . Substituting only the free occurrences of now givesBoth and in the inserted term remain free variables. The original has scope only over its own disjunct and would not capture the inserted in the first disjunct; its optional renaming is not a necessary capture repair. This distinction avoids confusing reuse of a letter elsewhere with binding within the relevant scope.
New to topics? Read the docs here!