 Second-order logic has several kinds of variables. It has individual variables denoted by lower case letters \(x, y, z, \ldots\) possibly with subscripts. It has property and relation variables denoted by upper case letters \(X,Y,Z,\ldots\) possibly with subscripts. Finally, it has function variables denoted by upper case letters \(F, G, H, \ldots\) possibly with subscripts. Sometimes function variables are omitted as, after all, functions are special kinds of relations. Each relation and function variable has an arity, which is a positive natural number.