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

Nhờ bổ đề đường chéo (người họ hàng hình thức của lập luận đường chéo Cantor), số học có thể dựng một câu $G_F$ thỏa $F \vdash G_F \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G_F\urcorner)$ — một câu tự khẳng định rằng nó không chứng minh được trong $F$. Nếu $F \vdash G_F$, thì $\mathrm{Prov}_F(\ulcorner G_F\urcorner)$ đúng, nên $F \vdash \neg G_F$, mâu thuẫn với tính nhất quán. Do đó $F \nvdash G_F$ — đó chính xác là điều $G_F$ khẳng định, khiến $G_F$ đúng trên $\mathbb{N}$. (Về sau Rosser đã bỏ được giả thiết $\omega$-nhất quán.)

Bước 1 (số học hóa cú pháp). Cố định một cách mã hóa tính toán được, gán cho mỗi ký hiệu, mỗi công thức, và mỗi dãy hữu hạn công thức trong ngôn ngữ của $F$ một số tự nhiên duy nhất, gọi là số Gödel của nó. Vì $F$ được tiên đề hóa hiệu quả, quan hệ $\mathrm{Prf}_F(p, n)$ — "$p$ là mã của một chứng minh cho công thức có mã $n$" — có thể diễn đạt bằng một công thức số học chỉ dùng $+$, $\times$ và các lượng từ, vì việc kiểm tra một chứng minh từng dòng là một thủ tục cơ giới hữu hạn. Đặt $\mathrm{Prov}_F(n) := \exists p\, \mathrm{Prf}_F(p, n)$.

Bước 2 (bổ đề đường chéo). Với mọi công thức số học $\psi(x)$ có một biến tự do, bổ đề đường chéo tạo ra một câu $D$ sao cho $F \vdash D \leftrightarrow \psi(\ulcorner D \urcorner)$ — $D$ khẳng định về chính mã của nó rằng $\psi(x)$ đúng với nó. Áp dụng điều này cho $\psi(x) := \neg\mathrm{Prov}_F(x)$: ta thu được một câu $G_F$ với $F \vdash G_F \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G_F \urcorner)$. Nói nôm na, $G_F$ nói rằng "Tôi không chứng minh được trong $F$."

Bước 3 ($F \nvdash G_F$). Giả sử phản chứng rằng $F \vdash G_F$. Vì $F$ được tiên đề hóa hiệu quả, bản thân chứng minh này có một mã $p_0$, nên $\mathrm{Prf}_F(p_0, \ulcorner G_F \urcorner)$ đúng, do đó $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner)$ (các sự kiện số học chứng minh được về những con số cụ thể thì tự chúng cũng chứng minh được trong $F$). Nhưng tương đương đường chéo kết hợp với $F \vdash G_F$ lại cho $F \vdash \neg \mathrm{Prov}_F(\ulcorner G_F \urcorner)$. Vậy $F$ chứng minh được cả một mệnh đề lẫn phủ định của nó, mâu thuẫn với tính nhất quán. Do đó $F \nvdash G_F$.

Bước 4 ($G_F$ đúng, và — với giả thiết $\omega$-nhất quán — $F \nvdash \neg G_F$). Vì $F \nvdash G_F$, không số nào mã hóa một chứng minh của $G_F$, nên $\neg\mathrm{Prov}_F(\ulcorner G_F \urcorner)$ đúng trên $\mathbb{N}$; theo tương đương đường chéo, đây chính xác là điều $G_F$ khẳng định, nên $G_F$ đúng. Nếu $F$ cũng chứng minh được phủ định của $G_F$, tức $F \vdash \neg G_F$, thì kết hợp điều này với tương đương đường chéo sẽ cho $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner)$ — "có số $p$ nào đó mã hóa một chứng minh của $G_F$" — mà không hề có một chứng minh cụ thể nào làm chứng, đúng là tình huống mà $\omega$-nhất quán loại trừ. Vậy với $\omega$-nhất quán, $F \nvdash \neg G_F$ cũng đúng, và $F$ không đầy đủ.

Chính phép chứng minh của định lý thứ nhất — "nếu $F$ nhất quán thì $F$ không chứng minh được $G_F$" — có thể được hình thức hóa ngay bên trong $F$, cho ra $F \vdash \mathrm{Con}(F) \to G_F$. Nếu $F$ chứng minh được $\mathrm{Con}(F)$, quy tắc modus ponens sẽ suy ra $F \vdash G_F$, mâu thuẫn với định lý thứ nhất.

