Chứng minh hoàn chỉnh, được xác minh về mặt cơ học của Định lý Banach-Tarski trong ACL2(R)
A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R).
Bài nghiên cứu này trình bày một chứng minh chính thức về định lý Banach-Tarski trong ACL2(r). Định lý Banach-Tarski phát biểu rằng một quả cầu đơn vị có thể được phân chia thành số lượng hữu hạn các mảnh có thể quay để tạo thành hai bản sao giống hệt nhau của quả cầu. Chúng tôi đã chính thức hóa các phép quay 3D và tạo ra một nhóm phép quay 3D tự do có bậc 2. Trong công việc trước đây, tính không thể đếm được của các số thực đã được chứng minh trong ACL2(r) và một phiên bản của Tiên đề Lựa chọn có thể chọn một phần tử đại diện một cách nhất quán từ một lớp tương đương đã được giới thiệu trong ACL2 phiên bản 3.1. Sử dụng nhóm phép quay tự do và công việc trước đây này, các tác giả cho thấy hình cầu đơn vị có thể được phân tích thành hai tập hợp, mỗi tập hợp tương đương với hình cầu ban đầu. Sau đó, các tác giả cho thấy quả cầu đơn vị ngoại trừ gốc có thể được phân tích thành hai tập hợp, mỗi tập hợp tương đương với quả cầu ban đầu bằng cách ánh xạ các điểm của quả cầu đơn vị tới các điểm trên hình cầu. Cuối cùng, chúng tôi xử lý gốc bằng cách quay quả cầu đơn vị quanh một trục sao cho gốc nằm bên trong hình cầu. Có vẻ nghịch lý, kết quả cấu trúc lại cho ra hai bản sao của quả cầu đơn vị.