Mechanized HOL Reasoning in Set Theory
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914721226031104 |
|---|---|
| author | Guilloud, Simon Gambhir, Sankalp Gilot, Andrea Kunčak, Viktor |
| author_facet | Guilloud, Simon Gambhir, Sankalp Gilot, Andrea Kunčak, Viktor |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_13403 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Mechanized HOL Reasoning in Set Theory Guilloud, Simon Gambhir, Sankalp Gilot, Andrea Kunčak, Viktor Logic in Computer Science I.2.3; F.4.1 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. |
| title | Mechanized HOL Reasoning in Set Theory |
| topic | Logic in Computer Science I.2.3; F.4.1 |
| url | https://arxiv.org/abs/2403.13403 |