Bước 1 (vị từ chứng minh được hình thức hóa được, chứ không chỉ định nghĩa được). Vì $\mathrm{Prov}_F$ được xây dựng từ quan hệ cơ giới, kiểm tra được $\mathrm{Prf}_F(p,n)$, ba "điều kiện suy dẫn được" sau tự chúng chứng minh được ngay bên trong $F$ (đây là chỗ lập luận cần $F$ mở rộng số học Peano, chứ không chỉ cần nhất quán): ($P_1$) nếu $F$ chứng minh được $\varphi$ thì $F$ chứng minh được $\mathrm{Prov}_F(\ulcorner\varphi\urcorner)$; ($P_2$) $F$ chứng minh được $\mathrm{Prov}_F(\ulcorner\varphi\to\psi\urcorner) \to (\mathrm{Prov}_F(\ulcorner\varphi\urcorner)\to\mathrm{Prov}_F(\ulcorner\psi\urcorner))$; ($P_3$) $F$ chứng minh được $\mathrm{Prov}_F(\ulcorner\varphi\urcorner) \to \mathrm{Prov}_F(\ulcorner\mathrm{Prov}_F(\ulcorner\varphi\urcorner)\urcorner)$.

Bước 2 (hình thức hóa chính lập luận của Định lý 1). Theo tương đương đường chéo, $F \vdash \neg G_F \to \mathrm{Prov}_F(\ulcorner G_F \urcorner)$. Lập luận không hình thức của Định lý 1 — "nếu $G_F$ chứng minh được, thì chính chứng minh đó sẽ làm chứng cho $\mathrm{Prov}_F(\ulcorner G_F\urcorner)$, và tương đương đường chéo khi đó sẽ trao cho ta một chứng minh của $\neg G_F$ luôn" — không dùng gì ngoài thao tác cơ giới trên ký hiệu đã được bao trùm bởi ($P_1$)–($P_3$), nên nó có thể được mô phỏng từng bước như một suy diễn hình thức ngay bên trong $F$, cho ra $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner) \to \mathrm{Prov}_F(\ulcorner \neg G_F \urcorner)$. Vì chứng minh được cả $G_F$ lẫn phủ định của nó cho phép $F$ suy ra $0 = 1$ bằng nguyên lý ex falso quodlibet, điều này cho $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner) \to \neg\mathrm{Con}(F)$, tức $F \vdash \mathrm{Con}(F) \to G_F$.

Bước 3 (kết luận). Giả sử phản chứng rằng $F \vdash \mathrm{Con}(F)$. Kết hợp với $F \vdash \mathrm{Con}(F) \to G_F$ bằng modus ponens, $F$ sẽ chứng minh được $G_F$. Nhưng Định lý 1 đã cho thấy $F \nvdash G_F$ với $F$ nhất quán — mâu thuẫn. Vậy $F$ không thể chứng minh được $\mathrm{Con}(F)$, đúng như khẳng định.

Được Gödel chứng minh năm 1929 (luận án tiến sĩ của ông), định lý này nói rằng các quy tắc suy luận của logic bậc nhất là đầy đủ: chúng không bỏ sót hệ quả logic nào. Định lý bất toàn (1931) không mâu thuẫn với điều đó: $G_F$ không chứng minh được là vì $F$ có những mô hình phi chuẩn trong đó $G_F$ sai, dù $G_F$ đúng trong mô hình chuẩn $\mathbb{N}$.

Bước 1 (tính đúng đắn — chiều dễ, $T \vdash \varphi$ kéo theo $T \models \varphi$). Lập luận bằng quy nạp theo độ dài của một chứng minh hình thức của $\varphi$ từ $T$. Mọi tiên đề của $T$ đúng trong bất kỳ mô hình $M$ nào của $T$ theo định nghĩa; mọi tiên đề thuần túy logic (chẳng hạn $\varphi \to (\psi \to \varphi)$) là hằng đúng, đúng dưới mọi cách diễn giải bất kỳ. Và mỗi quy tắc suy luận bảo toàn tính đúng trong $M$: với modus ponens, nếu $M \models \theta$ và $M \models \theta \to \varphi$ thì tự động $M \models \varphi$. Vậy mọi dòng của chứng minh đều đúng trong $M$, đặc biệt dòng cuối, $\varphi$, cũng đúng; vì $M$ là một mô hình bất kỳ của $T$, nên $T \models \varphi$.

