A new notation for building sets?

We write \forall x\in\mathbb{R}\ldotp x^2 \ge 0 to express that the square of any real number is non-negative. We write \exists x\in\mathbb{Z} \ldotp x \ge 0 \land x \le 0 to express that there exists an integer that is both non-negative and non-positive. We write \lambda x:\mathsf{int} \ldotp x+1 to denote the successor function. In a less well known example from nominal logic, we write {\sf N}x\ldotp\phi  to mean, roughly, that we should pick any name for x that isn’t the same as the name of any free variable already occurring in \phi.

Observe that all of these functions work by defining a variable to stand for something, and then referring to that something in the body of the function.

For the \lambda-calculus example, it’s helpful to refer to an arbitrary input when defining the output of the function. In the existential case, we refer to an arbitrary element of the set over which we’re quantifying; this scheme is particularly helpful here because we can write x twice in the body and know that we’re talking about the same thing both times.

Sets are often built in a similar way. For instance, we write \{x\in\mathbb{Z}\mid x<0\} to denote the set of negative integers. The similarity is clear: we define a variable x to stand for an arbitrary integer, and then refer to that variable in the body, where we constrain it. So why is the syntax so different? Why the vertical line in place of the dot? Why the curly braces in place of a single symbol?

Consider a new set builder notation that is more compatible with the functions presented above. We might propose to have the above set defined like so:

{\sf S}x\in\mathbb{Z} \ldotp x<0

Is there a good reason why sets are not defined like this? I believe there is. Whereas \lambda x \ldotp \lambda y \ldotp x is perfectly sensible, there is no meaning for {\sf S}x \ldotp {\sf S} y\ldotp x>y. That the proposed syntax admits such a construction is a crucial weakness. Note that the original notation does not condone building a set in this way.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s