Đặt vấn đề

Hãy tưởng tượng chúng ta chế tạo được một con robot tên là Bé Chứng Minh.

Bé này không biết buồn.

Không biết đói.

Không biết chủ nhật là ngày nghỉ.

Nó chỉ có một cuốn sách luật rất dày.

Trong sách ghi một số điều được phép tin ngay từ đầu, gọi là tiên đề (axiom), cùng một đống quy tắc kiểu:

Nếu đã chứng minh được A, và đã chứng minh được “A kéo theo B”, thì được phép kết luận B.

Thế là mỗi ngày Bé Chứng Minh ngồi trong căn phòng lạnh lẽo của nó, cầm những ký hiệu như:

$$ 0,1,+,\times,=,\forall,\exists $$

rồi ghép chúng lại, từng bước một, không sai một ly.

Nếu hỏi:

$$ 1 + 1 = 2? $$

Nó chứng minh.

Nếu hỏi một định lý phức tạp hơn, nó có thể mất mười phút, mười năm, hoặc mười triệu năm, nhưng về nguyên tắc chúng ta vẫn hy vọng:

nếu câu đó đúng, rồi một ngày nào đó con robot cũng sẽ chứng minh được.

Nghe khá hợp lý.

Toán học chẳng phải là thứ chắc chắn nhất con người có hay sao?

Một tam giác không tranh luận.

Số 7 không đổi ý vào sáng thứ Hai.

Phương trình không nổi nóng vì bị xúc phạm.

Vậy chỉ cần chọn đúng tiên đề, viết đúng luật, rồi nhét toàn bộ toán học vào một cỗ máy suy luận khổng lồ.

Câu nào đúng thì máy chứng minh TRUE.

Câu nào sai thì máy chứng minh FALSE.

Xong.

Toán học được đóng hộp.

Vũ trụ của những con số cuối cùng đã bị con người nhốt gọn vào một quyển sách luật.

Hãy hình dung một cỗ máy nhận tiên đề ở đầu vào và liên tục sinh ra các định lý ở đầu ra. Giấc mơ đầu thế kỷ XX là liệu một hệ thống như vậy có thể bao phủ toàn bộ toán học hay không.

Rồi năm 1931, một ông tên là Kurt Gödel đi tới.

Ông không đập cái máy.

Ông cũng không nói toán học sai.

Ông chỉ nhẹ nhàng chỉ vào cuốn sách luật rồi nói đại ý:

Dù các anh viết cuốn sách này cẩn thận đến đâu, nếu nó đủ mạnh để nói về số tự nhiên, sẽ luôn có thứ lọt ra ngoài.

Và từ đây mọi chuyện bắt đầu hơi ngáo.

Giấc mơ nhốt toán học vào một chiếc hộp

Đầu thế kỷ XX, toán học gặp một vấn đề khá nghiêm trọng.

Người ta đã xây được những tòa lâu đài khổng lồ: giải tích, hình học, đại số, lý thuyết tập hợp…

Nhưng càng xây cao, người ta càng bắt đầu hỏi:

Cái móng bên dưới có chắc không?

David Hilbert và nhiều nhà toán học thời đó muốn đưa toán học về một nền móng thật chặt chẽ.

Ý tưởng đại khái là:

Chọn một tập tiên đề rõ ràng.
Chọn các quy tắc suy luận chính xác.
Từ đó chứng minh tất cả các định lý.
Đồng thời chứng minh rằng hệ thống không bao giờ tự sinh ra mâu thuẫn.

Ta có thể hình dung hệ thống này giống một trò chơi LEGO.

Tiên đề là những viên LEGO ban đầu.

Quy tắc suy luận nói rằng những viên nào được phép gắn với nhau.

Định lý là những thứ ta xây ra được.

Nếu mọi thứ hoàn hảo, ta muốn hai tính chất.

Consistent – nhất quán

Hệ thống không được chứng minh đồng thời:

$$ P $$

và:

$$ \neg P $$

Ví dụ nó không được vừa chứng minh:

2 + 2 = 4

vừa chứng minh:

2 + 2 ≠ 4

Nếu chuyện đó xảy ra thì coi như nhà cháy.

Trong logic cổ điển, từ một mâu thuẫn ta có thể suy ra đủ thứ linh tinh.

Complete – đầy đủ

