2026-07-22T04:53:59Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20746 2024-11-27T23:18:07Z ddc:004 open_access

Mechanized HOL Reasoning in Set Theory Guilloud, Simon Gambhir, Sankalp Gilot, Andrea Kunčak, Viktor Proof assistant First Order Logic Set Theory Higher Order Logic We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADTs) into first-order logic with ZFC axioms. Our approach interprets types as sets, with function (arrow) types coinciding with set-theoretic function spaces. We assume traditional FOL syntax without notation for term-level binders. To embed λ-terms, we define a notion of context, defining the closure of all abstractions occuring inside a term. We implement the embedding in the Lisa proof assistant for schematic first-order logic and its library based on axiomatic set theory (presented at ITP 2023). We show how to implement type checking and the proof steps of HOL Light as proof-producing tactics in Lisa. The embedded HOL theorems and proofs are interoperable with the existing Lisa library. This yields a form of soft type system supporting top-level polymorphism and ADTs within set theory. The approach offers tools for Lisa users to carry HOL-style proofs within set theory. It also enables the import of HOL Light theorem statements into Lisa, as well as the replay of small HOL Light kernel proofs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Simon Guilloud and Sankalp Gambhir and Andrea Gilot and Viktor Kunčak 2024 Is Part Of LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2024.18 urn:nbn:de:0030-drops-207464 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.18 eng https://creativecommons.org/licenses/by/4.0/legalcode