Định lý bất toàn thứ nhất của Kurt Gödel, công bố năm 1931, nói rằng mọi hệ tiên đề nhất quán, đủ mạnh để diễn đạt số học thông thường và có thể liệt kê được bằng một quy trình máy móc, đều chứa những mệnh đề không chứng minh được và cũng không bác bỏ được trong chính hệ đó. Định lý thứ hai nói rằng một hệ như vậy không thể tự chứng minh mình nhất quán.
Năm năm sau, Alan Turing, và độc lập với ông là Alonzo Church, chỉ ra một giới hạn tương tự cho tính toán: không có thuật toán nào quyết định được mọi mệnh đề toán học là đúng hay sai, và không có chương trình nào luôn đoán đúng một chương trình bất kỳ có dừng hay không. Từ đó ra đời khái niệm máy Turing, nền lý thuyết của mọi máy tính. Hai kết quả này hay bị trích sai; bài này giải thích chúng nói gì, không nói gì.
Chương trình Hilbert: giấc mơ tự động hoá chân lý
Đầu thế kỷ 20, toán học vừa trải qua một cơn chấn động: lý thuyết tập hợp ngây thơ dẫn tới nghịch lý, nổi tiếng nhất là nghịch lý Russell về "tập hợp của mọi tập hợp không chứa chính nó". Để đặt toán học lên nền vững chắc, David Hilbert đề ra một chương trình trong thập niên 1920: hình thức hoá toàn bộ toán học thành một hệ tiên đề với các quy tắc suy luận rõ ràng, rồi chứng minh, bằng những phương pháp hữu hạn đáng tin, rằng hệ đó nhất quán và đầy đủ.
Nhất quán nghĩa là không bao giờ chứng minh được cả một mệnh đề lẫn phủ định của nó. Đầy đủ nghĩa là mọi mệnh đề phát biểu được trong hệ thì hoặc chứng minh được, hoặc bác bỏ được. Hilbert và Wilhelm Ackermann còn nêu bài toán quyết định, tiếng Đức là Entscheidungsproblem: tìm một quy trình máy móc nhận vào một mệnh đề logic và trả lời nó có đúng trong mọi trường hợp không.
Nếu chương trình thành công, toán học về nguyên tắc sẽ trở thành một cỗ máy: mọi câu hỏi có câu trả lời, và câu trả lời tìm được bằng thủ tục. Gödel và Turing cho thấy giấc mơ đó không thực hiện được, nhưng con đường họ đi để chứng minh điều đó lại mở ra logic toán học hiện đại và khoa học máy tính.
Gödel đã chứng minh điều gì, theo cách dễ hình dung
Mã hoá mệnh đề thành số. Gödel gán cho mỗi ký hiệu, mỗi công thức, mỗi chứng minh một số tự nhiên, ngày nay gọi là số Gödel. Nhờ đó, các phát biểu về chứng minh, như "dãy công thức này là một chứng minh của công thức kia", trở thành các phát biểu về tính chất của số, mà số học diễn đạt được.
Dựng một câu nói về chính nó. Dùng kỹ thuật này, Gödel dựng được một mệnh đề G mà nội dung, khi dịch ra, là "mệnh đề G không chứng minh được trong hệ này". Nó gợi nhớ nghịch lý kẻ nói dối, nhưng thay "sai" bằng "không chứng minh được", và chính sự thay đổi đó tránh được nghịch lý.
Suy ra. Nếu hệ chứng minh được G, thì hệ chứng minh một điều sai, trái với giả thiết hệ nhất quán. Vậy G không chứng minh được, nghĩa là điều G nói là đúng. Ta có một mệnh đề đúng mà hệ không chứng minh được. Để kết luận hệ cũng không bác bỏ được G, Gödel cần một giả thiết mạnh hơn nhất quán một chút, và năm 1936 Barkley Rosser cải tiến để chỉ cần tính nhất quán.
Định lý thứ hai. Lập luận trên có thể hình thức hoá ngay bên trong hệ. Nếu hệ chứng minh được mình nhất quán, nó sẽ chứng minh được G, điều đã thấy là không thể. Vậy hệ không tự chứng minh được tính nhất quán của mình.
Thêm tiên đề có giải quyết được không? Có thể thêm G làm tiên đề mới, nhưng hệ mới lại có câu G phẩy của riêng nó. Hiện tượng bất toàn không xoá được bằng cách vá thêm, miễn là hệ vẫn liệt kê được bằng máy móc và đủ mạnh cho số học.
Turing năm 1936: định nghĩa "tính được" và bài toán dừng
Để trả lời bài toán quyết định của Hilbert, cần nói chính xác "quy trình máy móc" là gì. Trong bài báo năm 1936 về các số tính được và ứng dụng cho bài toán quyết định, Turing mô tả một cỗ máy tưởng tượng: một băng giấy dài vô hạn chia ô, một đầu đọc ghi mỗi lúc xem một ô, và một bảng quy tắc hữu hạn cho biết với trạng thái hiện tại và ký hiệu đang đọc thì ghi gì, dịch trái hay phải, chuyển sang trạng thái nào. Turing lập luận rằng bất kỳ phép tính nào một người làm theo quy tắc, với giấy bút đủ nhiều, đều mô phỏng được bằng cỗ máy như vậy.
Ông còn mô tả một máy vạn năng: một máy Turing duy nhất nhận vào mô tả của bất kỳ máy nào khác cùng dữ liệu, rồi mô phỏng nó. Đây là ý tưởng lý thuyết của máy tính lưu chương trình: phần cứng cố định, chương trình chỉ là dữ liệu.
Rồi ông chứng minh không có máy nào giải được bài toán dừng. Giả sử có một chương trình D nhận vào một chương trình P và trả lời P có dừng hay không. Dựng chương trình X làm ngược lại: nếu D nói P dừng khi chạy trên chính mã của nó thì X chạy mãi, nếu D nói không dừng thì X dừng. Hỏi X chạy trên chính nó thì sao: mọi câu trả lời của D đều sai. Vậy D không tồn tại. Từ đây suy ra bài toán quyết định của Hilbert không có lời giải. Alonzo Church đạt kết luận tương tự gần như cùng lúc bằng một hình thức khác, và người ta chứng minh được hai cách định nghĩa "tính được" là tương đương.
Gödel và Turing nói gì, không nói gì
Hai định lý này nằm trong số những kết quả bị trích dẫn sai nhiều nhất ngoài giới toán học. Bảng dưới gom các cách dùng sai hay gặp.
| Cách nói sai | Điều đúng |
|---|---|
| Gödel chứng minh toán học không đáng tin | Gödel chỉ ra giới hạn của từng hệ tiên đề hình thức; các định lý đã chứng minh vẫn đúng |
| Có những chân lý toán học mà con người không bao giờ biết | Định lý nói về một hệ cụ thể; mệnh đề không chứng minh được trong hệ này có thể chứng minh được trong hệ mạnh hơn |
| Định lý bất toàn áp dụng cho mọi hệ thống, kể cả luật pháp, xã hội | Chỉ áp dụng cho hệ hình thức đủ mạnh để chứa số học, có quy tắc suy luận chính xác |
| Bài toán dừng nghĩa là không kiểm được chương trình nào | Kiểm được rất nhiều chương trình cụ thể; chỉ không có một thuật toán chung đúng cho mọi chương trình |
| Gödel và Turing chứng minh máy tính không bao giờ thông minh như người | Đây là tranh luận triết học còn mở; các định lý không trực tiếp chứng minh điều này |
Một hệ quả thực tế của dòng ý tưởng này là định lý Rice năm 1953: mọi tính chất không tầm thường về hành vi của chương trình đều không quyết định được bằng một thuật toán chung. Đó là lý do mọi công cụ phân tích mã nguồn đều phải chấp nhận hoặc báo động nhầm, hoặc bỏ sót, hoặc chỉ làm việc với một lớp chương trình giới hạn.
Turing sau năm 1936 và di sản
Phần đời còn lại của Turing ngắn nhưng dày đặc, và ở mỗi mảng ông đều để lại dấu ấn lâu dài.
- Trong Thế chiến thứ hai, Turing làm việc tại Bletchley Park ở Anh, đóng góp lớn vào việc giải mã hệ thống mật mã Enigma của Đức. Phần lớn công việc này được giữ bí mật trong nhiều thập niên.
- Sau chiến tranh, ông tham gia thiết kế những máy tính điện tử đầu tiên ở Anh, đưa ý tưởng máy vạn năng vào phần cứng thật.
- Năm 1950, ông viết bài báo về máy tính và trí thông minh, đề xuất "trò chơi bắt chước", sau này gọi là phép thử Turing, như một cách thay câu hỏi mơ hồ "máy có nghĩ không" bằng một câu hỏi có thể kiểm được.
- Ông còn nghiên cứu sự hình thành hoa văn trong sinh học, như sọc và đốm trên da động vật, bằng phương trình phản ứng – khuếch tán; các ý tưởng này vẫn được dùng.
- Từ năm 1966, giải thưởng cao nhất của ngành khoa học máy tính mang tên ông.
- Gödel làm việc phần lớn sự nghiệp còn lại tại Viện Nghiên cứu Cao cấp Princeton, chứng minh thêm rằng giả thuyết continuum không bác bỏ được trong hệ tiên đề chuẩn của lý thuyết tập hợp.
Turing mất năm 1954 khi mới 41 tuổi. Những năm cuối đời ông bị kết án theo luật thời đó vì đồng tính; năm 2013 ông được ân xá. Khi kể về Turing, bạn nên dựa vào các tiểu sử nghiêm túc, vì phim ảnh đã thêm nhiều chi tiết hư cấu về công việc giải mã.
Gödel, Turing và AI hôm nay: dùng đúng mức
Người học AI thường gặp lập luận "định lý Gödel chứng minh AI không bao giờ bằng người" hoặc ngược lại "AI sẽ giải mọi bài toán". Cả hai đều vượt quá những gì định lý nói. Một cách suy nghĩ có kỷ luật:
- Nhớ rằng mọi chương trình AI chạy trên máy tính thông thường đều là một máy Turing về mặt lý thuyết. Nó không vượt được bài toán dừng, và không có hệ chứng minh tự động nào đầy đủ cho mọi mệnh đề số học.
- Phân biệt giới hạn lý thuyết với giới hạn thực tế. Phần lớn bài toán mà AI giúp làm trong học tập và công việc nằm rất xa vùng bất toàn; khó khăn thật thường là thiếu dữ liệu, sai sót suy luận hoặc thiếu kiểm chứng.
- Khi chatbot giải thích định lý bất toàn, yêu cầu nó nêu ba điều kiện của định lý: nhất quán, đủ mạnh cho số học, liệt kê được. Một giải thích bỏ qua điều kiện nào là đang đơn giản hoá quá mức.
- Dùng AI để luyện: nhờ nó đưa ra mười câu khẳng định về Gödel và Turing, có đúng có sai, rồi tự phân loại và giải thích. Câu lệnh mẫu: "Viết mười khẳng định về định lý bất toàn, trộn đúng và sai, không đánh dấu đáp án."
- Đọc ít nhất một văn bản gốc ở dạng dịch có chú giải, như bài báo năm 1936 của Turing. Phần đầu bài báo đọc được với kiến thức đại học năm nhất.
Câu hỏi thường gặp
Có ví dụ mệnh đề "tự nhiên" nào không chứng minh được trong số học thông thường không?
Có. Định lý Goodstein về một loại dãy số tăng rồi cuối cùng giảm về 0, và một dạng mạnh của định lý Ramsey do Paris và Harrington nêu năm 1977, đều đúng nhưng không chứng minh được trong số học Peano. Chúng chứng minh được trong các hệ mạnh hơn. Đây là những ví dụ cho thấy bất toàn không chỉ là câu tự quy chiếu nhân tạo.
Luận đề Church – Turing là định lý hay giả thuyết?
Đó là một luận đề, không phải định lý, vì nó nối một khái niệm trực giác là "tính được bằng quy trình máy móc" với một định nghĩa toán học chính xác. Không chứng minh được bằng toán học, nhưng mọi mô hình tính toán hợp lý được đề xuất đều hoá ra tương đương, nên nó được chấp nhận rộng rãi.
Máy tính lượng tử có vượt qua được bài toán dừng không?
Không. Máy tính lượng tử có thể giải một số bài toán nhanh hơn nhiều, nhưng những gì nó tính được thì máy Turing thông thường cũng tính được, chỉ chậm hơn. Ranh giới giữa tính được và không tính được không thay đổi.
Gödel có quan hệ gì với Einstein?
Hai người là bạn thân ở Viện Nghiên cứu Cao cấp Princeton và thường đi bộ cùng nhau. Gödel còn tìm ra một nghiệm của phương trình thuyết tương đối rộng mô tả một vũ trụ quay, trong đó về lý thuyết có những đường cong thời gian khép kín. Đây là đóng góp của ông cho vật lý.
Có cần học logic toán để hiểu kỹ định lý Gödel không?
Để hiểu chính xác, bạn cần nền logic vị từ bậc nhất và một ít lý thuyết tính được, thường có trong các học phần logic toán năm ba hoặc năm tư. Nhưng ý chính, cách mã hoá và câu tự quy chiếu, có thể hiểu ở mức sinh viên năm nhất với một giáo trình nhập môn tốt.