show/hide this revision's text 3 Answered additional questions.

To comment on the second part of your question:

When we talk about formal languages, we do this in another formal language, the so-called "meta-language". If you want to talk about the theory of the natural numbers (that is, the formulas satisfied by the structure of the natual numbers), you do this in a meta-language, usually ZFC, in which you can define the set of natural numbers, the set of formulas, and what it means for a formula to be true.

In classical logic, you just translate the universal quantifier of the language to the universal quantifier of the meta-language. $\forall x \varphi(x)$ is true iff $\varphi(t)$ is true for all $t$. All we've done is defined the universal quantifier in the language using the universal quantifier in the meta-language.

So if you want to define a domain of discourse as $\{x|\varphi\}$, $\varphi$ can be any formula in the meta-language. So if you use higher-order logic as metalanguage, $\varphi$ can be any higher-order formula.

As for syntactical rules: You do not need a domain of discourse in order to syntactically derive valid formulas, because all you do is manipulating strings. The introduction rule for universal quantification just says that if you can prove $\varphi(x)$ (which means that the proof cannot depend on the value of $x$), then you can prove $\forall x \varphi(x)$. This is just adding two symbols at the beginning of a formula.
show/hide this revision's text 2 Fix typo.

There are two main ways to define universal quantification.

Syntactically. You can introduce a universal quantification if the variable is free in none of the hypotheses, and you can eliminate a universal quantifier and substitute some term for it (provided there are no name clashes). These are the introduction rule ($\Gamma\vdash \varphi \Rightarrow \Gamma\vdash \forall x \varphi$ if $x$ is free in $\Gamma$) and the elimination rule ($\Gamma\vdash \forall x \varphi \Rightarrow \Gamma\vdash \varphi[t/x]$ if $t$ is free for $x$ in $\varphi$) respectively in natural deduction calculus.

Semantically. $\forall x P$\varphi$ is true iff $P[t/x]$\varphi[t/x]$ is true for all $t$ in the domain (i.e. where $x$ is substituted with a an element of the domain $t$).
show/hide this revision's text 1

There are two main ways to define universal quantification.

Syntactically. You can introduce a universal quantification if the variable is free in none of the hypotheses, and you can eliminate a universal quantifier and substitute some term for it (provided there are no name clashes).

Semantically. $\forall x P$ is true iff $P[t/x]$ is true for all $t$ in the domain (i.e. where $x$ is substituted with a an element of the domain $t$).