Predicate variable

second-order variable

A variable whose values can be predicates (cf. Predicate). In the formal structure of an axiomatic system, predicate variables differ from individual variables (cf. Individual variable) by the fact that formulas may be substituted for them. Thus, in second-order predicate calculus, if in the axiom

$$ \forall x \phi ( x) \rightarrow \phi ( t), $$

$ x $ is a predicate variable for $ n $- place predicates, then any formula with $ n $ distinguished variables may be taken for $ t $. Here the result of substituting a formula $ t $ with $ n $ distinguished variables $ z _ {1} \dots z _ {n} $ for the predicate variable $ x $ in the atomic formula $ x ( y _ {1} \dots y _ {n} ) $, where $ y _ {1} \dots y _ {n} $ are individual constants, is the formula $ t ( y _ {1} | z _ {1} \dots y _ {n} | z _ {n} ) $ obtained from $ t $ by simultaneously replacing the free occurrences of $ z _ {1} \dots z _ {n} $ by $ y _ {1} \dots y _ {n} $, respectively.

References

[1]	A. Church, "Introduction to mathematical logic" , 1 , Princeton Univ. Press (1956)
[2]	G. Takeuti, "Proof theory" , North-Holland (1987)