Word-by-word translation into formal logic: "For all $x$ ($Px$ implies that $Qx$ is constant)"

Question

$Q(x)$ is constant on set $A$ means: for all $x\in A$, $Q(x)$ is not depended on $x$.

Is it possible to translate the following formula into formal logic word-by-word?

$\forall x\in \{y:P(y)\}$ ($Q(x)$ is constant.)

The translation of "$Q(x) $ is constant" should be: "$\forall xQ(x)\lor\forall x\neg Q(x)$"; however, this cannot be directly substituted into the original formula, as the "proper translation" should be $\forall x(Px\implies Qx)\lor \forall x(Px\implies \neg Qx)$, which cannot be further simplified. We seem to have a paradox here.

My guess: Rigorously speaking, we can only say that a predicate, $Q(\cdot)$, is constant. We cannot that say a proposition is constant. Note that for each $x$, $Q(x)$ is a proposition.

Motivation: one helpful member once give me a statement: "(For any $y$), all functions with a root have the same sign at $y$". I have a hard time translating this concise statement word-by-word into formal logic. I was thinking that not every rigorous natural language has a word-by-word translation into formal logic.

Answer 1

Your original formula is in a mixture of informal and formal language. The only reasonable way to read the informal "$Q(x)$ is constant", is to take it as having $x$ as a bound variable (by the usual abuse of terminology, where we talk about a function $f(x)$, when it is really $f$ that is the function). So you have to read the $x$ in "$Q(x)$ is constant" as different from the $x$ that appears as the argument in $P(x)$. So using your way of formalising "$Q(x)$ is constant", the resulting formalisation (with bound variables renamed for clarity) is: $$ \forall x (P(x) \implies ((\forall y Q(y)) \lor (\forall y\lnot Q(y))) $$ I would have a slight stylistic preference for formalising "$Q(x)$ is constant" as $\forall y,z(Q(y) \Leftrightarrow Q(z))$, giving: $$ \forall x (P(x) \implies (\forall y,z(Q(y) \Leftrightarrow Q(z))) ) $$ as an alternative answer (which reads more like what you would write if you wanted to formalise "$f(x)$ is constant", where $f$ is a function symbol).

On your final point, I would say that every rigorous mathematical statement can be translated into formal logic (essentially because that is the only way to define the concept of a "rigorous mathematical statement"). However, you can't expect the translation to be word-for-word in all cases.

Note: the question has been edited since I posted the above answer. The edit has moved it further away from being a question about how to formalise natural language and further towards how to disentangle a poor attempt to mix formal language and informal language.

Answer 2

Here are two ways to say that the predicate $Q$ is constant on the set of objects that satisfy $P$:

$(\forall x(Px\implies Qx))\lor(\forall x(Px\implies \lnot Qx))\tag{1}$

$\forall x,y((Px\land Py)\implies(Qx\iff Qy))\tag{2}$

If $Q$ is a function symbol instead of a relation symbol (see here), then expressions analogous to the above ones are:

$\exists y\forall x(Px\implies Qx=y)\tag{3}$

$\forall x,y((Px\land Py)\implies Qx=Qy)\tag{4}$

You might be hoping for something like (3) that works when $Q$ is a predicate. But the symbol $\exists$ in first-order logic always ranges over objects, not truth values, so there's no direct translation. Instead, the claim "there exists a truth value" translates into the disjunction of a "true case" and a "false case", so you get (1).