*** Welcome to piglix ***

Predicate variable


In first-order logic, a predicate variable is a predicate letter which can stand for a relation (between terms) but which has not been specifically assigned any particular relation (or meaning). In first-order logic (FOL) they can be more properly called metalinguistic variables. In higher-order logic, predicate variables correspond to propositional variables which can stand for well-formed formulas of the same logic, and such variables can be quantified by means of (at least) second-order quantifiers.

In the metavariable sense, a predicate variable can be used to define an axiom schema. Predicate variables should be distinguished from predicate constants, which could be represented either with a different (exclusive) set of predicate letters, or by their own symbols which really do have their own specific meaning in their domain of discourse: e.g. .

If letters are used for predicate constants as well as for predicate variables, then there has to be a way of distinguishing between them. For example, letters W, X, Y, Z could be designated to represent predicate variables, whereas letters A, B, C,..., U, V could represent predicate "constants". If these letters are not enough, then numerical subscripts can be appended, e.g. X1, X2, X3,... However, if the predicate variables are not perceived (or defined) as belonging to the vocabulary of the predicate calculus, then they are predicate metavariables, whereas the rest of the predicate letters are just called "predicate letters". The metavariables are thus understood to be used to code for axiom schemata and theorem schemata (derived from the axiom schemata). Whether the "predicate letters" are constants or variables is a subtle point: they are not constants in the same sense that are predicate constants, or that are numerical constants.


...
Wikipedia

...