Với mọi mệnh đề hợp lệ mà hệ thống có thể diễn đạt, ta muốn nó quyết định được:

$$ P $$

hoặc:

$$ \neg P $$

Nôm na:

Không được có câu hỏi nào cứ treo lơ lửng mãi mãi.

Đây là một giấc mơ rất đẹp.

Một cuốn sách cuối cùng.

Một bộ luật cuối cùng.

Một cái hộp đủ lớn để chứa toàn bộ chân lý toán học.

Nhưng Gödel tìm thấy một vết nứt ngay trong thành hộp.

Gödel làm trò gì?

Ý tưởng quan trọng nhất của Gödel nghe đơn giản đến mức hơi đáng ngờ:

Ông biến các câu toán học thành số.

Đây được gọi là Gödel numbering.

Thay vì nhìn:

10 = 0

như một chuỗi ký hiệu, ta có thể gán cho mỗi ký hiệu một con số.

Ví dụ minh họa:

10   -> 1
2=   -> 2
3+   -> 3
4(   -> 4
5)   -> 5
6...

Sau đó một công thức dài có thể được mã hóa thành một số tự nhiên rất lớn.

Cách mã hóa thực tế tinh vi hơn ví dụ trên, nhưng điểm quan trọng là:

Công thức trở thành số.

Không chỉ công thức.

Một bằng chứng cũng trở thành số.

Gödel numbering tạo ra một cây cầu kỳ quặc: một phía là ngôn ngữ nói về số; phía kia, chính những câu của ngôn ngữ đó cũng được biến thành số.

Đây là khoảnh khắc rất quan trọng.

Bởi vì khi câu chữ đã biến thành số, số học có thể bắt đầu nói về chính những câu chữ của số học.

Con rắn bắt đầu quay đầu nhìn thấy cái đuôi của mình.

Một cuốn sách đột nhiên đọc được chính nó

Giả sử trong hệ thống của chúng ta có câu:

Có một bằng chứng cho mệnh đề X.

Bởi vì cả X lẫn bằng chứng đều đã được mã hóa thành số, câu trên cũng có thể được diễn đạt bằng số học.

Ta có thể tưởng tượng một hàm:

$$ Proof(p,x) $$

mang ý nghĩa:

Số p mã hóa một bằng chứng hợp lệ cho mệnh đề có mã x.

Khi đó:

$$ \exists p ; Proof(p,x) $$

nghĩa là:

Tồn tại một bằng chứng cho câu x.

Và:

$$ \neg \exists p ; Proof(p,x) $$

nghĩa là:

Không tồn tại bằng chứng cho câu x.

Đến đây hệ thống đã đạt được một khả năng hơi nguy hiểm.

Nó không chỉ nói:

2 + 3 = 5.

Nó còn có thể nói:

Câu số 938472394823742 không có bằng chứng.

Nó bắt đầu bàn tán về khả năng chứng minh của chính mình.

Và Gödel dùng kỹ thuật tự tham chiếu để xây dựng một câu đặc biệt, gọi tạm là G.

Ý nghĩa của G gần giống:

Câu G này không thể được chứng minh trong hệ thống này.

Đọc lại lần nữa.

Tôi không thể được chứng minh ở đây.

Một mảnh toán học đang nói về số phận của chính nó.

Bây giờ cái hộp bắt đầu rung

Ta có:

G = “G không thể được chứng minh trong hệ thống F.”

Giả sử hệ thống F chứng minh được G.

Khi đó G nói rằng:

G không thể chứng minh được.

Nhưng F vừa chứng minh G.

Hệ thống đã chứng minh một câu tuyên bố rằng chính nó không thể được chứng minh.

Nếu các điều kiện kỹ thuật cần thiết được thỏa mãn, điều này dẫn hệ thống vào rắc rối với tính nhất quán.

Vậy nếu F nhất quán:

$$ F \nvdash G $$

Tức là F không chứng minh được G.

Nhưng khoan.

G nói gì?

G không chứng minh được trong F.

Và đúng là F không chứng minh được G.

Nghĩa là từ góc nhìn bên ngoài hệ thống, G đang mô tả đúng tình trạng của chính mình.

Ta có một thứ cực kỳ kỳ quặc:

một mệnh đề đúng nhưng hệ thống không thể tự chứng minh nó.

