Các Định lý của Godel và Triết lý của Chúng

Bằng cách mã hóa tính tự tham chiếu vào số học, Godel đã chứng minh rằng bất kỳ hệ thống hình thức nhất quán nào đủ phong phú cho số học đều chứa các câu đúng mà nó không thể chứng minh.

Definition

Định lý không đầy đủ thứ nhất của Godel phát biểu rằng bất kỳ hệ thống hình thức nhất quán, được tiên đề hóa hiệu quả nào có khả năng biểu diễn số học sơ cấp đều chứa một câu đúng mà nó không thể chứng minh cũng như bác bỏ; định lý thứ hai phát biểu rằng không có hệ thống nào như vậy có thể chứng minh tính nhất quán của chính nó.

Scope

Chủ đề này bao gồm các định lý không đầy đủ của Godel và cách giải thích triết học của chúng. Nó đề cập đến kỹ thuật số học hóa (đánh số Godel) và bổ đề đường chéo xây dựng một câu tự tham chiếu 'Tôi không thể chứng minh được'; định lý thứ nhất (các hệ thống như vậy không đầy đủ) và định lý thứ hai (chúng không thể chứng minh tính nhất quán của chính mình); và những ứng dụng triết học gây tranh cãi của các định lý — những tuyên bố về giới hạn của chủ nghĩa hình thức và chương trình của Hilbert, cũng như các lập luận của Lucas-Penrose rằng tâm trí con người vượt trội hơn bất kỳ thuật toán nào.

Core questions

• Việc đánh số Godel cho phép số học nói về các chứng minh của chính nó như thế nào?
• Các định lý không đầy đủ thiết lập chính xác điều gì và cho những hệ thống nào?
• Các định lý có ý nghĩa gì đối với chương trình của Hilbert và chủ nghĩa logic?
• Các định lý có cho thấy tâm trí vượt trội hơn máy móc không?

Key concepts

• Đánh số Godel (số học hóa)
• Bổ đề đường chéo
• Câu Godel
• Các định lý không đầy đủ thứ nhất và thứ hai
• Chương trình của Hilbert
• Tính nhất quán và tính omega-nhất quán

Key theories

Tính không đầy đủ thông qua phép chéo hóa

Godel số học hóa cú pháp để một công thức có thể biểu thị tính không thể chứng minh của chính nó; câu kết quả là đúng (nếu hệ thống nhất quán) nhưng không thể chứng minh được, thiết lập tính không đầy đủ, và định lý thứ hai cho thấy tính nhất quán tự thân là không thể chứng minh được trong hệ thống.

Lập luận của Lucas-Penrose

Lucas lập luận từ định lý của Godel rằng, bởi vì con người có thể thấy sự thật của câu Godel của bất kỳ cỗ máy nhất quán nào mô phỏng tâm trí, nên tâm trí không thể là một cỗ máy như vậy; lập luận này bị tranh cãi rộng rãi.

History

Godel đã chứng minh các định lý không đầy đủ vào năm 1931, giới hạn một cách dứt khoát chương trình của Hilbert nhằm chứng minh toán học là đầy đủ và nhất quán bằng các phương tiện hữu hạn. Các kết quả này đã gây tiếng vang lớn trong triết học toán học và tâm trí, với Lucas (1961) và sau đó là Penrose đưa ra các kết luận chống cơ học đã thúc đẩy một lượng lớn tài liệu phê bình.

Debates

Các định lý có bác bỏ chủ nghĩa cơ học về tâm trí không?

Liệu lập luận của Lucas-Penrose có suy luận hợp lệ từ tính không đầy đủ rằng sự hiểu biết toán học của con người vượt qua bất kỳ thuật toán nào, hay liệu nó có quá mức khi giả định rằng chúng ta luôn có thể biết tính nhất quán của chính mình và nhận ra câu Godel có liên quan.

Key figures

• Kurt Godel
• David Hilbert
• J. R. Lucas
• Roger Penrose
• Peter Smith

Seminal works

• godel1931
• smith2013

Frequently asked questions

Định lý của Godel có nghĩa là toán học bị hỏng không?

Không. Nó có nghĩa là không có hệ thống hình thức nhất quán đơn lẻ nào có thể chứng minh mọi sự thật số học, và không hệ thống nào có thể tự chứng nhận tính nhất quán của chính nó từ bên trong. Toán học vẫn tiến triển hoàn toàn tốt; các định lý thay vào đó đặt ra một giới hạn có nguyên tắc đối với những gì bất kỳ hệ thống tiên đề cố định nào có thể đạt được, bác bỏ hy vọng về một nền tảng hoàn chỉnh, tự chứng nhận.