How to grammatically formalise mathematical statements? I am currently trying to find the best way to express some first-order logic statements. I have several such statements, and I am unsure which gramatical rules I should follow to express them.
For example, I have a statement of the following form:
Let $F\subseteq\{f\mid f:A\to B\}$ be some subset of all functions from $A$ to $B$ and fix $b'\in B$. Then, there exists a function $f\in F$ such that for every element $a\in A$, $f(a)=b'$.
Following some authors in my field whose style I quite like, I am currently expressing such statement formally like this:
\begin{gather}
(\exists f\in F)(\forall a\in A)(f(a)=b')
\end{gather}
I have been suggested to write this:
\begin{gather}
\exists f\in F:\forall a\in A,f(a)=b'
\end{gather}
Or this:
\begin{gather}
\exists f\in F,\forall a\in A:f(a)=b'
\end{gather}
I am wondering whether

*

*some of the above expressions are correct / incorrect to express the statement in italics;


*there exist other valid (and commonplace) expressions to express the statement in italics;


*there exists one preferred formal way to express the statement in italics.
Also, some references that could help me clarify my doubts would also be appreciated.
Thank you all!
 A: *

*By convention, $$∀x\,P(x)→Q,$$ is read as $(2)$ below.


*Does $$∀x\color\red,P(x)→Q$$ mean

*

*“for each $x\color\red,\,P(x)$ being true implies that $Q$ is true” $$∀x\:[P(x)→Q]\tag1$$
or, non-equivalently,

*

*“if, for each $x,\,P(x)$ is true, then $Q$ is true” ? $$\big[∀x\,P(x)\big]→Q\tag2$$
For example, for the usual graph of $y=|x|,$ only the second statement is true: $$\forall x\,(x>0\implies \forall y\:y<0)\\(\forall x\:x>0)\implies\forall y\:y<0.$$


*The colon in the complete statement $$∀x:x^2\ge0$$ clearly does not mean ‘such that’. (elaboration)


*The point is, punctuation symbols in a formalisation don't generally correspond to, or even carry the same meaning as, in a verbal sentence. In the above examples, they aren't meaningful and merely supply breathing space.
But on the other hand, many authors place a punctuation mark after a quantifier specifically to delimit that its scope extends as far right as possible, that is, to signify reading $(1)$ above.
In short, in a symbolic formula/sentence, punctuation symbols can be ambiguous or misleading. They generally don't replace parentheses and are superfluous.
Summary: $$∀x,P(x)→Q\\∀x\,{:}\,P(x)→Q\\∀x.P(x)→Q$$ may be understood either as $$∀x\:[P(x)→Q],\tag1$$ or as the non-equivalent $$∀x\,P(x)→Q\\\big[∀x\,P(x)\big]→Q.\tag2$$


*For human reading, I prefer writing $$∃f{\in}F\; ∀a{\in}A\; f(a)=b'→∀y\;y=b'$$ and the more explicit $$\big(∃f{\in}F\; ∀a{\in}A\; f(a)=b'\big)→\big(∀y\;y=b'\big).$$ (I added the consequent for illustrative purposes.)


*None of your three suggestions \begin{gather}
(\exists f\in F)(\forall a\in A)(f(a)=b')\\
\exists f\in F:\forall a\in A,f(a)=b'\\
\exists f\in F,\forall a\in A:f(a)=b'
\end{gather} are ambiguous, but why use both comma and colon, especially in Example 3? Example 1 is fine.
A: In first order logic all the variables range on a unique set $X$, so no first order statement contains $\exists\ f \in F\ \forall a \in A$, no matter punctuation, parenthesis or italics. Moreover, if $f$ is a symbol for a function in one variable of the language, then any interpretation of $f$ will be a function $f \colon X \to X$.
