Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 8 / a / i

Use negation introduction on the unwanted existential quantification, and existential quantifier elimination rule with a fresh witness $a$:The witness name occurs neither in the surrounding assumptions nor in the conclusion $\perp$ of its subproof. This satisfies the eigenvariable condition; it is not an arbitrarily chosen fixed element assumed to witness the existential quantification. The result is $\neg \exists xP(x)$.