Combining Higher-Order Logic with Set Theory Formalizations

The Isabelle Higher-order Tarski–Grothendieck object logic includes in its foundations both higher-order logic and set theory, which allows importing the libraries of Isabelle/HOL and Isabelle/Mizar. The two libraries, however, define all the basic concepts independently, which means that the result...

Descripción completa

Detalles Bibliográficos
Autores principales: Kaliszyk, Cezary, Pąk, Karol
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Springer Netherlands 2023
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC10209288/
https://www.ncbi.nlm.nih.gov/pubmed/37252035
http://dx.doi.org/10.1007/s10817-023-09663-5
_version_ 1785046845486006272
author Kaliszyk, Cezary
Pąk, Karol
author_facet Kaliszyk, Cezary
Pąk, Karol
author_sort Kaliszyk, Cezary
collection PubMed
description The Isabelle Higher-order Tarski–Grothendieck object logic includes in its foundations both higher-order logic and set theory, which allows importing the libraries of Isabelle/HOL and Isabelle/Mizar. The two libraries, however, define all the basic concepts independently, which means that the results in the two are disconnected. In this paper, we align significant parts of these two libraries, by defining isomorphisms between their concepts, including the real numbers and algebraic structures. The isomorphisms allow us to transport theorems between the foundations and use the results from the libraries simultaneously.
format Online
Article
Text
id pubmed-10209288
institution National Center for Biotechnology Information
language English
publishDate 2023
publisher Springer Netherlands
record_format MEDLINE/PubMed
spelling pubmed-102092882023-05-26 Combining Higher-Order Logic with Set Theory Formalizations Kaliszyk, Cezary Pąk, Karol J Autom Reason Article The Isabelle Higher-order Tarski–Grothendieck object logic includes in its foundations both higher-order logic and set theory, which allows importing the libraries of Isabelle/HOL and Isabelle/Mizar. The two libraries, however, define all the basic concepts independently, which means that the results in the two are disconnected. In this paper, we align significant parts of these two libraries, by defining isomorphisms between their concepts, including the real numbers and algebraic structures. The isomorphisms allow us to transport theorems between the foundations and use the results from the libraries simultaneously. Springer Netherlands 2023-05-25 2023 /pmc/articles/PMC10209288/ /pubmed/37252035 http://dx.doi.org/10.1007/s10817-023-09663-5 Text en © The Author(s) 2023 https://creativecommons.org/licenses/by/4.0/Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/ (https://creativecommons.org/licenses/by/4.0/) .
spellingShingle Article
Kaliszyk, Cezary
Pąk, Karol
Combining Higher-Order Logic with Set Theory Formalizations
title Combining Higher-Order Logic with Set Theory Formalizations
title_full Combining Higher-Order Logic with Set Theory Formalizations
title_fullStr Combining Higher-Order Logic with Set Theory Formalizations
title_full_unstemmed Combining Higher-Order Logic with Set Theory Formalizations
title_short Combining Higher-Order Logic with Set Theory Formalizations
title_sort combining higher-order logic with set theory formalizations
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC10209288/
https://www.ncbi.nlm.nih.gov/pubmed/37252035
http://dx.doi.org/10.1007/s10817-023-09663-5
work_keys_str_mv AT kaliszykcezary combininghigherorderlogicwithsettheoryformalizations
AT pakkarol combininghigherorderlogicwithsettheoryformalizations

Ejemplares similares