A Proof of the De Zolt Postulate in Three-Dimensional Space - Cuconato, Bruno; Haeusler, Edward Hermann (Anais do Simpósio Brasileiro de Métodos Formais (SBMF); 2025: Anais do XXVIII Simpósio Brasileiro de Métodos Formais, 2025)
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.