We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant for schematic first-order logic and its library based on axiomatic set theory. HOL proof steps are implemented as proof producing tactics in Lisa, and the types are interpreted as sets, with function (or arrow) types coinciding with set-theoretic function spaces. The embedded HOL proofs, as opposed to being a layer over the existing proofs, are interoperable with the existing library. This yields a form of soft type system supporting top-level polymorphism and ADTs over set theory, and offer tools to reason about functions in set theory.

翻译：我们提出了将高阶逻辑（HOL）与代数数据类型（ADT）机械化嵌入到带有ZFC公理的一阶逻辑中的方法。我们在面向模式化一阶逻辑的Lisa证明助理及其基于公理化集合论的库中实现了该系统。HOL证明步骤被实现为Lisa中可生成证明的策略，其中类型被解释为集合，函数（或箭头）类型与集合论函数空间保持一致。嵌入的HOL证明并非作为现有证明的覆盖层，而是能与现有库实现互操作。这种方式在集合论之上形成了一种支持顶级多态性与代数数据类型的软类型系统，并为集合论中的函数推理提供了工具。