Logical notation: QuantifiersMore Advanced Topics

Often we need to impose a constraint not just on a particular individual like Tom but on every object in some domain. For this purpose we use the universal quantifier. By substituting a variable x for the name and binding it with ALL we may express the constraint that everyone is happy:
ALL x happy(x).
The universal quantifier frequently works together with the implication connective to impose a constraint on those individuals (if any) who satisfy a given condition. To say that all people loved by Tom are happy, for example, we may write
ALL x (Tom loves x IMP happy(x)).
More complex conditions are written in the same way. For instance:
ALL x ((Tom loves x AND x loves Tom) IMP happy(x)).
constrains any (and every) person in a mutually loving relationship with Tom to be happy, but imposes no constraint on the rest of us.
The universal quantifier is also used with the biconditional (equivalance) connective to state the conditions under which something holds. Thus we can say that happiness is being a postman who knows Tom:
ALL x (happy(x) IFF (x knows Tom AND postman(x)))
In effect, this allows us to define some properties in terms of others. For instance, to specify exactly who the postmen are, we can list them:
ALL x (postman(x) IFF (x = Tom OR x = Dick OR x = Harry))

The existential quantifier SOME occurs less often in constraints, but has its uses nonetheless, when we need to say there is something satisfying a given description. Consider:

Tom loves somebody
SOME x (Tom loves x).
Everybody loves somebody
ALL x SOME y (x loves y).
Everyone who knows Tom knows at least one person who knows Mary
ALL x (x knows Tom IMP SOME y (x knows y AND y knows Mary)).

The logical symbols   ∀   and   ∃   are abbreviations for the words ALL and SOME respectively, so they may be used to bind variables as in the usual notation for first order logic. Each quantifier ranges over just one of the sorts; which one is determined by looking at the type of the bound variable, which is deduced from its position in constraints.