Banach-Tarski paradoksuyla ilgili bulabileceğiniz en kapsamlı kaynak sanırım Stan Wagon'ın "The Banach-Tarski Paradox" isimli kitabıdır. Kitapta bu teoremin ve çeşitli varyasyonlarının kanıtını tüm detaylarıyla bulabilirsiniz.
Seçim aksiyomuyla olan ilişkisi şu. Kanıtın bir noktasında bir kümeler ailesinin boş olmayan her elemanından bir eleman seçiyoruz ve bunu yapabilmek için seçim beliti gerekiyor. Peki bu teoremi kanıtlamak için seçim belitini kesinlikle kullanmamız gerekli mi, yoksa bu teoremi sadece ZF aksiyomları ile kanıtlamak mümkün olabilir mi? Belki de ZF içerisinde bizim henüz bulamadığımız başka bir kanıt vardır?
Bu soruların cevabı ne yazık ki hayır. Banach- Tarski paradoksundaki bazı parçalar eli mahkum Lebesgue ölçülemez olmak zorundadır (aksi halde 1=2 olduğunu gösterip çelişki kanıtlardık). Yani Banach-Tarski paradoksunu kanıtlayabiliyorsanız ölçülemez bir kümenin olduğunu da kanıtlayabiliyorsunuz demektir.
Öte yandan Robert Solovay göstermiştir ki eğer ZFC+"Erişilemez bir kardinal vardır" teorisi tutarlı ise ZF+DC+"Gerçel sayıların her alt kümesi ölçülebilirdir" teorisi de tutarlıdır. Dolayısıyla, Banach-Tarksi paradoksu ZF+DC teorisi içerisinde kanıtlanamaz (eğer ZFC+"Erişilemez bir kardinal vardır" teorisi tutarlı ise). Makalenin kendisine erişmek için buraya bakabilirsiniz.
Referans verdiğim kitabın 13. bölümüne bakarsanız ZF+DC'nin Banach-Tarski paradoksunu kanıtlamaya yeterli olmadığını sadece ZF'nin tutarlı olduğu varsayımı altında da kanıtlayabileceğinizi görebilirsiniz.