I continue studying predicate logic, though not quite rigorous just yet, and continue asking question about quantifier. This time is about this page: If I want to avoid quantifiers?
I realize that the sentence $\forall x[Px]$ can be true or false, depending on the interpretation. However, whatever the interpretation is, isn't it true the variable $x$ must be in some domain $D$?
Hence, as suggested on that page, since when we learned about proving statement in propositional logic (probably in undergraduate courses), we treated proving $\forall x\in D,[Px]$ as proving $x \in D \implies Px$, why can't we just replace all quantifiers with $x\in D \implies Px$ in the case of $\forall$, and $x\in D\land Px$ in the case of $\exists$?
It is not quite a removal of quantifiers, but replacement perhaps? From universal to implication or from existential to conjunction or something like that? I am not quite sure myself, but when I learned about proving mathematical statement, $\forall x\in D,[Px]$ is logically equivalent to $x \in D \implies Px$ when interpreted. I also know that $\forall x\in D,[Px]$ is equivalent to $\forall x[x\in D \implies Px]$ formally in predicate logic, but why should, in the case of universal quantifier for instance, the statement $\forall x\in D,[Px]$ be different from $x \in D \implies Px$ (no "for all") when translated? "For all $x\in \mathbb{R}, x^2\geq 2$" sounds pretty much the same with "If $x\in \mathbb{R}$, then $x^2\geq 0$", but predicate logic treats them differently, in fact different things as one is a sentence and the other is just a formula, unless we add something to have "For all $x$, $x\in \mathbb{R}\implies x^2\geq 2$".
One says that "If $x\in \mathbb{R}$, then $x^2\geq 0$" is only informally stated and that it implicitly starts with a universal quantifier, since it has to be that way to become a sentence according to PL.
Moreover, one might argue that this $x \in D \implies Px$ might follow $\exists x$, which becomes $\exists x[x \in D \implies Px]$. Hence, quantifier must be specified, otherwise it would be unclear. But then again, if one wants to say that, it can be transformed into $x\in somewhere \land [x \in D \implies Px]$, no?
So in general, why is quantifier that necessary to express? If by doing the above translation, the expressive power of such logic is significantly less than the one containing quantifier, in what example can that be seen?
Feel free to correct my misunderstanding of logical statement, as I strongly believe it exists but I don't know where.
Best Answer
I think you have more or less understood the issue. If your formula has free variables, it is an 'open' formula with no specific truth value. Quantifiers let you form 'closed' formulae (called sentences) that have a specific truth value (given any model). Note that if the model has a finite domain, and you are only interested in talking about that single model, then you can easily replace "$\forall$" by an appropriate conjunction, and "$\exists$" by an appropriate disjunction. However, it is impossible to do so when you want to make statements about arbitrary models (even if they are guaranteed to be finite).
In some mathematical writings, people conventionally assume that all free variables are implicitly universally quantified, but that just means that the quantifier is merely hidden, and not that it was actually 'removed'. Also, under that same convention, the existential quantifier cannot be expressed with a quantifier-free formulation. For example, "$\forall x \exists y ( x \ne y )$" is one way of saying that there is more than one object. By the convention "$x \ne y$" would mean that every $x$ is distinct from every $y$, which is obviously different.
Furthermore, you cannot arbitrarily change the convention and stipulate that different variables refer to different objects, otherwise you cannot say "$\exists x \forall y ( x = y )$" to mean that there is exactly one object.
The bottom-line is that no matter what convention you choose, you have to have some mechanism for expressing quantification otherwise you would never be able to handle classical logic.