Are quantifiers redundant by treating free variables as implicitly universally quantified?

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?, 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 1

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.

Answer 2

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.

Answer 3

Rob Arthan's answer is exactly right; let me supplement it with an observation from computability theory.

Consider the structure $\mathcal{N}=(\mathbb{N};+,\times)$. It turns out that the quantifier hierarchy over $\mathcal{N}$ is non-collapsing: no fixed number of quantifiers will ever be sufficient for capturing all the definable sets in $\mathcal{N}$. This turns out (with a slight tweak re: bounded quantifiers, resulting in the arithmetical hierarchy) to have a computational interpretation, according to which definability with $n$ alternations of quantifiers + as many bounded quantifiers as you like corresponds to computability relative to the $n$th "iterated Halting Problem."

So in a precise sense, "few-quantifier" expressions are quantitatively less powerful than "many-quantifier" expressions.