A Proof of the De Zolt Postulate in Three-Dimensional Space

• Bruno Cuconato Pontifícia Universidade Católica do Rio de Janeiro / Fundação Getulio Vargas
• Edward Hermann Haeusler Pontifícia Universidade Católica do Rio de Janeiro https://orcid.org/0000-0002-4999-7476

Resumo

De Zolt’s postulate is a more mathematically precise restatement of Euclid’s geometric principle of “the whole is greater than the part” [8, Book I, Common Notion 5]. While the three-dimensional version of De Zolt’s postulate is not consistent with ZFC due to the Banach-Tarski paradox and related theorems, it is consistent with a proof-theoretically weaker theory. In this paper, we provide an implementation of such a weak type theory and a formal proof of De Zolt’s postulate in three dimensions in this theory.

Palavras-chave: De Zolt postulate, Formalization of Mathematics, Banach-Tarski paradox, Lean