 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/8/g/solution

The printed expression has one unmatched closing parenthesis. Remove that final surplus parenthesis and read the first disjunct as

\exists x P (x)

; the other disjunct has outer universal quantification over the displayed implication. To distinguish the two independent bound uses of

x

, rename the first to

u

Push the outer negation through the logical disjunction and through the quantifiers. Negating the implication preserves its existential antecedent and negates its consequent. Applying De Morgan's laws and the quantifier negation rules gives the negation normal form

(\forall u \neg P (u)) \land \exists x [(\exists y Q (x, y)) \land (\forall z \neg R (z)) \land (\exists t \neg T (x, t))] .

Each negation is now directly before an atomic formula. No bound variable has been captured, and no original existential quantification in the antecedent has accidentally been negated twice.

 New to topics? Read the docs here!