Bước 2 (tính đầy đủ — chiều khó, bằng phản đảo: $T \nvdash \varphi$ kéo theo $T \not\models \varphi$). Giả sử $T \nvdash \varphi$. Khi đó tập $T \cup \{\neg\varphi\}$ nhất quán (nếu nó chứng minh được một mâu thuẫn, $T$ sẽ chứng minh được $\varphi$ bằng phản chứng). Dùng phương pháp Henkin, mở rộng nó thành một tập nhất quán tối đại $\Sigma$ có nhân chứng: mỗi khi $\exists x\, \psi(x)$ nằm trong $\Sigma$, một hằng số $c$ mới được thêm vào sao cho $\psi(c)$ cũng nằm trong $\Sigma$. Dựng mô hình số hạng $M_\Sigma$ có các phần tử là những số hạng đóng của ngôn ngữ mở rộng, đồng nhất theo đẳng thức chứng minh được trong $\Sigma$, với các quan hệ và hàm được diễn giải trực tiếp từ $\Sigma$. Một phép quy nạp theo độ dài số hạng ("bổ đề chân lý") khi đó cho $M_\Sigma \models \theta \iff \theta \in \Sigma$ với mọi câu $\theta$.

Bước 3 (lắp ráp mô hình, và kết luận). Vì $\neg\varphi \in \Sigma$, bổ đề chân lý cho $M_\Sigma \models \neg\varphi$, và vì mọi tiên đề của $T$ đều nằm trong $\Sigma$, cũng có $M_\Sigma \models T$. Vậy $M_\Sigma$ là một mô hình thực sự của $T$ trong đó $\varphi$ sai, tức $T \not\models \varphi$. Điều này chứng minh mệnh đề phản đảo của Bước 2, và kết hợp với Bước 1, $T \vdash \varphi$ đúng khi và chỉ khi $T \models \varphi$ — đây chính là kết quả trong luận án tiến sĩ năm 1929 của Gödel, sau này được Leon Henkin (1949) tinh gọn lại thành phép dựng mô hình số hạng dùng ở đây.

Giả sử $H(P, x)$ quyết định được việc dừng. Ta dựng một máy $D(P)$ chạy $H(P, P)$, rồi lặp vô hạn nếu $H$ trả lời "dừng", và dừng nếu $H$ trả lời "lặp". Đưa cho $D$ chính mã của nó: $D(D)$ dừng khi và chỉ khi $H(D, D)$ nói rằng nó lặp — mâu thuẫn. Đây là người anh em song sinh bên phía tính toán của câu đường chéo Gödel.

Bước 1 (giả sử tồn tại bộ quyết định việc dừng). Giả sử phản chứng rằng tồn tại một thuật toán $H$ sao cho $H(P, x)$ luôn dừng và trả lời đúng "dừng" nếu chương trình có mã $P$ dừng trên đầu vào $x$, và "lặp" nếu ngược lại.

Bước 2 (dựng một máy đường chéo từ $H$). Định nghĩa một thuật toán mới $D(P)$ mà, với đầu vào là mã một chương trình $P$, trước hết tính $H(P, P)$ — chạy $H$ với $P$ được đưa vào làm cả hai vai trò chương trình lẫn đầu vào. Nếu $H(P, P)$ trả lời "dừng", thì $D$ cố tình đi vào vòng lặp vô hạn; nếu $H(P, P)$ trả lời "lặp", thì $D$ dừng ngay lập tức (chẳng hạn, trả về $0$).

Bước 3 (đưa cho $D$ chính mã của nó). Vì $D$ tự nó là một thuật toán, nó có một mã, và không gì ngăn ta chạy $D$ trên chính mã đó: xét $D(D)$. Có hai trường hợp, cả hai đều bất khả: nếu $D(D)$ dừng, thì theo cách dựng điều này xảy ra chính xác khi $H(D, D)$ trả lời "lặp" — nghĩa là $H$ đã báo sai rằng $D$ trên $D$ không dừng, dù nó vừa mới dừng. Nếu ngược lại $D(D)$ chạy mãi mãi, điều này xảy ra chính xác khi $H(D, D)$ trả lời "dừng" — nghĩa là $H$ đã báo sai rằng nó dừng, dù nó lặp vô hạn.

Bước 4 (kết luận). Dù trường hợp nào, $H$ cũng cho câu trả lời sai trên đầu vào $(D, D)$, mâu thuẫn với giả thiết rằng $H$ luôn đúng. Vậy không thể tồn tại thuật toán $H$ như thế: bài toán dừng không quyết định được.