One of the concepts that I have had some difficulty fully comprehending is the deployment of Universal Generalization in proofs. Here is what I think I understand correctly.
Let's say that I want to prove some generic, universally quantified statement like $\forall x \varphi (x)$ with respect to some domain of discourse $\mathcal D$. I know that if I prove $\varphi(y)$ with respect to $\mathcal D$, where $y$ is a variable that has "no assumptions placed on it", then I can conclude $\forall x \varphi (x)$ with respect to $\mathcal D$.
However, it appears to me that there is, implicitly, an assumption that must be placed on $y$: specifically, that $y$, although arbitrary, must exist within $\mathcal D$.
Therefore, at the outset of any proof strategy that invokes Universal Generalization, it seems like I always need to establish that my arbitrary $y$ resides within the domain of discourse.
Firstly, is this correct?
Secondly, how should one formally assert this?
The axiomatic framework that I have been recently working with is ZFC, and an easy example that I can think of that captures my above outline is the statement:
$\forall x (\emptyset \subseteq x)$ where $\varphi(x):=\emptyset \subseteq x$ ... or more formally: $\forall x \big (\forall z ( z \in \emptyset \rightarrow z \in x) \big )$
I would start this proof off by saying:
Let $x'$ be an arbitrary element in our domain of discourse.
Prove: $\forall z (z\in \emptyset \rightarrow z \in x')$.
Then I would say:
Let $z'$ be an arbitrary element in our domain of discourse.
Prove: $z' \in \emptyset \rightarrow z' \in x'$
etc etc.
My question is thus: What do I need to do to demonstrate that $x'$ and $z'$ are elements in our domain of discourse? What is the FOL justification that $x'$ and $z'$, in fact, reside within our domain of discourse?
Hopefully this question is sufficiently clear.
Cheers~
If you have some flexibility, i.e. you are not committed to a particular form of FOL*, then this problem could be avoided if all domains of quantification were may explicit as is usually the case in mathematical proofs. This would also allow different domains for different quantifiers even within the same statement.
If $D$ is your domain of quantification (a set in this case), then you would write universal generalizations in the form:
(1) $~~~~~~\forall x \in D: P(x)~~~~~~$OR$~~~~~~\forall x:[x\in D \implies P(x)]$
You would write existential generalizations in the form:
(2) $~~~~~~\exists x\in D: P(x)~~~~~~$OR$~~~~~~\exists x:[x\in D \land P(x)]$
To prove a statement of the form (1), you could start with an assumption that $x\in D$. Then it wouldn't matter if $D$ was empty or not. It would matter if you wanted to infer $P(x)$ from (1). Then $D$ would have to be non-empty.
$*$ If you are committed to a form of FOL that does not make the domain explicit on every quantifier, it may help to imagine all of this going on "behind the scenes" with the same unspecified, non-empty domain on every quantifier (as is the convention).