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 Bacon2 " (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 A and G, or specifc actors like Ewan McGregor3 and Cameron Diaz4 . To talk about all locations, or actors, we're forced to make huge formulas such as nhbr (Z, Y )∧¬nhbr (Z, A) ∧¬nhbr (Z, B) ∧ ... ∧¬nhbr (Z, X), just to express "there is a location which has only one neighbor".
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 ∀a : (coStarredWith (a, KevinBacon)). For " there is a location which has (at least) two neighbors ", we'll start with “there exists a location x ... “written ∃x :(...).
"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 "x has (at least) two neigh bors"? Well, we'll rephrase this as, " there exist distinct locations, y and z, which each of which is a neighbor of x ", written We need the condition ¬ (y = z) in = z) that formula to ensure that we have distinct locations. Compare to the algebraic equation x+y =4 in which one possible solution is x = y =2. Variables act the same way in both logic and algebra: different variables can happen to take on the same value.
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 quantifcation 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 specifcations, 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 y, such that you love y. " |
"N*Sync is the best band ever!" |
" For all bands x, N*Sync is better than band x (or, x = N ∗ Sync). " A quick listen can easily show this statement false. |
A casually subtle line from Something About Mary: "Every day is better than the next." |
" For all days x, x is better than next(x). " |
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 x, x loves my baby. For all persons y, if my baby loves y, then y is me. " If true, one can conclude the speaker is his own baby, and is narcissistic. |
"Every neighbor of x is unsafe." |
"For all locations y, if y is a neighbor of x, then y is unsafe." |
"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 x such that you've seen x, then for all episodes z, you've seen z." |
"Somebody loves everybody." |
"There exists some person y, such that for all persons x, y loves x." |
"There is someone for everybody." |
"For all persons x, there exists a person y, such that y is for x." |
"All's well that ends well." |
"For all events x, if x ends well then x is well." |
- 992 reads