Question: I am getting suspicious that there is no need whatsoever for quantifiers in formal first-order logic. Why do we write $\forall x, P(x)$, when can simply write $P(x)$, assuming that we know that $x$ is a variable (as opposed to a constant).

A similar question has been asked here: [Is the universal quantifier redundant?](https://math.stackexchange.com/questions/4088337/is-the-universal-quantifier-redundant), and a commenter states that the order of quantifiers matters. Indeed, the order of mixed quantifiers matters, but all existential quantifiers can be reformulated as universal quantifiers, so in fact the order does not matter.

I'm struggling to think of a case where a quantifier provides essential information for a statement.

Answer: 
The problem with replacing $\exists$ with $\neg\forall\neg$ to not have to worry about the order of quantifiers becomes apparent if you actually try doing so and omitting the quantifiers. For instance, $\exists x P(x)$ becomes $\neg \forall x \neg P(x)$ and then you omit the quantifier to get $\neg\neg P(x)$. Wait, that's equivalent to just $P(x)$, which would mean $\forall xP(x)$ under your convention. So $\exists x P(x)$ turned into just $\forall xP(x)$, which isn't right!

The problem here is that the order of negation and universal quantifiers matters. That is, $\forall x\neg P(x)$ is different from $\neg\forall x P(x)$ (so $\neg \forall x \neg P(x)$ is different from $\forall x \neg\neg P(x)$). If you omit universal quantifiers everywhere, you lose this distinction.
Let's consider these two quantified statements:
$$
\begin{align\*}
\forall x\exists y M(x, y) \tag\*{(1)}\\
\exists x\forall y M(x, y) \tag\*{(2)}
\end{align\*}
$$
and let's take the universe of discourse to be people and interpret $M(x,y)$ to mean $y$ is the mother of $x$. Statement (1) says that everybody has a mother while statement (2) say that there there is a person who has every person as a mother. These statements have very different meanings: quantifiers are not redundant.

We write quantifiers to keep close track of the dependencies in our mathematical problems.