Result: Formal Proof of Banach-Tarski Paradox

Title:
Formal Proof of Banach-Tarski Paradox
Authors:
de Rauglaudre, Daniel
Contributors:
Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Design, study and implementation of languages for proofs and programs (PI.R2), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Centre Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
Source:
Journal of Formalized Reasoning. 10(1):37-49
Publisher Information:
CCSD; ASDD-AlmaDL, 2017.
Publication Year:
2017
Collection:
collection:UNIV-PARIS7
collection:CNRS
collection:INRIA
collection:INRIA-ROCQ
collection:LORIA2
collection:TESTALAIN1
collection:INRIA2
collection:USPC
collection:INRIA2017
collection:UNIV-PARIS
collection:UP-SCIENCES
collection:INRIAARTDOI
collection:IRIF
Subject Terms:
ACM: D.: Software, D.3: PROGRAMMING LANGUAGES, [MATH.MATH-LO]Mathematics [math], Logic [math.LO], [INFO.INFO-MS]Computer Science [cs], Mathematical Software [cs.MS]
Original Identifier:
HAL: hal-01673378
Document Type:
Journal article<br />Journal articles
Language:
English
ISSN:
1972-5787
Relation:
info:eu-repo/semantics/altIdentifier/doi/10.6092/issn.1972-5787/6927
DOI:
10.6092/issn.1972-5787/6927
Access URL:
https://hal.science/hal-01673378
https://hal.science/hal-01673378v1/document
https://hal.science/hal-01673378v1/file/6927-22125-1-PB.pdf
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.hal.01673378v1
Database:
HAL

Further Information

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.