高阶逻辑

高阶逻辑亦称"广义谓词逻辑"、"高阶谓词逻辑"。一阶逻辑的推广系统，谓词逻辑的重要组成部分。谓词逻辑有一阶逻辑和高阶逻辑之分。在一阶逻辑中，量词只能用于个体变元，取消这一限制条件，允许量词也可用于命题变元和谓词变元，由此构造起来的谓词逻辑就是高阶逻辑。公理化的高阶逻辑系统或高阶逻辑的自然推理系统又称为广义谓词演算或高阶谓词演算。高阶逻辑在数学中，高阶逻辑在很多方面有别于一阶逻辑。其一是变量类型出现在量化中;粗略的说，一阶逻辑中禁止量化谓词。允许这么做的系统请参见二阶逻辑。