# Syntax for complex restrictions on domains of quantifiers

In restricting the domains of the universal and existential quantifiers, all of the examples that I've seen take the form: $\forall x \in X[P(x)]$. But what is the correct syntax for more complicated domain restrictions such as $x \in \mathbb{R}$ and $x < 0$?

Consider an assertion like: "The equation $x^2 + a = 0$ has a real root for any negative real number, a."

I know that this can be expressed as: $\forall a \in \mathbb{R} \exists x[a < 0 \implies x^2 + a = 0]$.

Can it also be expressed as: $\forall a \in \mathbb{R} \land a < 0 \exists x[x^2 + a = 0]$?

What about $\forall a \in \mathbb{R}, a < 0 \exists x[x^2 + a = 0]$?

Thanks for the help.

• Are you able to cite a source that does not treat your "$\forall x \in X[P(x)]$" as a syntax hack for your equivalent implication, and then only for single operator constraints? It may help you to know that your initial predicate variable constraint is sensical in a order-sorted logics, but your complex constraint is not, except using the equivalent implication for the non-sort constraint. – Eric Towers Jun 20 '18 at 0:13
• Sure. Here's an example from U of Maine: "Universal Quantifier: $(\forall x \in U) P(x)$ means "for all (or any) x in the set U, such that P(x) is true." The link is: math.umaine.edu/~farlow/sec13.pdf The Stanford MOOC (Introduction to Mathematical Thinking) I'm taking uses that same syntax and shows it as equivalent to the implication version. Nothing I've seen suggests that it is a hack. Anyway, given that there is syntax for applying a quantifier to set membership, it seemed natural to ask whether you could apply a quantifier to more complex expressions in order to limit the domain. – Geoff Jun 20 '18 at 1:14
• Another common example is $(\forall x < 0)P(x)$. From U of Arizona: "$\forall x > 0\exists y(y^2 = x)$". Link is here: math.la.asu.edu/~boerner/mat243/… But never anything more complex than that. Again, since it there is syntax for applying a quantifier to an inequality to limit domain, it seemed reasonable to ask whether the same syntax could be applied for a more complex expression. – Geoff Jun 20 '18 at 1:25

"The equation $x^2+a=0$ has a real root for any negative real number $a$"

"for every $a$, if $a$ is real and negative, then the equation $x^2+a=0$ has a real root",

i.e. :

"for every $a$, if $a$ is real and negative, then there is a $b$ such that $b$ is real and $b^2+a=0$."

Now we can easily symbolize it :

$\forall a \ [(a \in \mathbb R \land a < 0) \to \exists b \ (b \in \mathbb R \land b^2+a=0)]$,

or equivalently :

$\forall a \ \exists b \ [(a \in \mathbb R \land a < 0) \to (b \in \mathbb R \land b^2+a=0)].$

Note. If we want to use the restricted quantifier notation, we can rewrite is as follows :

$\forall a_{(a \in \mathbb R \land a < 0)} \exists b_{(b \in \mathbb R)} \ (b^2+a=0),$

or, in an "intermediate" version as :

$\forall a_{(a \in \mathbb R)} \exists b_{(b \in \mathbb R)} \ (a < 0 \to b^2+a=0).$

IMO, we have not gained so much regarding readibility.

• Thanks very much for clarifying and including the link on restricted quantifier notation. – Geoff Jun 20 '18 at 15:15
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.8594877123832703, "perplexity": 531.8091277678045}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2021-25/segments/1623487630175.17/warc/CC-MAIN-20210625115905-20210625145905-00106.warc.gz"}