# Mechanized HOL Reasoning in Set Theory

arXiv: https://arxiv.org/abs/2403.13403 · HTML: https://mlsanity.com/paper/2403.13403/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Mar 2024.

## Built on by (most cited first, 2 of 2)

- [Faithful Logic Embeddings in HOL -- Deep and Shallow](https://mlsanity.com/paper/2502.19311/) (2025)
- [Reformalization of the Jordan Curve Theorem](https://mlsanity.com/paper/2607.01734/) (2026)

## Abstract (arXiv)

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.