高阶逻辑中的亨金语义 我们先从一阶逻辑的局限性开始。一阶逻辑允许我们对个体进行量化（如 ∀x, ∃y），但其表达能力有限。例如，我们无法将“任意两个元素都有唯一的上确界”这一性质定义为一个单独的公式，因为它要求量化“所有子集”或“所有性质”，这超出了个体域的范围。高阶逻辑通过允许对集合、函数甚至更高阶的对象进行量化，克服了这一限制。 接下来，我们面临高阶逻辑的语义问题。在一阶逻辑中，模型为每个符号指定了明确的解释：个体常量对应论域中的元素，关系符号对应论域上的关系。然而，在高阶逻辑中，当我们引入二阶变量（如 X，代表个体域的子集）时，一个核心问题是：这些二阶变量的取值范围应该是什么？最直观的想法是“全语义”，即二阶变量取遍个体域的所有可能子集（即幂集）。但库尔特·哥德尔的不完备性定理表明，基于全语义的二阶逻辑没有完备的演绎系统。 为了获得一个可公理化的、完备的系统，逻辑学家莱昂·亨金提出了一种新的语义解释。亨金语义的核心思想是：将高阶变量的取值范围与个体域解耦。在一个亨金模型中，我们不仅需要指定一个个体域 D，还需要为每一阶的类型指定一个非空的“论域”。例如，对于个体类型，论域就是 D；对于（个体到个体的）函数类型，论域是 D^D 的某个非空子集；对于关系类型（即个体集合），论域是 P(D) 的某个非空子集。这些论域共同构成了一个“框架”。 然后，我们来看赋值函数。在亨金模型中，一个赋值不仅需要为个体变量指定个体域中的值，还需要为每个高阶变量指定其对应论域中的一个具体对象。例如，对一个二阶关系变量 X，赋值函数会从为关系类型指定的论域（即 D 的某个子集族）中选取一个集合作为其解释。只有当赋值函数满足模型中的公式时，该公式在模型中才为真。 最后，我们讨论亨金语义的关键性质。如果对每个类型的论域都取“所有可能”的对象（如关系类型取整个幂集 P(D)），那么我们就得到了前面提到的“全语义”，这是一种特殊的亨金模型。但亨金语义允许更一般的“广义语义”或“一般模型”，其中高阶论域可以是相应的全集的任意非空子集。正是这种灵活性使得亨金能够证明：带有标准公理系统的高阶逻辑，在亨金语义下是可靠且完备的。这意味着一个公式在所有的亨金模型中为真，当且仅当它可以在该逻辑系统中被证明。这解决了全语义下的不完备性问题，为高阶逻辑的形式化研究奠定了坚实的基础。