Tính nhất quán của New Foundations – Chứng minh toán học hóc búa được kiểm chứng bằng Lean

 (leanprover-community.github.io)
1 điểm bởi GN⁺ 2024-04-24 | 1 bình luận | Chia sẻ qua WhatsApp
  • Phần khó trong chứng minh tính nhất quán của lý thuyết tập hợp New Foundations do Quine đề xuất năm 1937 đã được kiểm chứng bằng Lean, và định lý cốt lõi được trình bày trong ConNF/Model/Result.lean
  • Cách tiếp cận là dùng kết quả rằng tính nhất quán của New Foundations và Tangled Type Theory(TTT) là tương đương, rồi xây dựng hình thức một mô hình TTT trong Lean
  • Việc xây dựng mô hình TTT trở nên khó vì tính ngoại diên đòi hỏi các tập hợp phải được xác định duy nhất bởi các phần tử thuộc kiểu thấp hơn
  • Việc xây dựng mô hình sử dụng kiểu cơ sở, t-set, các hoán vị cho phép, support nhỏ và preferred extension; để kiểm soát kích thước kiểu bằng μ cần đến freedom of action theorem
  • Kernel của Lean kiểm tra chứng minh đã hình thức hóa, nhưng không đảm bảo mệnh đề hình thức khớp với ý nghĩa tiếng Anh dự định, nên cần rà soát phần diễn dịch khi diễn giải kết quả

Hoàn tất kiểm chứng tính nhất quán của New Foundations bằng Lean

  • Năm 1937, Quine đề xuất lý thuyết tập hợp New Foundations, và Randall Holmes từ năm 2010 đã tuyên bố rằng ông có chứng minh về tính nhất quán của nó
  • Dự án này tập trung vào việc kiểm chứng bằng trình chứng minh định lý tương tác Lean phần khó trong chứng minh của Holmes, nhằm chỉ ra tính nhất quán của New Foundations
  • Chứng minh đã hoàn tất và mệnh đề định lý có thể xem trong ConNF/Model/Result.lean
  • Các tài liệu liên quan cũng được cung cấp kèm theo

Chạy mã trên máy cục bộ

  • Để chạy cục bộ, hãy cài elan, clone repository rồi chạy lệnh sau ở thư mục gốc của repository
lake exe cache get
  • Sau đó có thể xem mã trong trình soạn thảo như Visual Studio Code, và biên dịch trực tiếp từ dòng lệnh bằng lake build

Mối liên hệ giữa New Foundations và TTT

  • New Foundations được biết là nhất quán khi và chỉ khi Tangled Type Theory(TTT) nhất quán
  • Dự án đã xây dựng hình thức một mô hình TTT trong Lean, và từ đó thu được kết luận trên giấy về tính nhất quán của New Foundations, tức Con(NF)
  • Công việc dựa trên nhiều tài liệu chứng minh của Holmes, nhưng cần rất nhiều thay đổi và bổ sung để phù hợp với lý thuyết kiểu của Lean

Nền tảng của kiểm chứng bằng Lean và lưu ý khi diễn giải

  • Dự án phụ thuộc vào mathlib, thư viện toán học cộng đồng viết bằng Lean
  • Nhờ mathlib, các kết quả quen thuộc như cardinal và group có thể được sử dụng mà không cần chứng minh lại trong dự án
  • Các định nghĩa và định lý của mathlib cũng như của dự án này được trusted kernel của Lean kiểm tra
    • Kernel của Lean kiểm chứng bằng tính toán rằng chứng minh đã xây dựng thực sự đúng
  • Tuy nhiên, Lean không thể kiểm tra đến mức mệnh đề hình thức có khớp với câu tương đương tiếng Anh dự định hay không
    • Khi rút ra kết luận từ mã, cần xem xét cẩn thận phần dịch giữa mô tả tiếng Anh và mệnh đề hình thức

Cấu trúc và khó khăn của Tangled Type Theory

  • TTT là một lý thuyết tập hợp đa sort với dấu bằng = và quan hệ thuộc ∈
  • Sort được đánh chỉ mục bởi ordinal giới hạn λ, và các phần tử của λ được gọi là chỉ số kiểu
  • Điều kiện hình thành biểu thức bị giới hạn bởi kiểu
    • x = y được hình thành đúng khi x và y có cùng kiểu
    • x ∈ y được hình thành đúng khi kiểu của x thấp hơn kiểu của y
  • Khó khăn cốt lõi đến từ tiên đề tính ngoại diên của TTT
    • Một tập hợp thuộc kiểu α phải được xác định duy nhất bởi các phần tử thuộc kiểu β < α bất kỳ
    • Ví dụ, nếu hai tập hợp thuộc kiểu α khác nhau, thì với mọi β < α chúng phải có các phần tử thuộc kiểu β khác nhau
  • Yêu cầu này khiến việc xây dựng mô hình TTT phức tạp hơn so với xây dựng mô hình lý thuyết tập hợp đơn giản

Các bước chính trong xây dựng mô hình

  • Xây dựng kiểu cơ sở

    • Đặt λ là ordinal giới hạn, κ > λ là ordinal chính quy, và μ > κ là cardinal giới hạn mạnh có đối đồng điều ít nhất là κ
    • Một tập hợp có kích thước nhỏ hơn κ được gọi là small
    • Trước tiên xây dựng base type ở level -1, là kiểu phụ trợ nằm dưới mọi kiểu của mô hình
    • Các phần tử của kiểu này được gọi là atoms, nhưng không phải atom theo nghĩa của ZFU hay NFU
    • Có μ atom, được phân hoạch thành các litters có kích thước κ

  • t-set và các hoán vị cho phép

    • Ở mỗi level kiểu α, tạo ra các collection sẽ trở thành phần tử của mô hình TTT, gọi là t-set
    • Đồng thời xây dựng allowable permutations, là nhóm hoán vị tác động lên t-set
    • Quan hệ thuộc được bảo toàn dưới tác động của allowable permutations
    • Mỗi t-set được quy định là có support đối với tác động của allowable permutations
    • support là một tập nhỏ gồm các đối tượng gọi là addresses
    • Nếu một allowable permutation cố định mọi phần tử của support thì nó cũng cố định t-set đó

  • Khớp tính ngoại diên bằng preferred extension

    • Mỗi t-set ở level α có một preferred extension thuộc một kiểu nào đó β < α
    • Có thể khôi phục extension được ưu tiên từ các phần tử của t-set, và extension của các kiểu thấp hơn khác được suy ra từ β-extension đó
    • Cấu trúc này được dùng để thỏa mãn tiên đề tính ngoại diên của TTT

  • Kiểm soát kích thước kiểu

    • Mỗi kiểu α chỉ có thể được xây dựng khi có các giả định như kích thước của mọi kiểu β < α đều đúng bằng μ
    • Việc chứng minh collection t-set ở level α có kích thước ít nhất μ là dễ, nên cần chứng minh rằng nó có không quá μ phần tử
    • Để làm vậy, chứng minh rằng không có quá nhiều mô tả khác nhau một cách cơ bản của các tangles dưới tác động của allowable permutations
    • Bước này cần freedom of action theorem, một bổ đề kỹ thuật cho phép xây dựng allowable permutations
    • Kết quả chính của phần này nằm trong ConNF.mk_tSet

  • Hoàn tất quy nạp và kiểm tra tiên đề

    • Thực hiện đệ quy quy trình trên để tạo kiểu của các tangles ở mọi level kiểu α
    • Đây là bước dễ trong lý thuyết tập hợp, nhưng trong lý thuyết kiểu thì cần nhiều công sức vì nhiều giả định quy nạp cần thiết đan xen với nhau
    • Sau đó kiểm tra cấu trúc thu được có thỏa mãn hữu hạn tiên đề hóa của lý thuyết hay không, nhằm xác nhận đó là một mô hình của TTT
    • Dự án sử dụng việc chuyển đổi hữu hạn tiên đề hóa của Hailperin cho NF comprehension scheme thành hữu hạn tiên đề hóa của TTT
    • Tệp kết quả nằm trong results file
    • Lựa chọn này mang tính tùy ý; với hạ tầng đã xây dựng, cũng có thể dễ dàng chứng minh các hữu hạn tiên đề hóa khác

Bài viết liên quan

1 bình luận

 
GN⁺ 2024-04-24
Ý kiến trên Hacker News

  • Tôi cho rằng rủi ro một chứng minh viết bằng Lean bị sai là rất nhỏ
    Tuy vậy, ngoài lỗi của Lean, vẫn có một rủi ro đã được biết rõ cả trong kiểm chứng phần mềm lẫn toán học: cần đọc chính xác kết luận để xác nhận rằng mệnh đề thực sự cần thiết đã được chứng minh
    Tôi đã đọc kỹ kết luận cuối cùng của Wilshaw và cho rằng nó thực sự chứng minh đúng điều cần phải chứng minh

    • Bài báo cũng nói điều tương tự: mọi định nghĩa và định lý trong mathlib và trong dự án này đều đã được trusted kernel của Lean kiểm tra, và chứng minh mà chúng ta xây dựng đã được xác minh về mặt tính toán là thực sự đúng
      Tuy nhiên, Lean không thể kiểm tra liệu các mệnh đề của định nghĩa và định lý có khớp với diễn đạt tiếng Anh mà người ta dự định hay không, nên khi rút ra kết luận từ mã của dự án này cần cẩn thận với việc chuyển dịch sang tiếng Anh

    • Vấn đề tôi nói đến cũng liên quan đến lo ngại về thư viện: khi dùng một khái niệm đã được định nghĩa, cần chắc chắn rằng định nghĩa đó là đúng, tức là điều thực sự cần thiết đã được chứng minh
      Hình thức hóa của Wilshaw có dùng thư viện, nhưng không dễ bị phản biện này. Điều được chứng minh là một khái niệm đã định nghĩa nào đó thỏa mãn một nhóm công thức logic bậc nhất cụ thể, và nếu có một vị từ thỏa các công thức đó thì NF là nhất quán

    • Một rủi ro khác là lỗi của chính Lean. Đây cũng không phải chuyện chưa từng có với theorem prover 1
      Có thể khó vô tình đụng phải, nhưng những cộng tác quy mô lớn nơi người bất kỳ điền vào từng bước như 3 đang ngày càng phát triển. Tình huống ai đó cố tình phá bằng cách lợi dụng một lỗi mình phát hiện ra để điền vào một bước nào đó có thể sẽ trở thành điều đáng lo

    • Từ góc nhìn nền tảng học, điều quan trọng là chứng minh này cũng là một chứng minh về equiconsistency giữa NF và kernel của Lean. Bản thân kernel của Lean được con người rà soát
      Theorem prover cơ giới hóa vận hành theo cách bảo toàn mức độ đúng đắn đã được đưa vào từ con người hoặc từ các hệ thống bên ngoài khác

  • Nếu tôi không nhầm, đây có vẻ là trường hợp đầu tiên mà proof assistant được dùng để chốt lại vị thế của một chứng minh khó vốn ở trong trạng thái mơ hồ suốt nhiều năm
    Trước đây đã có các dự án kiểm chứng những chứng minh sẵn có mà phần tính toán lớn do phần mềm không đáng tin đảm nhiệm, như định lý bốn màu trong Coq, nhưng có lẽ đây là lần đầu tiên mà ngay cả địa vị nhận thức luận của kết quả trong cộng đồng toán học rộng hơn cũng còn bất định

  • Có ai có thể giải thích sơ bộ điều gì là đặc biệt hoặc mới mẻ ở cách hình thức hóa lý thuyết tập hợp “New Foundations” so với các cách hình thức hóa khác không?
    Hoặc nếu có thì một đường link giải thích phù hợp cho sinh viên đại học toán hoặc người làm kỹ thuật cũng được

    • Tôi vừa sửa bài Wikipedia, giờ chắc sẽ dễ đọc hơn: https://en.wikipedia.org/wiki/New_Foundations
      Theo tôi, điểm cốt lõi là sự tồn tại của tập hợp phổ quát. Trong hệ thống kiểu của ngôn ngữ lập trình, loại tập hợp phổ quát này rất hữu ích cho trường hợp sử dụng của tôi
      Các cách lách như vũ trụ tích lũy của các hệ hiện có hoặc type-in-type đều không làm tôi hài lòng. Thay vào đó, ta chỉ cần kiểm tra xem chữ ký kiểu có được phân tầng hay không, rồi có thể quên luôn chuyện kiểu có các mức số
    • Điều tôi thực sự thích về mặt thẩm mỹ ở NF là cách nó điều chỉnh tiên đề chọn tập con để “tập hợp của mọi tập hợp” không gây ra nghịch lý Russell
      Về cơ bản, nó yêu cầu vị từ dùng để chọn tập con phải tuân theo một hệ kiểu rất nhẹ. “x không là phần tử của chính nó” không phải là một câu hỏi được định kiểu hợp lệ trong một hệ kiểu hợp lý, và đặc biệt cũng không thỏa yêu cầu “có thể phân tầng” của NF, nên không thể tạo ra tập hợp nghịch lý Russell gồm mọi tập hợp không chứa chính nó
    • Một điểm “hay” của NF là nó chỉ có hai tiên đề/lược đồ tiên đề: 1) các tập hợp có cùng phần tử thì bằng nhau, 2) với mọi tính chất có thể phân tầng thì tồn tại tập hợp gồm mọi thứ có tính chất đó
      Định nghĩa của “có thể phân tầng” cũng không quá phức tạp. Trong khi đó, ZF có tám tiên đề/lược đồ tiên đề trông khá chắp vá

  • Tôi tìm đến bài này vì tò mò không biết khác biệt nền tảng giữa Coq và Lean là gì, liệu chúng có chạy trên cùng một loại logic hay không 1
    Tôi hầu như không hiểu được cuộc thảo luận đó và cũng không thực sự dùng cả hai. Nếu có thể giải thích thêm hoặc so sánh với các proof assistant khác thì tôi rất muốn nghe

    1 https://proofassistants.stackexchange.com/questions/153/what...

  • Có vẻ những người ủng hộ Lean đôi khi dùng cách diễn đạt hơi quá đà. Lean không phải là phương pháp chứng minh ưu việt hơn như người ta hay ngầm hiểu, mà là một cách chứng minh thay thế
    Nếu thử học Lean, bạn sẽ sớm nhận ra nó là một ngôn ngữ lập trình và hệ thống vốn cũng có bug, đồng thời phụ thuộc rất nhiều vào các tầng thư viện do những con người khác viết. Những thư viện đó có chứa các lựa chọn thiết kế, và cũng có thể có lỗ hổng hoặc bug
    Vì thế, tôi không hoàn toàn đồng ý với kiểu diễn đạt như “Lean nói rằng chứng minh đó là đúng”. Cách nói chính xác và trung thực hơn, theo tôi, là các nhà toán học đã kiểm chứng chứng minh được viết ra, rồi con người dịch chứng minh đó sang Lean và nó cũng được kiểm chứng ở đó. Nói như thể Lean cung cấp sự xác minh vàng duy nhất thì không hẳn chính xác, hoặc ít nhất tôi chưa thấy lời giải thích nào cho điều đó. Phụ đề “số hóa chứng minh của Randall Holmes” có lẽ là cách diễn đạt chính xác nhất

    • Tôi cho rằng chứng minh được máy kiểm chứng trong một hệ thống mạnh như Lean vượt trội hơn rất nhiều so với chứng minh chỉ do con người kiểm tra. Con người thật đáng kinh ngạc, nhưng cũng chán nản và dễ bỏ sót chi tiết
      Đây không chỉ là một khẳng định mang tính lý thuyết. Phải mất hơn 2.000 năm con người mới nhận ra Elements của Euclid thiếu một tiên đề. Đó là một sai sót cơ bản đến mức một hệ thống kiểm tra chứng minh bằng máy hoạt động đúng sẽ làm lộ ra ngay lập tức
      Nhiều chứng minh toán học đã được xuất bản cũng về sau bị phát hiện là sai. Khi toán học ngày càng tinh vi hơn, con người càng khó kiểm tra đúng mọi bước. Máy móc hiện vẫn chưa giỏi tạo ra chứng minh như con người, nhưng về mặt kiểm chứng thì không gì sánh bằng
      Cũng có những hệ thống “cạnh tranh” với Lean nên tôi sẽ không nói Lean là “con đường chân chính duy nhất”. Ví dụ, tôi cũng thích Metamath. Tuy vậy, chữ “cạnh tranh” giữa các hệ thống này cần được đặt trong ngoặc kép. Mỗi hệ thống có ưu và nhược điểm riêng, và có nhiều người thích, dùng hoặc đóng góp cho nhiều hệ thống cùng lúc. Tất cả đều có thể kiểm chứng định lý với mức độ chặt chẽ mà con người không thể thực tế đạt được

    • Có thể có bug, nhưng theo hiểu biết của tôi thì thứ cần được tin cậy chỉ là kernel
      Nếu “các tầng thư viện do những con người khác viết” ở đây là nói đến mathlib, thì có vẻ nhận định đó không đúng. Mã của mathlib rốt cuộc cũng được biên dịch thành mã mà kernel xử lý
      Bản thảo bài báo trên website 0 cũng nhấn mạnh điểm này: Lean là một dự án lớn, nhưng để bảo đảm một chứng minh được chấp nhận là đúng thì chỉ cần tin vào kernel. Ngay cả khi tactic tạo ra một hạng chứng minh sai, kernel vẫn có cơ hội phát hiện lỗi đó trước khi chấp nhận chứng minh

    • Điểm khác biệt là trong Lean, bạn chỉ cần tin vào kernel. Mọi thứ còn lại được xây dựng trên đó. Nếu kernel là sound thì mọi thứ khác cũng sound
      Điều này rất khác với ngôn ngữ lập trình thông thường. Với ngôn ngữ thông thường, bug có thể xuất hiện ở bất kỳ đâu. Nó cũng rất khác với toán học, nơi bất kỳ bổ đề nào cũng có thể chứa sai sót

    • Điểm tuyệt vời của trình chứng minh định lý là, miễn là kernel đúng, thì một chứng minh sai thậm chí còn không biên dịch được
      Đối với chứng minh, không có loại bug chỉ xuất hiện ở thời điểm chạy như trong phần mềm truyền thống. Thậm chí còn không có “thời điểm chạy” nào cả
      Lean cũng có thể được dùng như một ngôn ngữ lập trình “thông thường”, và khi đó vẫn có nguy cơ bug lúc chạy, nhưng ở đây không phải như vậy

    • Bạn đang hiểu sai về trình chứng minh định lý. Đây không phải kiểu câu chuyện “mọi tầng trừu tượng đều rò rỉ”. Không cần phải tin thư viện, chỉ cần tin vào kernel
      Việc tin vào kernel dĩ nhiên không phải chuyện nhỏ, nhưng so với chứng minh phi hình thức thì đó vẫn là một bước nhảy vọt lớn. Trong chứng minh phi hình thức, bạn thực sự phải tin vào “thư viện”, tức là văn hóa và tri thức của người khác, vì không có cách thực tế nào để rút mọi thứ xuống tận các tiên đề

  • ZFC đã chết, NF muôn năm?
    Với tư cách một người làm toán nghiệp dư chủ yếu dùng tập hợp như ngôn ngữ chung để mô tả những thứ khác, tôi không rõ điều này có hàm ý gì với toán học rộng hơn. Nhất là nếu tính hữu dụng của NF tương tự ZFC hiện tại và các biến thể của nó
    Liệu NF có được kỳ vọng sẽ phổ biến trong chứng minh bằng máy ngang với ZFC không? Sự tồn tại của tập hợp phổ quát cho cảm giác trực quan hơn, nên ít nhất nhờ chứng minh này mà mối quan tâm cá nhân của tôi với hình thức hóa đã sống lại

    • Từ góc nhìn nghiệp dư ngây thơ, vì mọi mô hình ZFC đều có thể được mở rộng thành mô hình NF, nên kết quả nhất quán tương đối dường như khiến NF ít nhất cũng hữu dụng ngang ZFC
      Nhưng có lẽ NF sẽ không trở nên đặc biệt hữu dụng trừ khi xảy ra một trong các điều sau

      1. Chứng minh được NF là mâu thuẫn. Khi đó ZFC cũng mâu thuẫn. Những ngôi sao trên bầu trời đêm sẽ bắt đầu tắt dần từng cái một ;)

      2. Chứng minh được ZFC là mâu thuẫn. Khi đó khả năng NF là nhất quán vẫn còn. Chỉ còn biết chúc may mắn thôi

      Dĩ nhiên cũng rất có thể tôi đang bỏ sót những lợi thế thực dụng về “chất lượng sống” của NF, như có thể nói về proper class, hay tránh nghịch lý Russell bằng các công thức phân tầng

    • Hoàn toàn không có ý định thúc đẩy NF như một hệ nền tảng độc lập. NF là một hệ khá khác thường
      Nhưng nếu ai đó muốn thúc đẩy nó, thì kết quả nhất quán này ít nhất cho biết rằng xét về nguy cơ dẫn đến mâu thuẫn, nó không lớn hơn nguy cơ đi đến mâu thuẫn trong ZFC

  • Tôi thực sự rất thích điều này
    Tôi tự hỏi liệu cuối cùng nó có dẫn đến chứng minh cộng tác và “sửa bug”, khiến toán học trở thành một quá trình giống như code trên GitHub hay không

  • Tôi ước mình có thời gian rảnh để theo dõi dự án mathlib. Thật sự rất tuyệt
    Có cách nào để tham gia dù chỉ rất lỏng lẻo không?

  • Tôi không thuộc lĩnh vực này, nhưng chẳng phải có định lý Gödel nói rằng mọi hệ đủ mạnh đều không thể tự chứng minh tính nhất quán của chính nó sao?

    • Có lẽ bạn đang nghĩ tới định lý bất toàn của Gödel: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
      Tuy vậy, dù hệ X không thể tự chứng minh tính nhất quán của chính mình, một hệ mạnh hơn Y có thể chứng minh tính nhất quán của X. Và một hệ khác mạnh hơn nữa cũng có thể chứng minh tính nhất quán của Y. Như vậy sẽ hình thành một chuỗi trong đó mỗi hệ chứng minh tính nhất quán của hệ yếu hơn.
      Điều này không chứng minh rằng hệ đó nhất quán theo nghĩa tuyệt đối. Nếu Y có mâu thuẫn, thì có thể chứng minh cả việc X nhất quán lẫn việc X có mâu thuẫn. Dù vậy điều này vẫn có giá trị. Rốt cuộc, một trong những lý do chúng ta dùng Y là vì hiện chưa biết có mâu thuẫn nào trong đó. Các hệ hình thức đôi khi có thể mâu thuẫn một cách tinh vi, nên việc “nhất quán với giả định rằng một hệ khác là nhất quán” vẫn tốt hơn rất nhiều so với “không có chứng minh tính nhất quán nào cả”
    • Ở đây không phải hệ đó tự chứng minh tính nhất quán của chính nó. Tính nhất quán được chứng minh trong một hệ khác mạnh hơn
    • Điểm thú vị là, ngay cả nếu một hệ mạnh có thể tự chứng minh tính nhất quán của chính nó, chỉ riêng điều đó cũng không cho ta biết gì cả
      Một hệ có mâu thuẫn cũng có thể tự chứng minh tính nhất quán của chính nó. Vì vậy, ngay cả khi một hệ có chứng minh rằng bản thân nó nhất quán, ta vẫn không thể biết liệu nó có thực sự nhất quán hay không
    • Có thể hiểu chứng minh này là: “nếu Lean 4 nhất quán thì New Foundations cũng nhất quán”. Điều này không mâu thuẫn với định lý bất toàn của Gödel
    • Hệ ở đây dường như không cố chứng minh các giả định nền tảng của chính nó, mà đang được xây dựng trên một tập hợp giả định đã có sẵn. Có lẽ định lý bạn đang nghĩ tới không áp dụng ở đây

  • Cuộc thảo luận trên Reddit với sự tham gia của một trong những người tạo ra nó cũng đáng xem 0

    https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...