Đây chính là tinh thần của Định lý bất toàn thứ nhất của Gödel (Gödel’s First Incompleteness Theorem).

Nói chính xác hơn, với những hệ hình thức nhất quán, được tiên đề hóa hiệu quả và đủ mạnh để biểu diễn một lượng số học cần thiết, sẽ tồn tại những mệnh đề mà hệ không thể quyết định được. (Stanford Encyclopedia of Philosophy)

Nhưng đây có phải nghịch lý “câu này là sai” không?

Rất dễ nhầm Gödel với nghịch lý nói dối:

Câu này là sai.

Nếu câu đó đúng thì nó sai.

Nếu nó sai thì nó đúng.

Đầu quay như chong chóng.

Nhưng Gödel không viết:

Tôi sai.

Ông viết một thứ tinh tế hơn:

Tôi không thể được chứng minh trong hệ thống F.

Hai khái niệm hoàn toàn khác nhau:

Truth: một câu có đúng hay không.
Provability: hệ thống có tạo ra được bằng chứng cho câu đó hay không.

Và đây có lẽ là chỗ đẹp nhất của toàn bộ câu chuyện.

Trước Gödel, người ta có thể mơ rằng:

$$ Truth = Provability $$

Mọi thứ đúng đều có thể chứng minh.

Nhưng Gödel tạo ra một khe hở:

$$ Truth \neq Provability $$

Ít nhất khi ta cố nhốt tất cả vào một hệ hình thức cố định đủ mạnh.

Có những nơi sự thật đứng ở phía bên kia bức tường, còn bộ máy chứng minh của ta cứ chạy vòng vòng phía bên này.

Một ví dụ kiểu trẻ con

Giả sử có một ngôi làng.

Trong làng có một quyển sách tên:

SÁCH LUẬT TỐI CAO

Luật nói rằng mọi giấy chứng nhận hợp lệ đều phải được cấp dựa trên những quy tắc trong sách.

Người dân rất tự hào:

Chuyện gì đúng trong làng thì Sách Luật cũng chứng nhận được hết!

Một hôm có cậu bé Gödel đi vào làng và viết lên một tờ giấy:

Tờ giấy này không thể nhận được giấy chứng nhận từ Sách Luật Tối Cao.

Bây giờ quan chức gặp vấn đề.

Nếu cấp chứng nhận cho nó, nội dung tờ giấy hóa ra sai.

Nếu hệ thống luật đủ nhất quán, họ không thể làm vậy.

Thế là họ không cấp.

Nhưng khi họ không cấp…

…thì điều tờ giấy nói lại đúng.

Cả làng đứng im.

Con chó vẫn chạy.

Cái cây vẫn rung.

Mặt trời vẫn mọc.

Chỉ có ông trưởng làng bắt đầu nghi ngờ cái tên SÁCH LUẬT TỐI CAO nghe hơi tự tin quá.

Thế thì thêm G làm tiên đề là xong chứ?

Đây là phản ứng tự nhiên nhất.

Nếu hệ thống F không chứng minh được G, ta cứ thêm G vào làm tiên đề mới.

Tạo hệ thống:

$$ F_1 = F + G $$

Xong.

G giờ chứng minh được.

Quá dễ.

Gödel chắc quên mất nút Add.

Nhưng không.

Bởi vì nếu hệ thống mới $F_1$ vẫn nhất quán và đủ mạnh, Gödel lại chạy tiếp.

Sẽ tồn tại một câu mới:

$$ G_1 $$

mà $F_1$ không giải quyết được.

Ta thêm tiếp:

$$ F_2 = F_1 + G_1 $$

Rồi lại xuất hiện:

$$ G_2 $$

Cứ thế.

Giống như ta xây bức tường cao hơn để chạm tới đường chân trời.

Cao thêm một mét.

Đường chân trời vẫn ở phía trước.

Cao thêm một kilomet.

Nó vẫn ở đó.

Ta có thể mở rộng một hệ tiên đề để giải quyết những câu trước đây chưa quyết định được. Nhưng nếu hệ mới vẫn thuộc phạm vi của định lý Gödel, nó lại có những câu chưa quyết định được của riêng mình.

Gödel không nói rằng:

Có một câu thần bí mà không hệ thống nào trên đời chứng minh được.

Điều ông chỉ ra tinh tế hơn:

