Confusion about definition of $\forall x P(x)$ and about the universal quantifier in general

Question

In this question I saw the definition (neglecting domain of discourse) $$\forall x P(x) = \forall x ( \;x \in A \Longrightarrow P(x) \;).$$

Why isn't the $\forall$ symbol redundant on the RHS? That is, why not just write $$\forall xP(x) = x ( \;x \in A \Longrightarrow P(x) \;)?$$

What is wrong about this? Also, if the latter definition is indeed wrong, then how does one actually define the universal quantifier? I know in categorical logic it's definable as an adjoint, and that definition seems to use implication alone (though I'm not sure).

I'm also confused by this MO question where it's written either existential or universal quantification must be taken as a primitive... How does this settle with the categorical definition?

Answer 1

I saw the definition (neglecting domain of discourse)...

If we neglect $x∈A$ the two formulae are not the same.

The so-called bounded quantifiers

$\forall x \ \in A : P(x)$ and $\exists x \ \in A :P(x)$

are abbreviations respectively for the two formulae :

$\forall x (x \in A \to P(x))$ and $\exists x (x \in A \land P(x))$.

The "official syntax" is : $\forall x \varphi$ and $\exists x \varphi$.

In many mathematical context, where the proof is "restricted" to a specific context, like e.g. natural numbers, it is very useful to abbreviate the longer : $\forall n (n \in \mathbb N \to P(n))$ with $\forall n \in \mathbb N : P(n)$.