Định lý không đầy đủ của Gödel và Tính toán

Các định lý không đầy đủ của Gödel chỉ ra rằng bất kỳ hệ thống hình thức nào đủ mạnh và nhất quán đều chứa những phát biểu đúng mà nó không thể chứng minh, một kết quả gắn liền sâu sắc với tính không quyết định được phát hiện trong lý thuyết tính toán.

Definition

Các định lý không đầy đủ phát biểu rằng bất kỳ hệ thống hình thức nhất quán nào có khả năng biểu diễn số học cơ bản đều không đầy đủ, với các phát biểu số học đúng mà nó không thể chứng minh, và không thể chứng minh tính nhất quán của chính nó; về mặt tính toán, tập hợp các phát biểu có thể chứng minh được là có thể nhận biết được nhưng phần bù của nó thì không, phản ánh tính không quyết định.

Scope

Chủ đề này bao gồm định lý không đầy đủ thứ nhất và thứ hai, kỹ thuật số học hóa (arithmetization) và tự tham chiếu thông qua đánh số Gödel, mối quan hệ chặt chẽ giữa tính không đầy đủ và tính không quyết định của bài toán dừng và của logic bậc nhất, cùng với những hệ quả đối với giới hạn của suy luận hình thức và chứng minh tự động.

Core questions

• Tại sao không có hệ thống hình thức nào nhất quán, đủ mạnh có thể chứng minh tất cả các phát biểu số học đúng?
• Làm thế nào mà sự tự tham chiếu thông qua đánh số Gödel tạo ra một câu đúng không thể chứng minh được?
• Tính không đầy đủ và tính không quyết định của bài toán dừng là hai khía cạnh của một hiện tượng như thế nào?
• Tính không đầy đủ ngụ ý gì đối với giới hạn của việc chứng minh định lý tự động?

Key theories

Định lý không đầy đủ thứ nhất

Bất kỳ hệ thống hình thức nhất quán nào đủ mạnh để mã hóa số học đều chứa một phát biểu đúng mà nó không thể chứng minh cũng như không thể bác bỏ, được xây dựng bởi một câu mà về cơ bản khẳng định tính không thể chứng minh của chính nó.

Tính không đầy đủ thông qua tính toán

Tính không đầy đủ xuất phát từ tính không quyết định của bài toán dừng: nếu mọi chân lý số học đều có thể chứng minh được, người ta có thể quyết định việc dừng bằng cách tìm kiếm các chứng minh, vì vậy sự tồn tại của các vấn đề không quyết định được buộc phải có sự tồn tại của các chân lý không thể chứng minh được.

Clinical relevance

Tính không đầy đủ và đối tác tính toán của nó đặt ra những giới hạn cứng rắn đối với suy luận tự động: không có thuật toán nào có thể quyết định tất cả các chân lý số học hoặc giải quyết mọi vấn đề toán học, vì vậy các hệ thống chứng minh định lý và xác minh phải dựa vào sự hướng dẫn của con người, các lý thuyết hạn chế, hoặc chứng minh tương tác thay vì quyết định tự động hoàn toàn.

History

Gödel đã chứng minh các định lý không đầy đủ vào năm 1931, dập tắt hy vọng của Hilbert về một sự hình thức hóa toán học hoàn chỉnh và tự biện minh. Trong vòng năm năm, Church và Turing đã kết nối những giới hạn này với tính không quyết định, và cách đọc tính không đầy đủ theo hướng tính toán thông qua bài toán dừng đã trở thành một yếu tố chủ yếu của lý thuyết tính toán.

Key figures

• Kurt Gödel
• Alan Turing
• Alonzo Church
• John Barkley Rosser

Seminal works

• godel1931
• boolos2007

Frequently asked questions

Tính không đầy đủ có nghĩa là toán học bị lỗi không?

Không. Nó có nghĩa là không có một hệ thống hình thức nhất quán nào có thể chứng minh mọi chân lý số học, chứ không phải toán học không nhất quán hoặc không đáng tin cậy. Các nhà toán học làm việc trong và giữa các hệ thống hình thức, và tính không đầy đủ chỉ đơn thuần đánh dấu một giới hạn nội tại về những gì bất kỳ hệ thống cố định nào có thể nắm bắt.

Định lý Gödel liên quan đến bài toán dừng như thế nào?

Chúng có mối liên hệ chặt chẽ. Tính không giải được của bài toán dừng ngụ ý tính không đầy đủ: nếu một hệ thống hình thức có thể chứng minh mọi chân lý về việc chương trình nào dừng, người ta có thể quyết định việc dừng bằng cách tìm kiếm các chứng minh, mâu thuẫn với kết quả của Turing. Cả hai đều thể hiện, trong logic và trong tính toán, cùng một giới hạn cơ bản của phương pháp hình thức.