谓词变量 在一阶逻辑中谓词变量是表示在项之间的一个关系的谓词字母这个关系还没有被特殊的指派任何特定的关系或意义内涵在一阶逻辑FOL中它们可以被更合适的到叫做元变量在高阶逻辑中谓词变量对应于命题变量它可以表示同一个逻辑中的合式公式而这种变量可以被通过至少二阶量词的方式来量化 在元变量意义上谓词变量可以用来定义公理模式谓词变量应当区别于谓词常量它可以被表示为要么通过不同的排他的谓词字母集合要么通过在其论域中实际上有自己特殊的意义的符号 比如                      displaystyle  in  leq   subset   如果字母用于谓词常量又用于谓词变量则必须有区分它们的方式例如字母 W X Y Z 可以被指定表示谓词变量而字母 A B C U V 可以表示谓词常量如果这些字母不够则可以添加数字下标比如 X X X 但是如果谓词变量被认知或定义为实际上属于谓词演算的词汇表则它们实际上是谓词元变量而余下的谓词字母就叫做谓词字母元变量因此被理解为用来实际上编码公理模式和定理模式推导自公理模式谓词字母实际上是常量还是变量是个微妙的要点                   displaystyle  in  leq   subset  是谓词常量而                 π    e   displaystyle    sqrt  pi  e  是数值常量它们不是同样意义的常量 另一种选择是使用小写希腊字母来表示这种元变量谓词那么这种字母可以用来表示谓词演算的全部合式公式 wff 的任何自由变量项都可以被合成为希腊字母谓词的项这是建立高阶逻辑的第一步 如果只允许谓词变量被约束到零元数的谓词字母没有参数这种字母实际上表示命题则这种变量实际上是命题变量允许用二阶量词约束这种命题变量的任何谓词逻辑都是二阶谓词演算或二阶逻辑 如果还允许谓词变量被约束到是一元或更多元的谓词字母这时这种字母表示命题函数使得参数的定义域被映射到不同命题的值域这时这种变量可以被量词约束到这种命题的集合那么结果就是高阶谓词演算或高阶逻辑