Could someone help me formally define logical quantifiers ($\forall, \exists$)?
I'm thinking that I could define $\forall$ as the logical conjunction of predicates which take in elements from a set as its argument:
$\forall_{x \in X} (P(x)) := \land_{x \in X} (P(x)) = P(x_1) \land P(x_2) \land P(x_3) \land \cdots$
But, I have yet to define what a set is. Furthermore, I also need the quantifiers to define what a set in ZFC set theory.
So I'm pretty much in a deadlock.
On
There are two broad approaches to defining the "meaning" of quantifiers (and logical connectives in general): syntactically or semantically.
In the syntactic approach, rules are given for how to manipulate formulas containing the connectives. There are multiple sets of rules you can use. Structural proof theory makes a fairly compelling case for some choices and does a good job of separating the connectives from each other rather than having all their meanings intertwined. For example, in Natural Deduction, universal quantification is handled by the following two rules:$$\cfrac{\Gamma\vdash P(x)\quad x\text{ not free in }\Gamma}{\Gamma\vdash\forall x.P(x)}\forall I\qquad\cfrac{\Gamma\vdash\forall x.P(x)}{\Gamma\vdash P(t)}\forall E$$ The first states that if $P(x)$ is derivable given the statements in $\Gamma$ and the variable $x$ is not free in any of the statements in $\Gamma$, then we can derive that in context $\Gamma$, $\forall x.P(x)$. The second states that if $\forall x.P(x)$ is derivable in context $\Gamma$, then in context $\Gamma$, $P(t)$ is derivable where $t$ is any term.
For a semantic approach, we interpret formulas into mathematical objects. Traditionally, the mathematical objects are sets, but I think this produces a misleading view of the meaning of the connectives. While the traditional approach definitely gives an appropriate semantics for classical predicate logic, it is not appropriate for most non-classical logics. We can, nevertheless, easily define the quantifiers for most of those non-classical logics. For example, the syntactic rules above are the same for classical and intuitionistic predicate logic. Mauro ALLEGRANZA's statement: "[a] universal quantifier is a (potentially) infinite conjunction" is true for set-theoretic semantics of classical predicate logic, but isn't true at all for many other logics. Even for classical predicate logic, it can be misleading. For non-classical logics, it can be completely meaningless. Instead, we should endeavor to find the minimal mathematical structure needed to interpret a connective. Categorical logic attempts to do this. Combined with the aforementioned modularity of structural proof theory, we get to a situation where we can specify properties of a category to support only the connectives we care about like Lego blocks. Alternatively, we can look at what structure a given category has and thus see what logical connectives can be interpreted into this category. This leads to the very powerful idea of an internal logic/internal language.
The categorical approach can lead to radically different semantics and this makes logic deeply relevant to far more areas of math than it has been traditionally. Homotopy Type Theory is a dramatic recent example. If you have little or no experience with category theory, the following probably won't mean much to you, but I'll present it anyway. It is a bit of a simplification from the usual, more general approach. First, we can notice that we usually have or can derive the following rules: for formulas $\varphi$,$\psi$, and $\chi$, $\varphi\vdash\varphi$, and if $\varphi\vdash\psi$ and $\psi\vdash\chi$ then $\varphi\vdash\chi$. This makes the set of formulas and the entailment relationship into a preordered set. Now, we take a category $\mathcal C$ that we'll intuitively think of as a category of variable contexts. That is, we'll interpret variable contexts like $x:S,y:T,z:S$, which describes having variables $x$ and $z$ of sort $S$ and a variable $y$ of sort $T$, as objects of $\mathcal C$. To this end, it is common to require that $\mathcal C$ has finite products so that a multi-variable context can be viewed as a product of single variable contexts. (Traditionally, classical predicate logic is often presented in a single-sorted way so there is no need to explicitly declare the sort of a variable.) We can then consider a functor $P:\mathcal C^{op}\to\mathbf{Proset}$ where $\mathbf{Proset}$ is the category of preordered sets and order-preserving (i.e. monotonic) functions. (A categorist would call this an indexed $(0,1)$-category.) The idea is that for a variable context $C$ in $\mathcal C$, $P(C)$ represents the (interpretation of the) preordered set of formulas. Suppressing the sorts to reduce noise, we might decorate the turnstile with the available variables, e.g. $\varphi\vdash_{\{x,y,z\}}\psi$ where only $x$, $y$, and $z$ may appear as free variables in $\varphi$ and $\psi$. Since $\mathcal C$ has finite products, we can project off variables in our contexts, i.e. we have a map in $\mathcal C$ that takes e.g. $\pi_z:\{x:S,y:T,z:S\}\to\{x:S,y:T\}$ and similarly for all other variable contexts. $P(\pi_z)$ is then a monotonic (i.e. entailment preserving) function that takes a formula $\varphi$ with (potential) free variables $x$ and $y$ to $\varphi$ with (potential) free variables $x$, $y$, and $z$, but since it's the same formula, it clearly can't possible use $z$. Universal quantification is then the statement that $P(\pi)$ has a right adjoint (or, as it would be called in this context, a Galois connection) for all projections $\pi$, and that a certain extra condition which basically states that substitution commutes with the universal quantifier if they talk about different variables. (Incidentally, existential quantification is the left adjoint.) The natural deduction rules I mentioned above correspond to core parts of this adjunction.
Conjunction corresponds to the existence of a greatest lower bound (a meet) in each preordered set. Existence of "infinite" conjunctions would correspond to having complete lattices (among other things) which is neither assumed nor implied by the above characterization of the universal quantifier. Roughly and intuitively speaking, universal quantification implies that the "truth" of the quantified formula is "uniformly" or "continuously" or "smoothly" "true" as the quantified variable changes. Conjunction, infinite or otherwise, is more "pointwise" Even in classical logics, aspects of this appear, e.g. in the notion of $\omega$-(in)consistency.
Perhaps it would help things to point out that the formula $(\forall x\in X) [P(x)]$ is actually an abbreviation of a more correct formula $(\forall x)[(x\in X)\to(P(x))]$ where in principle the universal quantification is over everything that there is in the set-theoretic sense. Other than that you don't "define" quantifiers.