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