一句话：为 Gordon 的 HOL 引入 Henkin 式一般模型，并证明一种增强演绎系统相对这些模型既可靠又完备。
Mike Gordon 的高阶逻辑（HOL）是交互式定理证明最重要的逻辑基础之一。其标准语义由 Andrew Pitts 给出，采用向下封闭的集合论宇宙，并通过宇宙上的全局选择函数解释 HOL 的 Hilbert 选择算子。本文填补 HOL 元理论中的一处空白：提出与标准模型相对应的自然 Henkin 式一般模型，并发现一种 HOL 演绎系统的增强形式，证明该演绎相对这些一般模型既可靠又完备。这一结果厘清了 HOL 标准语义与一般模型之间的关系，为基于 HOL 的证明助手提供了更完整的元理论支撑。
Mike Gordon’s Higher-Order Logic (HOL) is one of the most important logical foundations for interactive theorem proving. The standard semantics of HOL, due to Andrew Pitts, employs a downward closed universe of sets, and interprets HOL’s Hilbert choice operator via a global choice function on the universe. In this paper we fill a gap in the meta-theory of HOL: We provide a natural Henkin-style notion of general model corresponding to the standard models, and discover an enrichment of HOL deduction that we prove to be sound and complete w.r.t. these general models.
DOI 原文 ·
@inproceedings{paperbot8661,
title = {Completing Gordon’s Higher-Order Logic},
author = {Andrei Popescu},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00008}
}