I wanted to develop a tree-format natural deduction of the following tautology.
$$ \exists_{x \in S}(P(x)) \quad \implies \quad ( \forall_{y \in S}(P(y) \implies Q(y)) \implies \exists_{z \in S}(Q(z)) \; ) $$
Intuitively I can see how it is true, and I can also see how the proof should work in outline form, informally:
- $\exists_{x \in S}(P(x))$ means there exists an $a$ such that $P(a)$
- $\forall_{y \in S}(P(y) \implies Q(y)$ gives us $Q(a)$ from $P(a)$.
- From $Q(a)$ we get $\exists_{z \in S}(Q(z)))$
The following is my tree-format deviation.
Question: I am concerned my use of the constant symbol $a$ violates the rules for scoping constants used in sub-proofs. Is there an error in the above proof?
Discussion
I think the $a$ introduced in the assumption $[P(a)]^1$ is fine in the conclusion of the $\implies$-elim rule, $Q(a)$.
But I don't think that $a$ should be used in the line $P(a) \implies Q(a)$ because that is not strictly within the scope of the assumption $[P(a)]^1$.
Perhaps I should have $P(b) \implies Q(b)$?
But thinking further, $P(a) \implies Q(a)$ can't be used without the assumption of $a$ and $P(a)$, so maybe the structure of my tree is wrong?
For reference, this answer (link) gives a non-tree natural deduction proof.
My reference for "constant symbol" is this chapter (pdf).