Với mỗi hệ hình thức phù hợp mà ta cố định, nếu nó đủ mạnh và nhất quán, vẫn sẽ có thứ nó không thể quyết định.

Điểm này rất quan trọng vì định lý Gödel thường bị kể quá tay thành đủ loại triết lý vũ trụ mà bản thân định lý không nói. (Stanford Encyclopedia of Philosophy)

Định lý bất toàn thứ hai: cú đấm thứ hai

Gödel chưa dừng lại.

Sau khi chỉ ra rằng một hệ thống không thể chứng minh mọi sự thật có thể diễn đạt bên trong nó, ông còn chứng minh một điều khó chịu hơn.

Giả sử F là một hệ hình thức đủ mạnh và nhất quán.

Ta muốn F chứng minh:

F không bao giờ sinh ra mâu thuẫn.

Gọi câu đó là:

$$ Con(F) $$

Ta hy vọng:

$$ F \vdash Con(F) $$

Nôm na:

Tôi tự kiểm tra rồi. Tôi bảo đảm tôi hoàn toàn đáng tin.

Gödel nói:

Không dễ vậy đâu.

Định lý bất toàn thứ hai cho thấy một hệ thống nhất quán đủ mạnh không thể, bằng những công cụ nội tại phù hợp của chính mình, chứng minh tính nhất quán của chính nó. (Stanford Encyclopedia of Philosophy)

Hãy tưởng tượng một ngân hàng in ra giấy:

Ngân hàng này chắc chắn không bao giờ in tiền giả.

Rồi bằng chứng duy nhất cho câu trên lại là:

Vì ngân hàng này vừa in tờ giấy nói thế.

Ừm.

Có gì đó chưa ổn.

Muốn kiểm tra hệ thống F, ta thường cần đứng trong một hệ thống mạnh hơn, gọi là F'.

Nhưng rồi lại có thể hỏi:

Ai bảo F’ nhất quán?

Ta bước ra ngoài một tầng.

Rồi lại thấy thêm một tầng nữa.

Một chiếc gương soi vào một chiếc gương.

Trong gương là một chiếc gương.

Trong chiếc gương đó lại có một chiếc gương.

Và toán học nhìn xuống hành lang vô tận của chính nó.

Gödel không chứng minh rằng “toán học vô dụng”

Không.

Hoàn toàn ngược lại.

Định lý Gödel chính nó là một thành tựu toán học cực kỳ chính xác.

Nó không nói:

Không gì có thể chứng minh.

Nó nói rằng có giới hạn đối với những gì một hệ hình thức cố định có thể chứng minh.

Phần lớn toán học hằng ngày vẫn hoạt động ngon lành.

Ta vẫn chứng minh được:

$$ a^2+b^2=c^2 $$

trong tam giác vuông.

Vẫn thiết kế CPU.

Vẫn xây cầu.

Vẫn mã hóa dữ liệu.

Vẫn phóng tàu lên trời rồi căng thẳng chờ nó đáp xuống đúng chỗ.

Gödel không phá toán học.

Ông phát hiện đường biên của một cách hiểu về toán học.

Gödel cũng không chứng minh “con người thông minh hơn máy tính”

Đây cũng là một bước nhảy khá phổ biến.

Người ta đôi khi lập luận:

Máy tính là hệ hình thức.

Gödel chứng minh hệ hình thức có giới hạn.

Vậy não người chắc chắn vượt qua mọi máy tính.

Không nhanh vậy được.

Các suy luận liên hệ định lý Gödel với bản chất tuyệt đối của trí tuệ con người hay ý thức là chủ đề triết học còn gây tranh cãi; bản thân định lý bất toàn không trực tiếp chứng minh rằng trí óc con người không thể được mô phỏng bởi máy tính. (Stanford Encyclopedia of Philosophy)

Gödel đang nói một điều rất cụ thể về:

hệ hình thức;
tiên đề;
khả năng biểu diễn số học;
chứng minh;
tính nhất quán;
và tính đầy đủ.

Đi xa khỏi khu vực đó thì phải bước cẩn thận.

Không nên cầm một định lý logic rồi chạy ra hét:

Gödel chứng minh linh hồn tồn tại!

Gödel ở đâu đó chắc cũng hơi mệt.

Điều đáng sợ nhất không phải là “không biết”

Điều làm Gödel đặc biệt không phải vì ông phát hiện một bài toán khó.

