Pattern matching quantifiers

Question

When using quantifiers semi-formally (e.g., like abbreviation for "it exists" and "for all" on a blackboard), the most reliable and non-ambiguous style is to stay close to the formal syntax and to introduce a single (bound) variable with each quantifier:

• $(\forall x\in\mathbf{R})(x = 0)$,
• $(\forall x\in\mathbf{R})(\exists y\in\mathbf{R})(y = 0)$,
• $(\forall x\in\mathbf{R})(\exists x\in\mathbf{R})(x = 0)$.

(The third sentence is equivalent to the second since $(\exists x\in\mathbf{R})(x = 0)$ says the same thing as $(\exists y\in\mathbf{R})(y = 0)$.)

It is equally unambiguous to introduce several (bound) variables with a single quantifier like in

• $(\forall a,b\in\mathbf{R})(\exists c,d\in\mathbf{R})(a = b = c = d)$,

since this is a simple abbreviation of

• $(\forall a\in\mathbf{R})(\forall b\in\mathbf{R})(\exists c\in\mathbf{R})(\exists d\in\mathbf{R})(a = b = c = d)$.

Additionally, it is common to introduce bound variables by tuples:

• $(\forall (a,b)\in\mathbf{R}^2)(\exists (c,d)\in\mathbf{R}^2)(ac + bd = 0)$.

I suppose that the following is equally allowed:

• $(\forall (a,b)\in X)(\exists (c,d)\in Y)(ac + bd = 0)$,

where $X$ and $Y$ are some given subsets of $\mathbf{R}^2$.

Here it is getting more interesting. How far can this pattern-matching use of quantifiers be pushed?

Is the following a (semi-formally) valid formula?

• $(\forall (a,0)\in X)(\exists (0,d)\in Y)(a = d)$.

How about this one:

• $(\forall (a,0)\in X)(\exists (0,0)\in Y)(a = 0)$.

Or even simpler:

• $(\exists 1\in\mathbf{R})(0 = 0)$.

It seems that with some effort and care, a reasonable meaning of all of the above pattern-matching formulae can be given.

However, suppose that some real parameter $z = 42$ is defined somewhere in the current context, then what is the meaning of the following?

• $(\exists (0,y,z)\in\mathbf{R}^3)(y = z = 0)$.

A similar problem here:

• $(\forall (x,z)\in\mathbf{R}^2)(\exists (0,y,z)\in\mathbf{R}^3)(y = z = 0)$.

My question is: are there any established rules for using pattern matching in quantifiers, at least in semi-formal context?

Any references to respectable textbooks or papers will be appreciated.

Answer 1

Your examples all have the form $$(Q\, t(x_1,\dots,x_n)\in X)\, \varphi(x_1,\dots,x_n)$$ where $Q$ is a quantifier, $t$ is a term which mentions the variables $x_1,\dots,x_n$ (and possibly other constants, and/or parameters), $X$ is a set, and $\varphi$ is a formula which mentions the variables $x_1,\dots,x_n$ (and possibly other variables, constants, and/or parameters).

Such a formula can be viewed as shorthand in the usual way for bounded quantifiers: $$(\exists\, t(x_1,\dots,x_n)\in X)\, \varphi(x_1,\dots,x_n) \Leftrightarrow \exists x_1\dots\exists x_n ((t(x_1,\dots,x_n)\in X)\land \varphi(x_1,\dots,x_n)) $$

$$(\forall\, t(x_1,\dots,x_n)\in X)\, \varphi(x_1,\dots,x_n) \Leftrightarrow \forall x_1\dots\forall x_n ((t(x_1,\dots,x_n)\in X)\rightarrow \varphi(x_1,\dots,x_n)) $$

Your question at the end about reusing variables can then be answered by the usual variable scoping conventions for quantifiers $\forall x$ and $\exists x$ in first-order logic.

---

So your example: $$(\forall (x,z)\in\mathbf{R}^2)(\exists (0,y,z)\in\mathbf{R}^3)(y = z = 0)$$ becomes: $$\forall x\, \forall z\, (((x,z)\in \mathbf{R}^2)\rightarrow \exists y\, \exists z (((0,y,z)\in \mathbf{R}^3)\land (y = z = 0)))$$

and because the last two instances of $z$ are inside the scope of the inner $\exists z$ quantifier, this has the same meaning as:

$$\forall x\, \forall z\, (((x,z)\in \mathbf{R}^2)\rightarrow \exists y\, \exists z' (((0,y,z')\in \mathbf{R}^3)\land (y = z' = 0)))$$

---

Edit: In the comments, you write

What about $(\exists(0,y,z)\in\mathbb{R}^3)(y=z=0)$ when $z=42$? Isn't it the same as $(\exists(0,y,42)\in\mathbb{R}^3)(y=42=0)$? If not, how to use constants in my patterns if I have the names of the constants (like $z$)?

and

Such a simple and general interpretation IMO is questionable, as in $(\forall(\pi,\rho)\in\mathbb{R}^2)(\sin(\pi+\rho)+\sin(\pi)+\sin(\rho)=0)$. (Why some constants, like $1$ or $0$, can be used in patterns, but the others, like $\pi$ or $z$, cannot?)

Let me answer the second question first. It's important to distinguish between constants and variables. In a given context, variables are symbols whose values can range over a domain - they're the things the quantifiers are referring to (there exists a value of $x$ / for all values of $x$). On the other hand, constants have a fixed value. It's important that we're clear about which things are variables. If no other information is given, and in a context where it makes sense that we're talking about real numbers, I would expect $0$ and $1$ and $\pi$ to be constants, and $x$, $y$, $z$, $\rho$, etc. to be variables.

So when you write $\forall (\pi,\rho)\in \mathbb{R}^2$, I would expect that $\pi$ means the real number $\pi$ (whose value is fixed), while $\rho$ is a variable. Of course, it would be better to not use this quantifier at all, and instead write $\forall \rho\in \mathbb{R}$ (since for any $\rho\in \mathbb{R}$, $(\pi,\rho)\in \mathbb{R}^2$). Or if you mean to use $\pi$ as a variable, use another variable name so as not to conflict with the well-known constant $\pi$!

Of course, the cardinal rule is that if there's room for confusion, be more precise, e.g. explain which symbols are variables and which are constants, or don't use shorthand.

Now for the first question. If we're in a context where $z = 42$ is really a constant, see the previous discussion. But usually $z$ is used as a variable name, so I'll assume that going forward. If we're in a context where the variable $z$ has been previously bound to a value, the convention is that reusing $z$ in a new quantifier resets the value of $z$ within the scope of that quantifier. This is why $\forall z(\exists z \varphi(z))$ has the same meaning as $\forall z (\exists z' \varphi(z'))$.

I can see why you might like to allow a previously bound variable to be used in a pattern with its previously bound value, but I don't see how to make a coherent convention here which doesn't clash which the convention above about resetting variables when they're re-quantified. That is, when you see $\exists z\, \varphi(z)$, how do you know whether this is supposed to be a pattern-matching quantifier (with pattern $z$, in which case $z$ already has a value, and the quantifier does nothing) or a regular quantifier (in which case the value of $z$ gets reset)?

You could decide on a convention for yourself, but again, the cardinal rule is clarity. Why write things which are possibly ambiguous, when you could replace them with unambiguous notation? For example, instead of $$\forall z\, (\exists(0,y,z)\in X)\,\varphi(y,z)$$ why not just write $$\forall z\, \exists y\,(((0,y,z)\in X) \land \varphi(y,z))?$$