Universal quantifier and infinitary conjunction Out of curiosity, if we are working in the category of sets using an infinitary first-order logic, do we have the following equivalences ?
$$\forall x\in\mathbb N:P(x)\Leftrightarrow\bigwedge_{x\in\mathbb N}P(x)$$
$$\forall x\in\mathbb R:P(x)\Leftrightarrow\bigwedge_{x\in\mathbb R}P(x)$$
I'm wondering about the eliminability of the quantifiers (I could have asked the same question for the existential quantifier and disjunction).
Addendum :
Here is the theoretical background of the above question.
Let's consider the category $\textbf{Sets}$ of sets and its internal language (which is classical, since $\textbf{Sets}$ is a bivalent boolean topos). Since $\textbf{Sets}$ is also a geometric category, we can add an infinitary conjunction operator to its internal language, allowing the use of formulas such as :
$$\bigwedge_{x\in\mathbb R}P(x)$$
where the indexing set $\mathbb R$ is external to the language, and as long as for each $x\in\mathbb R$, $P(x)$ is a well-defined formula. But since we are in $\textbf{Sets}$, its internal set $R$ of real numbers corresponds to the external $\mathbb R$, so each $x\in\mathbb R$ corresponds to a canonical global element $x:\boldsymbol{1}\rightarrow R$ (and I still use "$x$" to name it). In the internal semantics, $P(x)$ is then to be understood as being an arrow $P\circ x:\boldsymbol{1}\rightarrow\{\textrm{true},\textrm{false}\}$ (and $P$ is a predicate on $R$, i.e. an arrow $P:R\rightarrow\{\textrm{true},\textrm{false}\}$).
Finally, since the internal language is typed, we have a typed universal quantification "$\forall_{x\in R}$. My question is thus : in $\textbf{Sets}$, are the following formulas equivalent in it internal logic ?
$$\forall_{x\in R}P(x)$$
$$\bigwedge_{x\in\mathbb R}P(x)$$
I hope my question makes sense...
 A: I'm not an expert on infinitary logic (especially in the classical case), but I would strongly suspect that this is not the case.
