Định lýĐã chứng minh

Định lý bất toàn thứ hai của Gödel

Phát biểu

Cho $F$ là một hệ hình thức nhất quán thỏa mãn các giả thiết của định lý bất toàn thứ nhất, và gọi $\mathrm{Con}(F)$ là mệnh đề số học phát biểu 'không tồn tại chứng minh cho một mâu thuẫn trong $F$ '. Khi đó $F$ không thể chứng minh $\mathrm{Con}(F)$ .

Vì sao đúng?

Toàn bộ lập luận chứng minh định lý bất toàn thứ nhất có thể được thực hiện và kiểm chứng ngay bên trong $F$ , cho ra $F\vdash \mathrm{Con}(F)\to G$ (với $G$ là mệnh đề của định lý thứ nhất). Nếu $F$ cũng chứng minh được $\mathrm{Con}(F)$ , nó sẽ chứng minh được $G$ , mâu thuẫn với định lý thứ nhất. Vậy không hệ nào đủ mạnh và nhất quán có thể tự chứng nhận tính nhất quán của chính mình từ bên trong.

Phác thảo chứng minh

Hình thức hóa toàn bộ chứng minh của định lý bất toàn thứ nhất thành một dãy các mệnh đề số học suy ra được ngay trong $F$ (cần cẩn trọng: vị từ chứng minh được $\mathrm{Prf}$ phải thỏa các điều kiện chứng minh được Hilbert–Bernays), thu được $F\vdash \mathrm{Con}(F)\to G$ ; vì $F\nvdash G$ theo định lý thứ nhất (giả sử tính nhất quán), suy ra $F\nvdash \mathrm{Con}(F)$ .

Người chứng minh

chứng minh năm 1931Kurt Gödel

Chủ đề chứa định lý này

Định lý bất toàn Gödel

Định lý liên quan

Định lý bất toàn thứ nhất của Gödel Định lý đầy đủ của Gödel

Chứng minh từng bước

Chưa có chứng minh từng bước cho định lý này.

Tài liệu tham khảo

Kurt Gödel (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I · DOI:10.1007/s00605-006-0423-7
Martin Davis (ed.) (1965). The Undecidable