A tale of two set theories

DOI10.1007/978-3-030-23250-4_4zbMath1428.68348arXiv1907.08368OpenAlexW2954151392MaRDI QIDQ2287897

Chad Edward Brown, Karol Pąk

Publication date: 22 January 2020

Full work available at URL: https://arxiv.org/abs/1907.08368

zbMATH Keywords

theorem provingset theoryMizarformalized mathematicsproof checking

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Nonclassical and second-order set theories (03E70) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Generating custom set theories with non-set structured objects ⋮ Combining higher-order logic with set theory formalizations ⋮ Grothendieck universes

Uses Software

• Coq
• Isabelle/HOL
• Mizar

This page was built for publication: A tale of two set theories