Usage
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 actually belonging to the vocabulary of the predicate calculus, then they are actually predicate metavariables, whereas the rest of the predicate letters are just called "predicate letters". The metavariables are thus understood to be used to actually code for axiom schemata and theorem schemata (derived from the axiom schemata). Whether the "predicate letters" are actually constants or variables is a subtle point: they are not constants in the same sense that are predicate constants, or that are numerical constants.
Another option is to use Greek lower-case letters to represent such metavariable predicates. Then, such letters could be used to represent entire well-formed formulae of Pred.Calc.: any free variable terms of the wff could be incorporated as terms of the Greek-letter predicate. This is the first step towards creating a higher-order logic.
If "predicate variables" are only allowed to be bound to predicate letters of zero arity (which have no arguments), where such letters actually represent propositions, then such variables are actually propositional variables, and any predicate logic which allows second-order quantifiers to be used to bind such propositional variables is a second-order predicate calculus, or second-order logic.
If predicate variables are also allowed to be bound to predicate letters which are unary or have higher arity, and when such letters represent propositional functions, such that the domain of the arguments is mapped to a range of different propositions, and when such variables can be bound by quantifiers to such sets of propositions, then the result is a higher-order predicate calculus, or higher-order logic.
Read more about this topic: Predicate Variable
Famous quotes containing the word usage:
“...Often the accurate answer to a usage question begins, “It depends.” And what it depends on most often is where you are, who you are, who your listeners or readers are, and what your purpose in speaking or writing is.”
—Kenneth G. Wilson (b. 1923)
“I am using it [the word ‘perceive’] here in such a way that to say of an object that it is perceived does not entail saying that it exists in any sense at all. And this is a perfectly correct and familiar usage of the word.”
—A.J. (Alfred Jules)
“Girls who put out are tramps. Girls who don’t are ladies. This is, however, a rather archaic usage of the word. Should one of you boys happen upon a girl who doesn’t put out, do not jump to the conclusion that you have found a lady. What you have probably found is a lesbian.”
—Fran Lebowitz (b. 1951)