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

Ba công cụ tương tác giúp bạn khám phá trực tiếp ba ý tưởng cốt lõi: đánh số Gödel, câu tự quy chiếu, và khoảng cách giữa "đúng" và "chứng minh được".

1. Máy đánh số Gödel

Chọn các ký hiệu để xây dựng một biểu thức. Máy sẽ mã hóa từng ký hiệu thành lũy thừa nguyên tố và tính số Gödel của toàn bộ biểu thức. Bấm vào token trong biểu thức để xóa từng ký hiệu.

Chọn ký hiệu bên trên để bắt đầu...
Thử nhanh:
Bảng ký hiệu & mã Gödel

2. Câu Gödel — "Tôi không chứng minh được"

Câu Gödel G tránh được mâu thuẫn của kẻ nói dối bằng một thay đổi nhỏ nhưng quyết định. Khám phá từng bước suy luận qua sơ đồ tương tác.

Nghịch lý kẻ nói dối (Liar)
"Câu này là SAI."
Gán T: "câu này sai" đúng → câu là sai → F ≠ T Mâu thuẫn
Gán F: "câu này sai" sai → câu không sai → đúng → T ≠ F Mâu thuẫn
Kết quả: không thể gán T hay F Không phải mệnh đề
Câu Gödel G
"Câu này KHÔNG CHỨNG MINH được."
Nếu G ⊢ (chứng minh được): G nói G không ⊢ → mâu thuẫn với nhất quán Không thể xảy ra
Nếu G không ⊢: G nói G không ⊢ → G nói đúng! Không mâu thuẫn
Kết quả: G không ⊢, nhưng G đúng Hệ bất toàn

Sơ đồ suy luận từng bước — câu Gödel G trong hệ nhất quán H:

Hệ hình thức H Tiên đề PA₁, PA₂, ... Luật suy diễn Modus ponens, ... Định lý ⊢ 2+2=4, ... G "G không chứng minh được trong H" ✗ ✓ Đúng!

3. Provable ⊊ True — sơ đồ Venn

Định lý bất toàn thứ nhất cho thấy tập định lý chứng minh được là một tập con thực sự nhỏ hơn tập mệnh đề đúng — có câu đúng nhưng không chứng minh được. Sơ đồ dưới đây minh họa quan hệ giữa ba vùng.

Mọi câu hình thức Câu ĐÚNG (True) Chứng minh được (Provable ⊢) G (đúng, không ⊢) G đúng ≠ ⊢ PH Sai 2+2=4 Goldbach?
Chứng minh được (⊢)
Đúng nhưng không ⊢ (vùng bất toàn)
Sai hoặc vô nghĩa (ngoài True)
Ví dụ cụ thể (bấm xem)