Bài toán khó thì toán học có đầy.

Có bài mất 300 năm mới giải được.

Có bài tới giờ vẫn chưa ai giải.

Nhưng một bài toán chưa giải và một mệnh đề không thể giải trong một hệ tiên đề nhất định là hai chuyện khác nhau.

Một bên là:

Chúng ta chưa tìm thấy chìa khóa.

Một bên là:

Với loại chìa khóa đang cho phép sử dụng trong căn phòng này, cái cửa đó không thể mở được.

Đây là chuyển động từ không biết sang biết rằng có giới hạn của việc biết bằng phương pháp này.

Nó giống như đang đi trong một khu rừng.

Ban đầu ta tưởng:

Chỉ cần đi đủ lâu rồi sẽ thấy hết khu rừng.

Gödel nói:

Không. Với chiếc bản đồ này, có những vùng bản đồ không thể tự mô tả hoàn toàn chính nó.

Cái đáng kinh ngạc không phải bóng tối.

Mà là việc toán học có thể dùng chính ánh sáng của nó để chỉ ra:

Ở kia có một nơi ánh sáng này không chiếu tới.

Một chút kỹ thuật: định lý thực sự nói gì?

Phiên bản đơn giản của Định lý bất toàn thứ nhất thường được phát biểu:

Cho một hệ hình thức $F$:

nhất quán;
được tiên đề hóa một cách hiệu quả;
đủ mạnh để biểu diễn một lượng số học cơ bản;

thì $F$ không thể đầy đủ.

Tồn tại một mệnh đề $G$ sao cho hệ không thể giải quyết hoàn toàn nó bằng các quy tắc của chính mình.

Có thể viết hình dung:

$$ F \nvdash G $$

và trong các dạng định lý thích hợp:

$$ F \nvdash \neg G $$

Stanford Encyclopedia of Philosophy mô tả kết quả tổng quát này như một giới hạn của khả năng chứng minh trong các lý thuyết tiên đề hình thức đủ mạnh để thực hiện số học. (Stanford Encyclopedia of Philosophy)

Còn định lý thứ hai:

$$ F \nvdash Con(F) $$

nếu F thực sự nhất quán và đáp ứng các điều kiện kỹ thuật tương ứng.

Điều thú vị là số học đủ sức mã hóa cả hoạt động chứng minh số học.

Đây chính là đòn quyết định.

Gödel biến toán học thành dữ liệu của chính toán học.

Ngày nay dân lập trình nghe hơi quen.

Code có thể đọc code.

Compiler có thể compile compiler.

Interpreter có thể chạy interpreter.

Một chương trình có thể nhận chính source code của nó làm input.

Từ đây xuất hiện cả một gia đình những vấn đề sâu sắc liên quan tới:

self-reference;
computability;
decidability;
halting problem;
formal verification.

Không phải tất cả đều là cùng một định lý, nhưng chúng cùng đứng gần một vực sâu: khi một hệ thống đủ mạnh để quay lại mô tả chính nó, những giới hạn kỳ lạ bắt đầu xuất hiện.

Từ Gödel đến Turing

Năm năm sau bài báo của Gödel, Alan Turing nghiên cứu một câu hỏi nghe rất kiểu dân lập trình:

Có thể viết một chương trình nhận vào một chương trình khác rồi luôn xác định được chương trình kia có dừng hay chạy mãi mãi không?

Nếu tồn tại chương trình như vậy:

1def will_halt(program, input):
2    ...
3    return True_or_False

thì tuyệt đẹp.

Nhưng Halting Problem cho thấy không tồn tại một thuật toán tổng quát giải quyết đúng bài toán này cho mọi chương trình.

Một lần nữa, tự tham chiếu xuất hiện.

Một chương trình được đưa vào để phân tích chính chương trình.

Máy tính quay camera vào màn hình đang chiếu camera.

Màn hình xuất hiện trong màn hình.

Rồi trong màn hình đó lại có một màn hình.

Gödel và Turing không chứng minh cùng một thứ, nhưng lịch sử logic thế kỷ XX đã phát hiện một điều rất sâu:

Có những giới hạn không đến từ việc máy tính quá chậm.

Không đến từ thiếu RAM.

Không đến từ CPU chưa đủ mạnh.

Mà nằm ngay trong cấu trúc logic của bài toán.

Bạn có thể mua thêm một triệu GPU.

