Higher-Order Tarski Grothendieck as a Foundation for Formal Proof

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F19%3A00337659" target="_blank" >RIV/68407700:21730/19:00337659 - isvavai.cz</a>

Výsledek na webu

<a href="https://drops.dagstuhl.de/opus/volltexte/2019/11064/" target="_blank" >https://drops.dagstuhl.de/opus/volltexte/2019/11064/</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.ITP.2019.9" target="_blank" >10.4230/LIPIcs.ITP.2019.9</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Higher-Order Tarski Grothendieck as a Foundation for Formal Proof

Popis výsledku v původním jazyce

We formally introduce a foundation for computer verified proofs based on higher-order Tarski-Grothendieck set theory. We show that this theory has a model if a 2-inaccessible cardinal exists. This assumption is the same as the one needed for a model of plain Tarski-Grothendieck set theory. The foundation allows the co-existence of proofs based on two major competing foundations for formal proofs: higher-order logic and TG set theory. We align two co-existing Isabelle libraries, Isabelle/HOL and Isabelle/Mizar, in a single foundation in the Isabelle logical framework. We do this by defining isomorphisms between the basic concepts, including integers, functions, lists, and algebraic structures that preserve the important operations. With this we can transfer theorems proved in higher-order logic to TG set theory and vice versa. We practically show this by formally transferring Lagrange's four-square theorem, Fermat 3-4, and other theorems between the foundations in the Isabelle framework.

Název v anglickém jazyce

Higher-Order Tarski Grothendieck as a Foundation for Formal Proof

Popis výsledku anglicky

We formally introduce a foundation for computer verified proofs based on higher-order Tarski-Grothendieck set theory. We show that this theory has a model if a 2-inaccessible cardinal exists. This assumption is the same as the one needed for a model of plain Tarski-Grothendieck set theory. The foundation allows the co-existence of proofs based on two major competing foundations for formal proofs: higher-order logic and TG set theory. We align two co-existing Isabelle libraries, Isabelle/HOL and Isabelle/Mizar, in a single foundation in the Isabelle logical framework. We do this by defining isomorphisms between the basic concepts, including integers, functions, lists, and algebraic structures that preserve the important operations. With this we can transfer theorems proved in higher-order logic to TG set theory and vice versa. We practically show this by formally transferring Lagrange's four-square theorem, Fermat 3-4, and other theorems between the foundations in the Isabelle framework.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2019

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

10th International Conference on Interactive Theorem Proving (ITP 2019)

ISBN

978-3-95977-122-1

ISSN

—

e-ISSN

1868-8969

Počet stran výsledku

16

Strana od-do

—

Název nakladatele

Schloss Dagstuhl - Leibniz Center for Informatics

Místo vydání

Wadern

Místo konání akce

Portland

Datum konání akce

10. 9. 2019

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—