= Solution
A uniform witness can serve every particular input. Two <natural deduction> proofs differ in whether <universal introduction> happens outside or inside the existential witness box.
``
Proof 1:
1 ∃y ∀x R(x,y) premise
2 | ∀x R(x,b) assumption, b fresh
3 | R(a,b) ∀-elim 2, with a arbitrary
4 | ∃y R(a,y) ∃-intro 3
5 ∃y R(a,y) ∃-elim 1,2–4
6 ∀x ∃y R(x,y) ∀-intro 5
Proof 2:
1 ∃y ∀x R(x,y) premise
2 | ∀x R(x,b) assumption, b fresh
3 | R(a,b) ∀-elim 2, with a arbitrary
4 | ∃y R(a,y) ∃-intro 3
5 | ∀x ∃y R(x,y) ∀-intro 4
6 ∀x ∃y R(x,y) ∃-elim 1,2–5
``
In both proofs $a$ is absent from the original premise. In the second it is also absent from the witness assumption, whose $x$ is bound; universal generalization is therefore legal inside that box. The exported conclusions contain no free $b$.
The converse is \b[not valid]. On the domain $\{0,1\}$, interpret $R(x,y)$ as $x=y$. For each $x$, choose $y=x$, so $\forall x\exists yR(x,y)$ holds. Neither single choice of $y$ equals both 0 and 1, so $\exists y\forall xR(x,y)$ fails. This is the distinction between a <pointwise witness> and a <uniform witness>.
Back to article page
