= Solution
Extract the universally quantified <logical implication> and the existentially quantified <logical conjunction> from the premise. Use one fresh witness $a$ for both conjuncts of the latter, so that the resulting $R(a)$ and $\neg S(a)$ concern the same object:
|| Line
|| Context
|| Formula
|| Justification
| 1
| $\{1\}$
| $(\forall x\,(Q(x)\to R(x)))\land(\exists x\,(Q(x)\land\neg S(x)))$
| Premise
| 2
| $\{1\}$
| $\forall x\,(Q(x)\to R(x))$
| <conjunction elimination rule> $\land\text{-elim-L}$ on 1
| 3
| $\{1\}$
| $\exists x\,(Q(x)\land\neg S(x))$
| <conjunction elimination rule> $\land\text{-elim-R}$ on 1
| 4
| $\{1,4\}$
| $Q(a)\land\neg S(a)$
| Temporary assumption
| 5
| $\{1,4\}$
| $Q(a)$
| <conjunction elimination rule> $\land\text{-elim-L}$ on 4
| 6
| $\{1,4\}$
| $\neg S(a)$
| <conjunction elimination rule> $\land\text{-elim-R}$ on 4
| 7
| $\{1,4\}$
| $Q(a)\to R(a)$
| <universal elimination> $\forall\text{-elim}$ on 2; instantiate at $a$
| 8
| $\{1,4\}$
| $R(a)$
| <implication elimination rule> $\to\text{-elim}$ on 7, 5
| 9
| $\{1,4\}$
| $R(a)\land\neg S(a)$
| <conjunction introduction rule> $\land\text{-intro}$ on 8, 6
| 10
| $\{1,4\}$
| $\exists x\,(R(x)\land\neg S(x))$
| <existential quantifier introduction rule> $\exists\text{-intro}$ on 9; witness $a$
| 11
| $\{1\}$
| $\exists x\,(R(x)\land\neg S(x))$
| <existential quantifier elimination rule> $\exists\text{-elim}$ on 3, 10; discharge 4; $a$ fresh
The witness $a$ occurs in no undischarged premise or final conclusion. Therefore the <existential quantifier elimination rule> is valid and gives
$$
\boxed{(\forall x\,(Q(x)\to R(x)))\land(\exists x\,(Q(x)\land\neg S(x)))\vdash\exists x\,(R(x)\land\neg S(x)).}
$$
Back to article page
