Formal Proof of Banach-Tarski Paradox
DOI:
https://doi.org/10.6092/issn.1972-5787/6927Abstract
Banach-Tarski Paradox states that a ball in 3D space is equidecomposable with twice itself, i.e. we can break a ball into a finite number of pieces, and with these pieces, build two balls having the same size as the initial ball. This strange result is actually a Theorem which was proven in 1924 by Stefan Banach and Alfred Tarski using the Axiom of Choice.We present here a formal proof in Coq of this theorem.
References
Radu Diaconescu. Axiom of choice and complementation. Proceedings of the American Mathematical Society, 51(1):176–178, 1975.
The Coq Development Team. The Coq proof assistant reference manual. PiR2 Team, 2017. Version 8.6.
Stan Wagon. The Banach-Tarski Paradox. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.
Benjamin Werner. Sets in types, types in sets. In TACS, volume 1281 of Lecture Notes in Computer Science, pages 530–346. Springer, 1997.
Wikipedia. Banach-Tarski paradox — Wikipedia, the free encyclopedia, 2017. [Online; accessed 16-Apr-2017].
Wikipedia. Diaconescu’s theorem — Wikipedia, the free encyclopedia, 2017. [Online; accessed 20-Apr-2017].
Wikipedia. Hilbert’s paradox of the grand hotel — Wikipedia, the free encyclopedia, 2017. [Online; accessed 17-Apr-2017].
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2017 Daniel de Rauglaudre
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
