What are standard ways to write mathematical expressions involving quantifiers in a (semi)formal way ?
In different posts of mine concerning similar question I have encountered for a generic expression of the type "for all $x\in I$ and $y\in J$ holds $P(x,y)$" the following writing conventions
1) $\forall y\in J \ \ \forall x \in I: P(x,y)$ (this was how I would usually write statements in a formal way; sometimes also as $\forall y\in J: \ \ \forall x \in I: P(x,y)$ ;don't know if it standard)
2) $(\forall y)(\forall x)(x \in I \land y\in J \Rightarrow P(x,y))$ (in the accepted answer from this question)
3) $(\forall y: \ y \in J) (\forall x: \ x \in I) (P(x,y))$ (form the same answer as above)
4) $\forall y \ \forall x\ (x \in I \land y \in J \Rightarrow P(x,y))$ (in the accepted answer fromthis question)
5) $(\forall y\in J )(\forall x \in I) [P(x,y)] $ (in the accepted answer from this question).
( (I hope I "generalised" them correctly, because at some points, they where written only for one variable, for example 3) was written just as $(\forall x: \ x \in I) (P(x))$ )
Could you tell me which ones are generally accepted an if there is a standard to how these should be written ?
(I think unique readability should be a criterion and I'm not sure the way I'm used to writing mathematical expression satisfies that)
Best Answer
As your own survey shows, there is no real standard here. In general is is acceptable to write whatever is likely to be understood -- except perhaps in a class setting where the formal notation itself is the subject of the course, rather than just a background skill.
The design space can roughly be classified as
Punctuation. Parentheses/brackets around the quantifier? Colon, space, or dot? (Dots seem to be found mainly among computer scientists, perhaps influenced by the lambda calculus). Parentheses around the body formula? Nobody really cares about these choices, except that, as always, being consistent within a book or paper is a plus.
Multiple quantifiers. Some authors allow multiple quantifiers of the same kind to be collapsed into one piece of syntax, such as $(\forall x, y)P(x,y)$ instead of $(\forall x)(\forall y)P(x,u)$. This is almost always just treated as an abbreviation.
Precedence. When the syntax doesn't include explicit brackets around the body formula, the problem of delineating the scope of the quantifier arises. Does $\forall x : \phi \to \psi$ mean $(\forall x:\phi)\to\psi$ or $\forall x:(\phi\to\psi)$? There is a real risk of misunderstanding here, and unfortunately there doesn't seem to be a real consensus about the binding strength (at least not if we include computer science). Formal metamathematics generally insist of having everything fully parenthesized in principle, but seldom adhere to this in running text anyway. When there is any doubt, put in too many parentheses rather than too few!
Bounds. Here's a real distinction. In formal logic the "real" quantifiers are almost always "naked" and range over the entire universe. Most presentations allow bounds within the quantifiers in informal notation, but insist that they are really abbreviations for, say $\forall x(x\in I\to \phi(x))$ or $\exists x(x\in I\land \phi(x))$. On the other hand, in much of mathematics outside formal logic, the very meaning of many short notations (such as $x^y$ or $x'$ or $x^*$ or $x(y)$ or $xy$) depend on what kind of things $x$ and $y$ are. In such a setting, a "naked" quantifier would lead to intolerable confusion and ambiguity, so everyday mathematics almost always uses some kind of explicit bounds in the quantifiers that tell at least what the variable ranges over. It is generally understood that if we need to translate an everyday formula into formal logic, we'll need to expand the bound into a "logician's abbreviation", and use information from the bound to figure out which formal unfolding of $x^*$ to use in the scope of the quantifier.
At least the symbols $\forall$ and $\exists$ are fairly universal these days. In older logical literature (before about 1950) you can find a bewildering variety of quantification notations that don't include these symbols. For example, Gödel's original incompleteness proof notates $\forall x.\phi$ as "$x\Pi(\phi)$" in one part of the development and as "$(x)[\phi]$" in another.