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

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 is
Its 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!