Wednesday, January 09, 2008

Một chứng minh xây dựng tuyệt vời cho Bài toán Dừng

Chẹp chẹp chẹp! Hay thiệt là hay!

Mới có hơn một tháng mà khi mình quay lại thì thấy Wikipedia đã chuyển cách chứng minh bài toán dừng từ Phản chứng sang Lập luận Đường chéo! Chứng minh bằng phản chứng vốn không được "xây dựng" cho lắm, trong khi lập luận đường chéo (chính thống) thì "có vẻ" xây dựng hơn nhiều. "Có vẻ" ở đây là nhiều khi những điều kiện tiền đề của lập luận có ẩn chứa việc "phán" một cách không xây dựng, ví dụ "tiên đề lựa chọn".

Tìm kiếm trên mạng, mình toàn thấy những "chứng minh đường chéo... giả" mà thôi. Chẳng qua chỉ là những chứng minh bằng phản chứng rồi tưởng tượng ra một đường chéo nào đó chứ chẳng liên quan gì đến lập luận đường chéo gốc của Cantor (hoàn toàn không dùng phản chứng). Còn chứng minh trên Wikipedia, vốn được lấy từ chứng minh của peter_douglass trên sci.logic, thì chính xác là lập luận đường chéo theo kiểu của Cantor. Và hơn thế nữa, nó hoàn toàn xây dựng chứ không ẩn giấu những tiền đề không xây dựng như tiên đề lựa chọn. Nó tránh được tiên đề lựa chọn là vì tập hợp các chương trình dừng (tương ứng với hàm tính được) là một tập hợp liệt kê được, nên mỗi một phần tử trong bảng giá trị đều có thể được chỉ ra (xây dựng) bởi một chương trình (thuật toán) cụ thể.

No comments: