Số học Peano là đủ, vì số học Peano có thể mã hóa việc tính toán

• Số học Peano (PA) có thể biểu diễn quá trình tính toán mang tính cơ học, nên trong PA có thể chứng minh sự kết thúc của mọi dãy Goodstein đơn lẻ
• Thông qua dạng chuẩn Cantor và ký pháp cơ số di truyền, có thể biểu diễn dãy Goodstein và tính chất giảm dần của chúng, nhờ đó có thể xây dựng các chứng minh có độ dài hữu hạn
• Thông qua quy nạp (quy nạp mạnh/quy nạp siêu hạn), có thể mở rộng chứng minh tương ứng đến các số thứ tự ở bậc nhất định
• PA có thể chứng minh rằng với mọi số tự nhiên n, “G(n) đạt đến 0”, nhưng không thể đưa ra chứng minh tổng quát cho toàn bộ định lý Goodstein (với mọi n)
• Chỉ với PA cũng có thể hiện thực đầy đủ việc mã hóa tính toán, cấu trúc dữ liệu (List, Pair, v.v.), thậm chí cả bản thân ngôn ngữ lập trình (Lisp) và cả quá trình chứng minh của chính nó

---

Giới thiệu và bối cảnh vấn đề

• Bài viết này mô tả rằng số học Peano (PA) có thể chứng minh “với từng n, dãy Goodstein đạt đến 0 (G(n) terminates)”
• Điều này có thể là hiển nhiên với các nhà logic học, nhưng được giải thích từ góc nhìn mã hóa tính toán để lập trình viên có thể hiểu
• Với từng trường hợp của dãy Goodstein, có thể xây dựng một quy trình chứng minh cụ thể bên trong PA

Ordinals (số thứ tự) và dãy Goodstein

• Tạo số thứ tự (Sets as Ordinals) theo cách của Von Neumann
  • 0 là tập rỗng, 1 là {0}, 2 là {0,1}, ω là {0,1,2,…}, ω+1 là {0,1,2,…,ω}, v.v., với thứ tự được xác định rõ ràng
• Dãy Goodstein được mô tả bằng ký pháp cơ số di truyền dùng dạng chuẩn Cantor
  • Ví dụ: ω^ω là ((1,ω)), tức ((1,(1,1)))
  • Thứ tự < được xác định bằng so sánh từ điển theo số thứ tự/hệ số của từng hạng

Quy nạp và quy nạp siêu hạn (Transfinite Induction)

• Nguyên lý quy nạp của số học Peano: đúng với 0, và nếu đúng từ n→n+1 thì đúng với toàn bộ số tự nhiên
• Quy nạp mạnh cũng có thể được chứng minh trong PA
• Quy nạp siêu hạn (Transfinite induction): trong ZFC v.v. có thể mở rộng đến các số thứ tự vô hạn, và áp dụng cho các số được viết dưới dạng chuẩn Cantor
  • Định lý 1: mọi dãy giảm viết trong dạng chuẩn Cantor đều luôn hữu hạn
  • Định lý 2: có thể dùng quy nạp siêu hạn cho các số ở dạng chuẩn Cantor

Quy nạp siêu hạn trong PA và độ dài chứng minh của dãy Goodstein

• PA có thể tạo ra chứng minh về sự kết thúc của dãy Goodstein cho một n bất kỳ
  • Có thể xây dựng chứng minh theo chiều cao tháp của dạng chuẩn Cantor là m=O(log* n) (iterated log)
  • Ở mỗi bước, kết hợp m lần chứng minh để có độ dài chứng minh tổng thể là O(m^2), hoặc rút xuống O(m log m) nếu đưa vào ký pháp đặc biệt (ω[m])
• Tuy nhiên, trong PA không thể chứng minh toàn bộ định lý Goodstein (cho mọi n) (không thể quy nạp siêu hạn đến ε0)
  • Nếu làm được thì cũng có thể chứng minh tính nhất quán của PA, mâu thuẫn với bất toàn thứ hai của Gödel

Mã hóa chương trình và cấu trúc dữ liệu trong PA

• PA có thể mã hóa đầy đủ tính toán/chương trình/cấu trúc dữ liệu (số, cặp, danh sách và mọi cấu trúc khác)
• Có thể hiện thực nhiều chức năng theo các cách như sau:
  • Logic và phép toán cơ bản (+, *, pow, //, %, min, max, v.v.)
  • So khớp mẫu và rẽ nhánh điều kiện (if, cond, v.v.)
  • Mã hóa một số thành hai số (cặp), hoặc từ cặp mở rộng lặp lại thành các cấu trúc phức tạp hơn như danh sách, v.v. (danh sách đệ quy, cây, văn bản, v.v.)
• Nhờ việc mã hóa các cấu trúc dữ liệu này, có thể xây dựng cả trình thông dịch cho một máy ảo/ngôn ngữ lập trình bất kỳ (như Lisp)

Bootstrap sang Lisp và mã hóa

• Lấy Lisp làm ví dụ để giải thích cách hiện thực các phép toán số và logic cơ bản, cấu trúc dữ liệu, cùng bộ diễn giải/thông dịch ngôn ngữ lập trình
• Toàn bộ cấu trúc của Lisp (ánh xạ lệnh/đối số, special form, macro, v.v.) đều có thể được hiện thực trong PA bằng tổ hợp các hàm thích hợp
• Xa hơn nữa, ngay trong PA cũng có thể mã hóa và hiện thực chính quá trình chứng minh của PA, thủ tục chứng minh logic, và các cấu trúc tự quy chiếu dưới dạng ký hiệu

Mã hóa chính logic bên trong PA

• Trong logic toán học, có thể mã hóa quá trình chứng minh của logic bậc nhất (First-Order Logic) thành dữ liệu số trong PA
• Mỗi bước chứng minh/mệnh đề/quy tắc suy luận/kiểm tra tính hợp lệ của chứng minh đều được nhận diện và xử lý như một chuỗi hàm số/thao tác trên danh sách
• Kiểu mã hóa siêu mức và tự quy chiếu này dẫn đến các chứng minh về bất toàn của Gödel và bài toán dừng

Kết luận

• Ngay trong PA, có thể mã hóa, chứng minh và diễn giải đầy đủ tính toán, cấu trúc dữ liệu, chương trình, cho đến cả quá trình chứng minh logic
• Vì vậy, mọi dãy Goodstein cụ thể (với n cho trước, G(n) kết thúc) đều có thể được chứng minh cụ thể bên trong PA
• Tuy nhiên, một chứng minh kiểu “PA chứng minh định lý Goodstein trong chính PA” cho toàn bộ định lý Goodstein (mọi n) là điều bất khả do các giới hạn của logic
• Từ góc nhìn của lập trình viên, PA là một nền tảng logic hoàn chỉnh có thể mã hóa chính việc tính toán

[GN⁺]

Ý kiến Hacker News

• Đây là bản blog được viết lại từ câu hỏi tôi từng đăng trên Stack Overflow; có giải thích về giới hạn của những gì có thể chứng minh trong hệ tiên đề Peano và cách bootstrap Lisp bên trong hệ tiên đề Peano; phần đùa cợt chủ yếu nằm ở mục thứ hai; rất hoan nghênh các chỉnh sửa hoặc câu hỏi bổ sung
  • Trong lúc đọc bài này, tôi phát hiện ở mục "Why Lisp?" có một chỗ ngoặc không khớp (xem ví dụ (defun not (x) (if x false true)). Hễ ai đó bắt đầu dùng ngoặc là tôi theo bản năng sẽ kiểm tra xem chúng đã được đóng đúng chưa. Sau đó đọc đến đoạn nói rằng "thật dễ để lập trình máy tính kiểm tra xem ngoặc có cân bằng hay không" thì tôi cười lớn. Kiểu đùa này thực sự rất vui, và ở mục "Basic Number Theory", câu ; After a while, you stop noticing that stack of closing parens. cũng rất ấn tượng. Lâu rồi tôi mới lại đụng tới Lisp, và bài viết thật sự rất thú vị
  • Bài này thực sự rất hấp dẫn. Tôi mới chỉ đọc phần mở đầu, nhưng việc trong hệ tiên đề Peano (PA) có thể chứng minh rằng mọi trường hợp cụ thể của dãy Goodstein đều đi đến 0, nhưng không thể chứng minh rằng mọi trường hợp đều đi đến 0, là một điều rất thú vị (thực ra là kết quả khá hiển nhiên, nhưng vẫn cực kỳ cuốn hút). Và việc chỉ với hệ tiên đề Peano cũng có thể mã hóa tính toán thì thật sự kỳ lạ (xét về nguyên lý thì cũng hợp lý thôi, nhưng trước đây tôi chưa từng nghĩ thêm một tầng tự tham chiếu như vậy). Gần đây tôi cũng đang muốn học sâu hơn về lý thuyết tập hợp, và vừa học đến phần dãy Goodstein trong giáo trình Intro to Set Theory. Nếu ai có thể gợi ý giáo trình lý thuyết tập hợp nâng cao hoặc sách đào sâu về số học Peano thì tôi rất cảm kích. Mục tiêu nhỏ của tôi là hiểu vì sao PA không đủ để chứng minh định lý Goodstein, nhưng nếu có hướng đi khác đáng khuyên thì tôi cũng rất sẵn lòng
  • Có hai chỗ viết omega trong bài mà tác giả quên ghi thành \omega
• Rất giống với lý thuyết Boyer-Moore. Lý thuyết này xây dựng toán học ở mức của hệ tiên đề Peano. Boyer và Moore đã phát triển một bộ chứng minh định lý tự động hiện thực hóa lý thuyết này, và họ cũng có một bản sao chạy bằng GNU Common LISP. Các liên kết tới bài báo "A Computational Logic" và bản triển khai nqthm đều đáng xem. Điều gây ấn tượng trong bài báo là ví dụ cho thấy khi bắt đầu từ các tiên đề Peano thì các định lý phức tạp như phép nhân các số nguyên tố là khó, nhưng các tính chất như giao hoán của phép cộng, phân phối của phép nhân, hay các định lý liên quan đến hàm GCD thì hoàn toàn có thể chứng minh được
• Tôi có nền tảng cả toán lẫn lập trình, và cá nhân tôi thấy phần độc lập của định lý Goodstein còn thú vị hơn ở chỗ nó có thể được “lách qua” theo kiểu tự quy chiếu. Tôi đoán rằng nếu thêm giả thiết PA+"PA là omega-consistent" thì có lẽ có thể chứng minh định lý Goodstein, và như vậy cũng có thể làm được quy nạp siêu hạn (transfinite induction) tới epsilon_0. EDIT: Có lẽ chỉ cần "PA là nhất quán" thôi cũng đã đủ?
  • Tiếc là không phải vậy. Và không chỉ Con(PA), mà ngay cả bất kỳ công thức được lượng hóa phổ quát nào cũng không đủ. Xem câu trả lời trên Math StackExchange có liên quan. Liên quan đến câu hỏi đầu tiên, tôi tò mò không biết người ta mã hóa tính omega-consistency như một công thức của PA thế nào; tôi không nghĩ ra ngay nên thấy khá hứng thú
  • Tôi là người đặt câu hỏi trên Stack Overflow. Tôi đã thêm liên kết tới một số câu trả lời vào đó. Về bản chất, chỉ riêng "PA là nhất quán" thì không đủ, nhưng một dạng "nguyên lý phản chiếu đồng nhất" kiểu "nếu chứng minh được trong PA thì là đúng" thì đủ. Tôi không dám chắc nguyên lý này hoàn toàn giống với omega-consistency, nhưng theo giải thích trên Wikipedia thì có vẻ như vậy. Nếu T là omega-consistent thì điều đó có nghĩa là "T + RFN_T + tập mọi công thức đúng là nhất quán", và điều này được diễn giải tương đương với việc "T + RFN_T là đúng"
  • Tôi cũng thích cấu trúc quy nạp (đệ quy) kiểu này. Rốt cuộc ta tạo ra một siêu-chứng minh về việc PA chứng minh điều gì, và nếu đã tin PA thì có thể tin luôn siêu-chứng minh đó. Riêng đoạn chỉ cần "PA là nhất quán" thì tôi chưa thật sự hiểu chắc. Theo tôi, PA+"PA nhất quán" có vẻ vẫn cho phép tồn tại một mô hình trong đó định lý Goodstein đúng trên phạm vi các số tự nhiên chuẩn, đồng thời cũng có một mô hình trong đó định lý Goodstein sai với một số nguyên phi chuẩn nào đó N. Tôi nghĩ mệnh đề mạnh hơn là omega-consistency sẽ loại được kiểu trường hợp như vậy
  • Bài đăng trên Math Exchange nói rằng chứng minh PA+quy nạp siêu hạn (epsilon_0) sẽ chứng minh chính PA. Tôi nghĩ rằng với PA+"PA nhất quán" thì có thể chứng minh được quy nạp siêu hạn tới epsilon_0
  • Giờ có lẽ chủ đề này đã vượt quá mức chi tiết mà tôi thấy mình có thể phát biểu thoải mái. Theo ChatGPT thì chỉ riêng "PA+PA nhất quán" là không đủ. ChatGPT chắc đã tiêu hóa rất nhiều sách logic, nên nếu nó nói vậy thì có vẻ cũng đáng tin
• Bình luận tôi viết cho JoJoModding trên Stack Overflow là không đúng. Tôi đã nói rằng "vì trong các mô hình PA phi chuẩn có các số tự nhiên vô hạn nên dù PA chứng minh được rằng nó tạo ra một chứng minh nào đó, nó vẫn không chứng minh được rằng chứng minh ấy có độ dài hữu hạn"; nhưng thực ra nếu PA chứng minh rằng "PA đã chứng minh X" thì PA cũng chứng minh được chính X. Điểm quan trọng không phải là sự tồn tại của mô hình phi chuẩn, mà là việc mô hình số tự nhiên chuẩn là một mô hình của PA. Vì vậy, nếu "PA chứng minh rằng nó chứng minh X" thì trên thực tế sẽ sinh ra một chứng minh tương ứng với một số tự nhiên hữu hạn chuẩn, và từ số này có thể dựng ra bên trong PA một chứng minh thực sự của X
  • Tôi chưa có thời gian xem kỹ lại logic, nhưng ở mức ngôn ngữ tự nhiên thì có vẻ mấu chốt là sự khác nhau giữa "PA chứng minh forall n, G(n)" và "PA chứng minh forall n, Provable(G(n))". Tôi không mạnh về logic, nên nếu ai có thể giải thích cụ thể vì sao từ việc chứng minh forall n, Provable(P(n)) lại không thể suy ra chứng minh Provable(forall n, P(n)) thì tôi rất cảm ơn
  • Mệnh đề "nếu PA chứng minh rằng 'PA chứng minh X' thì PA chứng minh X" là không đúng. Trong PA ta có thể xây dựng một hàm tìm kiếm mọi chứng minh khả dĩ, và thực ra ở phần cuối câu trả lời tôi đã phác thảo cách này. Từ đó cũng có thể xây dựng các hàm như will-return, opposite-return, và điều này trùng với chứng minh chuẩn của bài toán dừng. Hãy xét trường hợp opposite-return(opposite-return, opposite-return): nếu PA chứng minh rằng opposite-return sẽ trả về, thì nó cũng chứng minh rằng thực ra nó sẽ không trả về; ngược lại, nếu PA chứng minh rằng nó sẽ không trả về, thì lại chứng minh rằng nó sẽ trả về. Nếu PA chấp nhận mệnh đề mạnh hơn kiểu "mọi thứ có thể chứng minh đều thực sự chứng minh được", thì đó chính là định lý bất toàn thứ hai của Gödel, nghĩa là PA sẽ mâu thuẫn. Vì vậy nhất định phải phân biệt giữa "PA chứng minh" và "PA chứng minh rằng nó chứng minh"
• Chỉ riêng phép tính lambda thuần túy cũng đã đủ, vì bản thân phép tính lambda đã có thể mã hóa tính toán
• Khi nói chuyện với ai đó về kiểu dữ liệu quy nạp, tôi đã cho họ xem định nghĩa Nat được tạo bằng zero/succ (như trong Lean hay Rocq). Người đó thắc mắc như "Chỉ thế này là đủ sao?", "Có cần hệ tiên đề Peano không? Có thứ gì còn nguyên thủy hơn kiểu dữ liệu quy nạp không?". Điều đó khiến tôi nghĩ rằng ta nên thường xuyên tự nhắc mình đừng xem hệ tiên đề Peano là thứ hiển nhiên về bản chất, mà chỉ là một lựa chọn thiết kế
  • Để trả lời câu hỏi "Có gì căn bản hơn kiểu dữ liệu quy nạp không?", tôi cho rằng bản thân số tự nhiên còn nguyên thủy hơn kiểu dữ liệu quy nạp. Mọi kiểu dữ liệu quy nạp đều có thể được tạo ra chỉ từ số tự nhiên và một vài bộ tạo kiểu nguyên thủy khác (Π, Σ, =, Ω)
• Xem Q&A về định lý Kirby-Paris
• Chia sẻ một video về việc tính nhất quán của PA là thứ có thể chứng minh bên trong PA liên kết YouTube
  • Đây là phần bắt buộc phải giải thích với những người không chuyên về logic. Theo định lý bất toàn thứ hai của Gödel, nếu PA có thể chứng minh tính nhất quán của chính nó thì PA sẽ trở thành mâu thuẫn (và có thể chứng minh bất cứ thứ gì, kể cả điều sai). Video này không chứng minh rằng PA là mâu thuẫn, mà chỉ cho thấy rằng theo một nghĩa yếu hơn, PA có thể "chứng minh tính nhất quán của chính nó". Nếu không biết nền tảng logic thì khó mà hiểu thật chính xác, nhưng vẫn đủ sức gây hứng thú
• Chủ đề này được 123 điểm, trong khi bài gốc trên SO lại chỉ có 11 upvote
  • Trên Stack Overflow phải có 15 điểm mới được upvote. Vì vấn đề reputation nên mọi người cũng không muốn đăng bài, và có vẻ giới hạn 15 điểm này đang cản việc upvote
• Chỉ riêng computation có đủ không? Các số thực tính được chỉ là một tập con của toàn bộ số thực
  • Tôi nghĩ ngay chính tên gọi "số thực" đã là một cách đặt tên dễ gây hiểu lầm. Có thể hiểu số thực là các tỷ lệ vật lý thực tế. Ví dụ, nói 180.255 pound thì đó là tỷ lệ vật lý thực giữa cân nặng thực của Jones và đơn vị pound chuẩn. Những tỷ lệ như vậy cũng tồn tại về mặt vật lý, tức là số thực có thể được hiểu như các tỷ lệ vật lý. Trong khi đó hiện nay quan điểm phổ biến là xem con số như khái niệm trừu tượng tách khỏi hiện thực, tiêu biểu là lập trường kiểu Platon. Nhưng trong thực tế, không thể đo lường hay biểu diễn cái gì với độ chính xác vô hạn. Chẳng hạn, đo với độ chính xác quá 50 chữ số là bất khả thi do giới hạn của cơ học lượng tử. Nếu muốn đo quỹ đạo các thiên thể trong Hệ Mặt Trời không sai số thì quá 50 chữ số sẽ phải tính đến ảnh hưởng khối lượng từ các sao lân cận, quá 100 chữ số thì phải mô hình hóa cả thiên hà, và cuối cùng còn phải xét đến những ảnh hưởng vật lý không thể đo đạc được. Vì thế trong thực tế chỉ có toán học với độ chính xác hữu hạn là khả thi. Tức là về nguyên tắc mọi thứ đều tính được, nhưng khi đi tới vô hạn thì bản thân mô hình toán học cũng trở nên vô nghĩa
  • Có thật vậy không? Thực ra ý niệm rằng cái không đếm được (uncountable) là “nhiều hơn” bắt nguồn từ một sự hiểu lầm. Xem bài giải thích của tôi. Nếu chấp nhận rằng cái không đếm được là nhiều hơn thì buộc phải chọn một lập trường gây tranh cãi về "sự tồn tại". Xem thảo luận liên quan. Cuối cùng, dù ta đẩy lập luận logic đi xa đến đâu thì mọi thứ vẫn đều có thể được biểu diễn bằng máy tính. Ngay cả khi thêm các tập lớn vào ZFC thì vẫn có thể xuất phát từ PA và suy luận tới mọi kết luận tùy ý, nên trên thực tế tôi cho rằng chỉ PA là đủ. Nếu cần thêm thuyết phục thì tôi khuyên đọc Gödel, Escher, Bach
  • Cách nhìn của tôi hơi khác. Các số thực nói chung không thể được xử lý dưới bất kỳ hình thức nào như tính toán, ký hiệu hóa hay ghi chép, nhưng các ‘mệnh đề’ về số thực thì bản thân chúng lại thường có thể được biểu diễn và tính toán một cách hữu ích. Những nỗ lực như của Harvey Friedman hay tác giả bài viết này, dùng những hệ đơn giản để tạo ra các giá trị phức tạp vượt xa trực giác, thật sự rất hấp dẫn. (Lưu ý: website audiomulch không truy cập được)
  • Nếu không gắn "đủ" với một mục tiêu cụ thể nào thì câu hỏi này mơ hồ về mặt định nghĩa. Điều quan trọng là đủ cho việc gì
  • Tôi nghĩ ngay chính câu hỏi "Chỉ riêng computation có đủ không?" là sai. Hiển nhiên là không đủ; nếu đủ thì một số người vốn xem thực tại như một cỗ máy đồng hồ dễ hiểu đã đúng hết rồi. Thực tại thú vị và phức tạp hơn nhiều