Suppose we want to express a statement like
“there is a location which has two neighbors”
(which is true, at least for the domain of WaterWorld board
locations), or
“
all actors have co-starred with
Kevin Bacon
”
(which isn't true, at least for the domain of all Hollywood actors).
As it stands, we can formulate these only awkwardly,
by talking about
*specific* (constant) locations like

We'll redress this by introducing two quantifiers,
∃ (“there exists”) and
∀ (“for all”).
For example, “all actors have co-starred with Kevin Bacon”
will be written

“For all” is really just an abbreviation for a large conjunction, while “exists” is a disjunction (it could also be called “for some”, though it's not). How large a conjunction/disjunction? As big as your domain, which actually could be very small, or it could be infinitely large. Even aside from the fact that we can't write down an infinitely large conjunction or disjunction, quantifiers let us form the conjunction without having to select a domain in advance.

To continue with our WaterWorld example,
how can we express the concept
“

We use quantifiers all the time in natural language. Consider the following examples, where we provide a natural English wording together with an equivalent phrasing that makes the quantification more explicit. We'll take the translations with a grain of salt, since sometimes people can disagree on the exact details of the intended English meaning. Such ambiguity can sometimes be a rich source of creativity, but it's not tolerable when documenting safety properties of software. While some of these examples are a bit frivolous, in general quantifiers let us precisely capture more interesting concepts in type-checking, data structures such as trees and hash tables, circuit specifications, etc.

Natural English | Formalized English |
---|---|

“ If you don't love yourself, you can't love anybody else. ” |
“
If you don't love you, there does not exists a person |

“N*Sync is the best band ever!” |
“
For all bands |

A casually subtle line from Something About Mary: “Every day is better than the next.” |
“
For all days |

A buggy line from a song (Everybody Loves My Baby, Jack Palmer and Spencer Willson, 1924): “Everybody loves my baby; My baby don't love [anybody] but me.” |
“
For all persons |

“Every neighbor of x is unsafe.” | “For all locations |

“There is a safe location that is a neighbor of x, if num(x)<3.” | “If num(x)<3, then there exists a location y, such that y is safe, and y is a neighbor of x.” |

“If you've seen one episode, you've seen 'em all.” | “If there exists one episode |

“Somebody loves everybody.” | “There exists some person |

“There is someone for everybody.” | “For all persons |

“All's well that ends well.” |
“For all events |

**Warning: The Ambiguous “Any”**

The ambiguous “any”:
I was playing a game with some friends, and we came across the rule:
“
If you have more cards than any other player,
then discard a card.
”
Does this mean
“than *all* other players”, or
“than *some* other player”?
Our group's opinion was divided (incl. across many native English speakers).

In our class terms, it's not always clear
whether “any” means for-all,
or for-some (there-exists).
Or maybe more accurately,
in the phrase “for any

#### Aside:

In your proof-writing (and your English writing, and your informal writing), think about replacing “any” with either “every” or with “some”, to make your meaning clear.