Is there formal definition of universal quantification?

Question

From wikipedia quantification has meaning:

In logic, quantification is the binding of a variable ranging over a domain of discourse

Is there any formal "definition" of universal quantifier for example using definition of domain of discourse?

I mean a formula build without universal quantifier, and existential one which has the same meaning if referenced to defined domain of discourse?

For example: Suppose we use domain of discourse (DoD) given by sentence $ U = \{ x|\phi(x) \}$ for some $\phi(x)$. Then naively we may wrote:

($\forall (x \in U) \Phi(x) ) \equiv ( \{ x|\phi(x) \} => \Phi(x) )$

In words: to say that some property follows for every x in DoD is the same as to say that if x is chosen from DoD then has this property.

We may try also the folowing one: ($\forall (x \in U) \Phi(x) ) \equiv (( \{ x|\phi(x) \} => \Phi(x) ) => (\phi(x) <=> \Phi(x) ))$

In words: to say that some property follows for every x in DoD is the same as to say that $\phi$ and $\Phi$ are evenly spanned.

Do You know any reference for such matter?

---

Gabriel: Yes, I agree that from formal point of view in mathematical practice DoD is a set and to extend it to bigger universe usual is done by pure formal way and may be changed to some additional axioms etc. But this is some kind of mathematical practice: "near every decent theory as far as we know is defined for DoD to be set or smaller but as it works also for proper classes we are trying to write it in a way". But then we omit important statement: every time DoD has to be defined and additional axioms about it existence, definition,properties has to be added to the theory. I am only a hobbyist but I do not know any theorem which states: structure to be DoD for formal theory over countable language has to have "this and this" property. Of course for example as in formula $\{ x|\phi(x)\}$ we may require that $\phi(x)$ has some property. For example we may require that it is in first order language. Or in second order. Or in finite order language etc. For me is rather clear that it cannot be whatever I like. As far as I know we do not have any theory for that. But maybe I am wrong?

So my question is: what is that mean "for all" in a context of different definition of DoD ( as well as "there exists"). Do we have clear meaning what it means for very big universes? We use some operator here named "for all" but have we possibility to define its meaning in syntactical way? If not, may we be sure that meaning of sentence "for all" is clearly defined?

I suggest this is example of Incomplete Inductive reasoning about possible ways of using general quantifier in mathematics. Moreover I suppose, even after reading something about Hilbert epsilon calculus that quantifiers has usual only intuitive meaning, that is its definition is far from such level of formality as for binary operation $\in$ for ZFC for example, where it may be anything (for example in von Neumann hierarchy of sets "model" of ZFC it is order). When we try to define formal theory we want to abstract from the "meaning" of the symbols and give only pure syntactical rules for them. As far as I know ( but I know not much) I do not know such definition for quantifiers, even in epsilon Hilbert calculus for example, because it omits the area of possible, acceptable or correct definitions of domain of discourse.

Answer 1

There is a definition in terms of $\varepsilon$-operator of Hilbert. See wikipedia. If not, either universal quantification or existential quantification is taken as primitive in classical logic, for in classical logic, one is derivable from the other. This is not true in intuitionistic logic, as the proof uses the law of excluded middle.

The nLab also has a page related to Hilbert's operator and its relation to the quantifiers.

Answer 2

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 \varphi$ is true iff $\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$).

---

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.

Answer 3

I suppose that the correct one answer for my question was given in 1957 year by Andrzej Mostowski by means of Generalized quantifiers.

In fact this is for me acceptable answer I was looking for, however Hilbert $\epsilon-$calculus seems to be interesting one too. As I accepted this as answer I do not reject this acceptance, but I think Mostowski approach is much interesting one. In this approach generalised quantifiers are related to notion of equality of sets, from which we may clear see what may be the meaning of sentence "for all elements" used for proper classes for example. It is interesting what may happen if one change equality for some weaker relation like equivalence in meaning isomorphism or homomorphism. Note also that meaning of general quantifier is independent of model structure and depends only on universe of discourse. For Hilbert $\epsilon-$calculus it is not so obvious because in constructions You always use certain objects from model. One may to ask if they may be constructed etc.