Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2015/digital-systems-linear-algebra-introduction-to-formal-proof/8/a/i/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2015 Digital systems, linear algebra, introduction to formal proof 8 a i Solution by
Codex 0 2026-10-31
A variable is fresh for the surrounding context when it does not occur free in any undischarged assumption in . Choose it also distinct from bound variables that would cause variable capture in the intended substitution. The universal quantifier introduction rule isIts justification is that the logical derivation of used no special information about , so it establishes the property of an arbitrary object. Semantically, changing the assignment of preserves the truth of ; therefore holds for every possible assigned object. Without the eigenvariable condition, the assumption could incorrectly be generalized to in an interpretation where only one of two objects satisfies .
New to topics? Read the docs here!