In the notation of first order logic, lower case letters are used for variables. Conventionally, we use letters from the end of the alphabet (x, y, z) for variables and those from the start of the alphabet (a, b, c) for names, but formally any letter can be a name or a variable. The only difference is that such a symbol is a variable if it is bound by a quantifier, and a name if it is not. This principle is the same in Logic for Fun except that variables there may be strings of symbols, just like names.
- In the formula ALLx(Fx IMP Gx), the letter x is a variable, bound by the quantifier ALLx. It holds the place occupied by the name a in Fa IMP Ga.