View source for Predicate variable

''second-order variable''

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

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p0743801.png" /></td> </tr></table>

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p0743802.png" /> is a predicate variable for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p0743803.png" />-place predicates, then any formula with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p0743804.png" /> distinguished variables may be taken for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p0743805.png" />. Here the result of substituting a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p0743806.png" /> with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p0743807.png" /> distinguished variables <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p0743808.png" /> for the predicate variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p0743809.png" /> in the atomic formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p07438010.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p07438011.png" /> are individual constants, is the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p07438012.png" /> obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p07438013.png" /> by simultaneously replacing the free occurrences of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p07438014.png" /> by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074380/p07438015.png" />, respectively.

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Church,   "Introduction to mathematical logic" , '''1''' , Princeton Univ. Press  (1956)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  G. Takeuti,   "Proof theory" , North-Holland  (1987)</TD></TR></table>