Nó vẫn không biến một bài toán bất khả quyết tổng quát thành bài toán có thuật toán giải được.

Đây là loại giới hạn khác hẳn giới hạn kỹ thuật.

Và đây mới là phần triết học thú vị

Con người rất thích những chiếc hộp.

Ta đặt tên.

Ta phân loại.

Ta viết luật.

Ta xây hệ thống.

Rồi vì hệ thống giải thích được 99.999% những thứ ta từng gặp, ta bắt đầu tin rằng:

Có lẽ cái hộp chính là thế giới.

Gödel nhắc chúng ta một điều hơi khó chịu.

Một hệ thống có thể cực kỳ mạnh.

Cực kỳ chính xác.

Không mơ hồ.

Không cảm tính.

Không phạm lỗi số học.

Và vẫn có giới hạn nội tại.

Không phải vì nó ngu.

Mà vì nó là một hệ thống.

Có lẽ điều thú vị nhất của Gödel không nằm ở câu:

Có thứ chúng ta không chứng minh được.

Mà nằm ở câu:

Ta có thể chứng minh rằng khả năng chứng minh có giới hạn.

Đó là một khoảnh khắc rất lạ.

Một công cụ quay lại đo giới hạn của chính công cụ.

Một con mắt nhìn thấy điểm mù của chính nó.

Một chiếc thước phát hiện rằng có những thứ chiếc thước không thể tự đo.

Một bản đồ ghi lên góc bản đồ:

Bản đồ này không thể chứa toàn bộ lãnh thổ mà nó đang cố mô tả.

Và nghịch lý thay, chính dòng chữ đó khiến bản đồ trở nên sâu sắc hơn chứ không kém giá trị đi.

Tổng kết

Nếu phải nhớ Gödel bằng một hình ảnh, mình sẽ không nhớ những công thức dài.

Mình sẽ nhớ một căn phòng.

Trong căn phòng có một cỗ máy chứng minh khổng lồ.

Nó chạy ngày đêm.

Bánh răng quay.

Giấy chạy ra thành từng cuộn.

Hàng triệu định lý được đóng dấu:

PROVED.

Rồi một ngày, cỗ máy in ra một mảnh giấy rất nhỏ.

Trên đó gần như viết rằng:

Có một điều đúng về tôi mà chính tôi không thể chứng minh.

Cỗ máy đứng im.

Không phải vì nó hỏng.

Không phải vì thiếu điện.

Không phải vì ai viết bug.

Mà bởi vì đó chính là hình dạng của giới hạn.

Định lý bất toàn Gödel không nói rằng toán học thất bại.

Nó nói một điều đẹp hơn nhiều:

toán học đủ mạnh để nhận ra rằng bản thân toán học, khi bị nhốt vào một hệ tiên đề cố định, không thể khép kín toàn bộ chân lý của chính nó.

Ta có thể xây một hệ thống lớn hơn.

Rồi lớn hơn nữa.

Nhưng đường chân trời lại lùi ra xa.

Có lẽ toán học không phải một căn phòng cuối cùng mà con người một ngày nào đó sẽ khóa cửa rồi tuyên bố:

Xong rồi.

Nó giống một vùng đất hơn.

Mỗi khi leo lên một ngọn núi, ta nhìn thấy thêm những ngọn núi khác.

Và ở cuối tầm mắt luôn có một đường mỏng màu xanh.

Không phải vì chúng ta chưa đi đủ xa.

Mà vì đường chân trời là thứ xuất hiện mỗi khi ta có một nơi để đứng.

Tham khảo

Stanford Encyclopedia of Philosophy, Gödel’s Incompleteness Theorems. (Stanford Encyclopedia of Philosophy)
Stanford Encyclopedia of Philosophy, Kurt Gödel. (Stanford Encyclopedia of Philosophy)
Stanford Encyclopedia of Philosophy, Gödel Numbering. (Stanford Encyclopedia of Philosophy)
Stanford Encyclopedia of Philosophy, Non-Deductive Methods in Mathematics. (Stanford Encyclopedia of Philosophy)
Stanford Encyclopedia of Philosophy, Independence and Large Cardinals. (Stanford Encyclopedia of Philosophy)
Kurt Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, 1931.

Gödel: Khi toán học phát hiện ra có những sự thật mà chính nó không thể chứng minh