Mechanized HOL Reasoning in Set Theory
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要