Định lýĐã chứng minh

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

Phát biểu

Trong mọi hệ hình thức nhất quán $F$ đủ mạnh để biểu diễn số học cơ bản (chẳng hạn chứa số học Peano) mà tập tiên đề của nó liệt kê được bằng thuật toán, luôn tồn tại một mệnh đề $G$ đúng nhưng không thể chứng minh cũng không thể bác bỏ trong $F$ .

Vì sao đúng?

Gödel xây dựng một mệnh đề mà, nhờ cách đánh số các công thức và chứng minh (số Gödel) biến câu nói về khả năng chứng minh thành câu nói về số, về bản chất tự nói về mình rằng 'Tôi không chứng minh được trong $F$ '. Nếu $F$ chứng minh được $G$ thì $F$ sẽ mâu thuẫn (chứng minh một điều sai); nếu $F$ chứng minh được $\neg G$ thì $F$ cũng chứng minh một điều sai. Vậy $G$ đúng nhưng không quyết định được trong $F$ .

Phác thảo chứng minh

Gán cho mỗi công thức và mỗi dãy hữu hạn công thức (một chứng minh khả dĩ) một số tự nhiên duy nhất (số Gödel); biểu diễn quan hệ 'số $y$ mã hóa một chứng minh của công thức được mã hóa bởi $x$ ' thành một quan hệ số học quyết định được $\mathrm{Prf}(y,x)$ ; dùng phép xây dựng đường chéo để tạo mệnh đề $G$ mà, khi giải mã, phát biểu $\neg\exists y\, \mathrm{Prf}(y,\ulcorner G\urcorner)$ (không có số nào mã hóa một chứng minh của $G$ ); sau đó xét hai trường hợp $F\vdash G$ và $F\vdash\neg G$ cho thấy trường hợp đầu mâu thuẫn với tính nhất quán còn trường hợp sau mâu thuẫn với tính $\omega$ -nhất quán (được làm yếu thành tính nhất quán thông thường nhờ cải tiến của Rosser), nên $F$ không chứng minh được cả hai, trong khi $G$ vẫn đúng.

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 Logic vị từ

Định lý liên quan

Định lý bất toàn thứ hai của Gödel Định lý đầy đủ của Gödel Tính không giải được của bài toán dừng

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
Ernest Nagel, James R. Newman (2001). Gödel's Proof