First, in many non-classical logics, it's definitely not the case. Intuitively, the universal quantifier states that the predicate holds "uniformly"/"smoothly"/"continuously" in the quantified variable, while the infinite conjunction only requires it to hold "pointwise".
Even for classical logics though, the issue that you have is that the $\mathbb N$ on the left, call it $N$, is not the same as the $\mathbb N$ on the right. $N$ is either a sort or an object of the logic, while $\mathbb N$ is an object of the meta-logic. There's no guarantee at all that the meta-logical $\mathbb N$ contains all the elements of the interpretation of $N$. More critically, there's no reason to expect that there is a numeral for every element of the interpretation of $N$. This is why we can have $\omega$-inconsistent theories.
I recently got around to reading Edward Nelson's work on Internal Set Theory (IST) and even if you don't care about the nonstandard analysis aspect, it is an excellent exercise in logic, set theory, and the distinctions between the object language and the meta-language. IST is a conservative extension of ZFC, so every theorem of ZFC holds in IST with the same proof no less. IST adds to the language of ZFC one new predicate symbol $\mathsf{St}$, where $\mathsf{St}(x)$ is read as "$x$ is standard". The axioms added to IST allow you to prove that there is a nonstandard set and, in fact, every infinite set has nonstandard elements. We can prove that $0$ is standard, and if $n$ is standard, so is $n+1$. We can prove that every nonstandard element of $\mathbb N$ is greater than any standard element of $\mathbb N$. This allows us to define (in the reals) the notion of "infinitesimal" as being smaller than the reciprocal of a nonstandard natural. Now a model of the reals of IST is the hyperreals. One of the problems with Robinson-style nonstandard analysis is that the hyperreals are not an Archimedean field, meaning $\forall x\in\mathbb R.x>0\implies\exists n\in\mathbb N.nx>1$ doesn't hold. Of course, the reals are an Archimedean field in ZFC and so they are in IST too. The issue is the Archimedean property in IST gets interpreted as "for all positive hyperreals, there exists a hypernatural ..." while asking if the hyperreals is Archimedean is asking if "for all positive hyperreals, there exists a natural number ..." where "natural number" is the meta-logic's notion of "natural number". The idea of the hyperreals is to have the meta-logic's notion of "natural number" correspond to the (proper!) class of standard natural numbers within the logic. It is not true in IST that for every positive real, $x$, there exists a standard natural number, $n$, such than $nx>1$.
Category theory also provides perspective on this. A short way of describing my earlier paragraphs is that to interpret (classical) first-order logic we need a (Boolean) hyperdoctrine. There are many (Boolean) hyperdoctrines other than $\mathbf{Set}$. (And many more if we drop the Boolean requirement, i.e. allow non-classical logics including ones where "continuously" or "smoothly" can be taken quite literally.)
However, if you just mean for these expressions to just refer to constructions within the given category of sets, then for "usual" set theories they refer to more or less the same thing. Spelling this out, $\bigwedge_{n\in\mathbb N}P(n)$ is just the $\mathbb N$-indexed product of the subobjects $P(n)$ in $\mathsf{Sub}(X)$, the poset of subobjects (i.e. subsets) of $X$ which is a wide pullback in $\mathbf{Set}$. That is, it's $\bigcap_{n\in\mathbb N}P(n)$. $X$ represents a set over which the free variable(s) ranges. It will be $1$ in the closed case. Viewing $\mathsf{Sub}$ as an indexed $(0,1)$-category, the weakening functor, $\pi^*$, takes a subset $S$ to $\pi^{-1}(S)$. Universal quantification is the right adjoint which is to say we're looking for an operation on subsets, $\forall_Y$, such that $\pi^{-1}(S)\subseteq T\iff S\subseteq\forall_Y(T)$ where $S\subseteq X$ and $T\subseteq X\times Y$. Calculating, we have $$\begin{align}
& \pi^{-1}(S)\subseteq T \\
\iff & \forall x\in X.\forall y\in Y.(x,y)\in\pi^{-1}(S)\implies (x,y)\in T\\
\iff & \forall x\in X.x\in S\implies\forall y\in Y.(x,y)\in T \\
\iff & \forall x\in X.x\in S\implies x\in\bigcap_{y\in Y}\{z\in X\mid (z,y)\in T\} \\
\iff & S\subseteq\bigcap_{y\in Y}\{z\in X\mid (z,y)\in T\}
\end{align}$$
What's special about $\mathbf{Set}$ is that we can identify a family of (sub)sets with a (sub)set. This is related to the equivalence of categories $\mathbf{Set}^I\simeq\mathbf{Set}/I$ where we view the set $I$ as a discrete category on the left. $\bigwedge_Y : \mathsf{Sub}(X)^Y\to\mathsf{Sub}(X)$, while $\forall_Y : \mathsf{Sub}(X\times Y)\to\mathsf{Sub}(X)$. Given $F:Y\to\mathsf{Sub}(X)$ we get a subset of $X\times Y$, i.e. an object of $\mathsf{Sub}(X\times Y)$, via $\bigcup_{y\in Y}F(y)\times\{y\}$. Going the other direction, we can define $F:Y\to\mathsf{Sub}(X)$ from $T\subseteq X\times Y$ via $F(y)=\{x\in X\mid (x,y)\in T\}$. This identification doesn't even make sense for most other categories, $Y$ is always a set in $\bigwedge_Y$, which is why $\bigwedge_Y$ and $\forall_Y$ are usually not the same. If the category has copowers or a way of embedding $\mathbf{Set}$, e.g. viewing sets as discrete spaces, then you may be able to get something similar, but it will likely be limited, i.e. $\bigwedge_Y$ corresponds to $\forall_Y$ for $Y$ that are "discrete" in some appropriate sense.
A: In the infinitary logic $L_{\infty\infty}$, neither $\forall x\in \mathbb{N}: P(x)$ nor $\bigwedge_{x\in \mathbb{N}} P(x)$ are well-formed formulas! 
$\forall x\, P(x)$ is certainly a formula. But here $x$ ranges over the entire domain of a model. You might have a particular model in mind with domain $\mathbb{N}$, but this won't be the case in general. Alternatively, you might be working in a many-sorted logic, in which case you have the well-formed formula $(\forall x\in S)\, P(x)$, where $S$ is a sort. If your sort is named $\mathbb{N}$ (which is a terrible idea, notationally), then $(\forall x\in \mathbb{N})\, P(x)$ is a well-formed formula, but in a general model there's no reason why the sort $\mathbb{N}$ should be interpreted as the natural numbers.
The other formula $\bigwedge_{x\in \mathbb{N}} P(x)$ is even worse, because $x$ shouldn't be both a variable and a natural number! The closest thing that would be a well-formed formula is $\bigwedge_{n\in \mathbb{N}} P(c_n)$, where $\{c_n\mid n\in \mathbb{N}\}$ is a family of constant symbols indexed by the natural numbers. 
Now trying to find a context where something like both of your formulas make sense... Let's imagine we have a sort named $N$ and constant symbols $\{c_n\mid n\in \mathbb{N}\}$ of sort $N$ in the language. Then we could write down the formulas $(\forall x\in N)\,P(x)$ and $\bigwedge_{n\in \mathbb{N}} P(c_n)$. But still, these formulas aren't equivalent, since in an arbitrary structure there might be other elements of sort $N$ that aren't named by a constant symbol. But they are equivalent modulo the axiom $(\forall x\in N)\, \bigvee_{n\in \mathbb{N}}(x = c_n)$, which asserts that every element of sort $N$ is named by a constant.
