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

a

1  ∀x. ¬P(x)    premise
2  | ∃x. P(x)   assumption
3  | | P(a)     assumption, a fresh
4  | | ¬P(a)    ∀-elim 1
5  | | ⊥        ¬-elim 3,4
6  | ⊥          ∃-elim 2,3–5
7  ¬(∃x. P(x))  ¬-intro 2–6

The witness name occurs neither in the surrounding assumptions nor in the conclusion

⊥

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 x P (x)$ .

Solution

 0  0

Choose a fresh parameter

a

. The universal quantifier elimination rule supplies both the implication and its premise at that same parameter:

1  ∀x. (P(x) → Q(x))        premise
2  | ∀x. P(x)               assumption
3  | P(a)                   ∀-elim 2
4  | P(a) → Q(a)            ∀-elim 1
5  | Q(a)                   →-elim 4,3
6  | ∀x. Q(x)               ∀-intro 5, a fresh
7  (∀x. P(x)) → (∀x. Q(x))  →-intro 2–6

The eigenvariable condition holds because

a

is absent from both undischarged assumptions at line 6. Hence the universally quantified implication is proved.

The proposed version with merely

P (x)

in the antecedent is not derivable. For a counterexample, take a two-element domain

{0, 1}

with

P

and

Q

both true precisely at zero. The universal premise holds. Under the assignment

x = 0

P (x)

is true but

\forall x Q (x)

is false. By soundness, a formal proof cannot exist. Attempting the previous derivation would fail exactly at universal quantifier introduction rule: the parameter would occur in the undischarged assumption