Vì sao chỉ cần số học Peano: PA có thể mã hóa tính toán

 (math.stackexchange.com)
1 điểm bởi GN⁺ 2025-06-15 | 1 bình luận | Chia sẻ qua WhatsApp
  • PA không thể chứng minh toàn bộ định lý Goodstein ∀n G(n), nhưng với mỗi số tự nhiên chuẩn n, có thể chỉ ra sự tồn tại của một chứng minh trong PA cho G(n) ngay bên trong PA
  • Cốt lõi là chỉ cần xử lý đến tháp lũy thừa ω có chiều cao hữu hạn cần thiết cho n, rồi cơ học hóa việc tạo ra chứng minh quy nạp siêu hạn trong phạm vi đó
  • Chiều cao cần thiết m tương ứng với độ cao của hereditary base notation của n, là O(log*(n)); nếu dùng ký hiệu rút gọn ω^[m] thì độ dài chứng minh giảm xuống mức O(m log m)
  • Kết quả này có nghĩa là “có thể tạo chứng minh cho từng trường hợp”, chứ không có nghĩa PA chứng minh được toàn bộ định lý Goodstein
  • PA có thể mã hóa mọi thứ bằng một số tự nhiên duy nhất: số, cặp, danh sách, trạng thái chương trình, và cả chứng minh logic hình thức; vì thế ngay trong PA cũng có thể kiểm tra một chứng minh được tạo ra có thực sự là chứng minh PA hay không

Dạng toán học của câu hỏi

  • Đối tượng được quan tâm là mệnh đề G(n) nói rằng dãy Goodstein cuối cùng sẽ đạt tới 0

  • Phân biệt đã biết như sau

    • PA có thể chứng minh từng trường hợp cụ thể trên các số tự nhiên chuẩn như G(15), G(268)
    • PA không thể chứng minh mệnh đề tổng quát ∀n ∈ N: G(n)

  • Câu hỏi là liệu PA có thể chứng minh mệnh đề ở dạng sau hay không

    ∀n ∈ N: ∃p ∈ N: P_PA(p, ⌜G(n)⌝)

  • P_PA(p, ⌜φ⌝) có nghĩa là p là mã chứng minh của φ trong PA

  • Kết luận là ở mức này thì chỉ riêng PA là đủ

PA phải chứng minh điều gì

  • Với mỗi n, PA cần chỉ ra ba điều sau
    • Có thể tính được độ dài chứng minh cần để chứng minh G(n)
    • Thủ tục dựng chứng minh đó sẽ kết thúc
    • Câu cuối cùng của chứng minh được dựng ra phát biểu sự kết thúc của G(n)
  • Với mỗi G(n), có thể dựng một chứng minh PA có độ dài O(log*(n) log(log*(n)))
  • log* là logarit lặp (iterated logarithm) và tăng rất chậm
  • Khi n lớn hơn, chứng minh cần thiết cũng dài hơn, nên chỉ riêng điều này không đủ để PA chứng minh toàn bộ định lý Goodstein

Dãy Goodstein và ký hiệu thứ tự

  • Dãy Goodstein dùng hereditary base notation, và cách viết này liên hệ với biểu diễn thứ tự viết theo dạng chuẩn Cantor

  • Trong cách xây dựng kiểu John von Neumann, thứ tự được tạo từ các tập hợp

    • 0 là tập rỗng
    • nếu có một thứ tự ord thì ord ∪ {ord} cũng là một thứ tự
    • nếu có một tập X gồm các thứ tự thì hợp của X cũng là một thứ tự

  • Dạng chuẩn Cantor biểu diễn thứ tự theo dạng sau

    ((n1, ord1), (n2, ord2), ..., (nk, ordk))
    • mỗi ni là một số tự nhiên dương
    • mỗi ordi là một thứ tự
    • ord1 > ord2 > ... > ordk

  • Ký hiệu này biểu thị thứ tự sau

    n1·ω^ord1 + n2·ω^ord2 + ... + nk·ω^ordk

  • So sánh được xử lý bằng so sánh từ điển theo thứ tự ord1, n1, ord2, n2; nếu một bên kết thúc trước thì bên ngắn hơn nhỏ hơn

Từ quy nạp đến quy nạp siêu hạn

  • Tiên đề thứ năm của PA cung cấp quy nạp trên các số tự nhiên
    • S(0) là đúng
    • nếu S(n) thì S(s n) cũng đúng
    • khi đó S đúng với mọi số tự nhiên
  • Từ đó, PA có thể định nghĩa đệ quy quan hệ < và cũng chứng minh được quy nạp mạnh
    • nếu với mọi n, từ giả thiết S đúng với mọi số nhỏ hơn n suy ra S(n) đúng, thì S đúng với mọi số tự nhiên
  • Trong ZFC, có thể chứng minh quy nạp siêu hạn, tức quy nạp mạnh trên toàn bộ các thứ tự
  • Với các đối tượng viết theo dạng chuẩn Cantor, dùng hai tính chất sau
    • mọi dãy giảm viết theo dạng chuẩn Cantor đều phải là hữu hạn
    • có thể áp dụng quy nạp siêu hạn cho các đối tượng ở dạng chuẩn Cantor

Phạm vi quy nạp siêu hạn khả dĩ bên trong PA

  • PA không thể chứng minh quy nạp siêu hạn cho mọi thứ tự
  • Thay vào đó, PA có thể xử lý các phạm vi thứ tự có chiều cao hữu hạn cụ thể
    • vì PA chứng minh được quy nạp mạnh nên có thể xử lý quy nạp siêu hạn đến ω
    • theo đúng logic đó, cũng có thể chứng minh quy nạp siêu hạn cho ω^ω
    • lặp lại cách này, ta có ω^(ω^ω), ω^(ω^(ω^ω)) và các tháp hữu hạn khác
  • Chứng minh ở mỗi bước chỉ khác ở chiều cao của tháp và có thể tạo ra một cách cơ học
  • Nếu viết nguyên tháp thứ m thì toàn bộ chứng minh có độ dài O(m^2)
  • Nếu dùng ký hiệu rút gọn như ω^[m] thì chỉ cần O(log m) độ dài để viết m, nên toàn bộ chứng minh là O(m log m)
  • Với từng thứ tự nằm dưới ε₀, đều tồn tại một chứng minh quy nạp siêu hạn trong PA, nhưng để gộp tất cả thành một chứng minh duy nhất thì sẽ cần một chứng minh dài vô hạn
  • Nếu PA chứng minh được quy nạp siêu hạn cho ε₀ thì PA sẽ chứng minh được tính nhất quán của chính nó, mâu thuẫn với định lý bất toàn thứ hai của Gödel

Thủ tục tạo chứng minh cho từng G(n)

  • Với một n cụ thể, chỉ cần đến độ cao tháp trong hereditary base notation của nó
  • Độ cao này là O(log*(n)) và được xem như một hàm mà PA có thể tính dễ dàng
  • Với đầu vào n, chương trình có thể xuất ra
    • các chứng minh về những sự kiện chung liên quan đến PA
    • chứng minh rằng G(n) theo dõi một dãy giảm trong ω^[m] với một m nào đó
    • quá trình tính m và chứng minh về giá trị của m
    • chứng minh quy nạp siêu hạn cho ω^[0]
    • chứng minh rằng quy nạp siêu hạn cho ω^[i] kéo theo quy nạp siêu hạn cho ω^[i+1]
    • các chứng minh quy nạp siêu hạn cho từng bước từ i = 0 đến m-2
    • chứng minh rằng quy nạp siêu hạn cho ω^[m-1] kéo theo việc mọi dãy giảm trong ω^[m] đều hữu hạn
    • kết luận rằng G(n) kết thúc
  • Đối với thủ tục này, PA có thể chứng minh rằng
    • thủ tục sẽ kết thúc
    • thủ tục tạo ra một danh sách các mệnh đề
    • danh sách bắt đầu bằng các tiên đề Peano
    • mỗi mệnh đề suy ra hợp logic từ các mệnh đề trước đó
    • bằng quy nạp, mọi mệnh đề trong danh sách đều được chứng minh
    • mệnh đề cuối cùng là “G(n) kết thúc”
  • Vì vậy, với mọi số tự nhiên n, PA chứng minh được việc PA chứng minh sự kết thúc của G(n)

Cách PA mã hóa tính toán

  • “Mã hóa” là quy ước để một số tự nhiên nào đó biểu thị một cấu trúc nhất định
  • Các thành phần cơ bản của PA là
    • 0
    • hàm kế tiếp (s n)
    • quan hệ bằng nhau
    • hàm tiền nhiệm (p n) cho các số khác 0
    • các định nghĩa đệ quy được biện minh bằng quy nạp
    • câu lệnh điều kiện phân nhánh theo 0 hoặc 1
  • Bên trong PA, có thể định nghĩa đệ quy các hàm số học cơ bản sau
    • <
    • min, max
    • +
    • *
    • lũy thừa
    • phần dư %
    • phép chia nguyên //
  • Các tính chất cơ bản của những hàm này đều có thể được chứng minh trong PA bằng quy nạp

Tạo cấu trúc dữ liệu từ một số tự nhiên duy nhất

  • Để mã hóa hai số tự nhiên thành một số tự nhiên, có thể dùng cách xen kẽ các bit trong biểu diễn nhị phân
    • các bit ở vị trí lẻ là head
    • các bit ở vị trí chẵn là tail
  • Từ cặp được tạo như vậy, cũng có thể trích lại head và tail
  • Khi đã tạo được cặp, cũng có thể biểu diễn danh sách liên kết
    • dùng 0 làm nil
    • danh sách rỗng
    • thêm phần tử vào đầu
    • đọc đầu và đuôi danh sách
    • tính độ dài
    • truy cập vị trí bất kỳ
    • chèn và xóa
  • Khi đã có số, cặp và danh sách, các cấu trúc như stack, queue, cây, tài liệu văn bản hay máy ảo cũng có thể được biểu diễn bằng một số tự nhiên duy nhất

Lisp và mã hóa thủ tục tính toán

  • Lisp được dùng như một ngôn ngữ dễ giải thích việc phân tích cú pháp và diễn giải nhờ cấu trúc dấu ngoặc và dạng command and arguments
  • Các số tự nhiên trong PA có thể được diễn giải như các cặp (type, value)
    • số
    • boolean
    • cặp
    • danh sách
    • văn bản, v.v.
  • Một số số tự nhiên có thể không phải là giá trị hợp lệ của một kiểu nhất định, nhưng các giá trị hợp lệ thì có thể biểu thị duy nhất một cấu trúc nào đó
  • Trên lớp mã hóa này, có thể xây dựng cấu trúc dữ liệu Lisp, máy ảo Lisp và trình thông dịch Lisp
  • Vì Lisp là Turing complete, theo con đường này có thể mã hóa mọi thủ tục tính toán khả tính và trạng thái của thủ tục đó bên trong PA
  • Trạng thái tính toán sau một số bước cụ thể cũng có thể được biểu diễn và theo dõi bên trong PA

PA cũng mã hóa cả chứng minh của chính PA

  • Chứng minh trong logic bậc một có thể được xem như một danh sách các mệnh đề
    • mỗi mệnh đề là một bước suy luận
    • vẫn có thể viết ra mệnh đề sai hoặc suy luận sai, nhưng thủ tục kiểm tra sẽ loại chúng ra
  • Bên trong PA, có thể tạo một kiểu như type-proof và mã hóa chứng minh thành danh sách các mệnh đề
  • Những thủ tục kiểm tra sau cũng có thể được mã hóa trong PA
    • kiểm tra chứng minh có được tạo đúng dạng hay không
    • kiểm tra từng bước chứng minh có hợp lệ hay không
    • kiểm tra đang giả định những tiên đề nào
    • kiểm tra kết luận cuối cùng có phải là mệnh đề mong muốn hay không
  • Nếu tồn tại một chứng minh của một mệnh đề từ một hệ tiên đề nào đó, thì cũng tồn tại một số tự nhiên cụ thể của PA biểu diễn chứng minh đó
  • Vì PA có thể biểu diễn phép tính kiểm tra xem số đó có thật sự là mã chứng minh hay không, nên bản thân “chứng minh trong PA” cũng có thể được xử lý ngay bên trong PA
  • Gödel đã mã hóa logic vào PA mà không cần mã hóa toàn bộ tính toán, nhưng từ góc nhìn của lập trình viên thì cách hiểu thông qua mã hóa tính toán là một con đường tự nhiên hơn

Bài viết liên quan

1 bình luận

 
GN⁺ 2025-06-15
Các ý kiến trên Hacker News

  • Đây là bài viết mở rộng từ một câu hỏi trên Stack Overflow thành bài blog
    Bài viết bàn về giới hạn của những gì có thể chứng minh bằng các tiên đề Peano, và cách bắt đầu bootstrap Lisp bên trong đó
    Tất cả các câu đùa dở đều nằm ở phần thứ hai; mọi đính chính hoặc câu hỏi tiếp theo đều được hoan nghênh

    • Sau khi đọc hết bài, tôi thấy trong ví dụ (defun not (x) ...) ở phần "Why Lisp?" có một chỗ ngoặc không khớp
      Điều đó khá buồn cười khi đặt cạnh đoạn sau đó viết rằng “bắt máy tính tìm ngoặc cân bằng thật sự rất dễ”, và chú thích “không còn thấy đống ngoặc đóng nữa” trong phần "Basic Number Theory" cũng thú vị
      Dù đã lâu không dùng Lisp, tôi vẫn có thể theo dõi lại và nắm được ý chính, nên bài viết rất hay
    • Tôi chưa đọc nhiều sau phần mở đầu, nhưng tiền đề rằng từng trường hợp cụ thể của dãy Goodstein đều có thể chứng minh trong PA là kết thúc ở 0, còn mệnh đề rằng mọi dãy đều kết thúc thì không thể chứng minh được, thật thú vị
      Việc chỉ với các tiên đề Peano đã có thể mã hóa tính toán cũng kỳ lạ đến mức đáng kinh ngạc, như thể có thêm một tầng tự tham chiếu nữa
      Gần đây tôi bắt đầu học thêm về lý thuyết tập hợp và đã đọc đến dãy Goodstein; tôi muốn biết có giáo trình lý thuyết tập hợp nâng cao ở bước tiếp theo, hoặc giáo trình đi sâu vào số học Peano nào được khuyên đọc không
    • Boot sector Lisp cũng tự bootstrap chính nó: https://justine.lol/sectorlisp2/
      Nhiều Lisp ở https://t3x.org cũng triển khai số và phần còn lại bằng cons cell và apply/eval
      Bộ đánh giá siêu tuần hoàn của John McCarthy là đoạn mã mà Alan Kay gọi là “các phương trình Maxwell của phần mềm”, và trong SectorLISP nó được triển khai theo kiểu ASSOC EVAL EVCON APPLY EVLIS PAIRLIS
      Một số Forth cũng tương tự, còn Zenlisp của T3X giải thích xoay quanh cách eval/apply gọi đệ quy lẫn nhau: http://t3x.org/zsp/index.html
    • Có hai chỗ viết “omega”, có lẽ nên viết là \omega

  • Từ góc nhìn của người từng làm cả toán học lẫn lập trình, điều thú vị hơn bản thân việc mã hóa tính toán là khả năng đi vòng qua tính độc lập của định lý Goodstein bằng kiểu tự tham chiếu này
    Có vẻ như PA + “PA là ω-nhất quán” có thể chứng minh định lý Goodstein, và có lẽ quy nạp siêu hạn đến ε₀ cũng có thể làm được một cách tổng quát
    Sửa: Tôi tự hỏi liệu chỉ PA + “PA là nhất quán” có đủ không

    • Với tư cách người đã viết câu hỏi SO ban đầu, tôi đã thêm vào câu hỏi vài liên kết đến các câu trả lời liên quan
      Về cốt lõi, chỉ “PA là nhất quán” thì không đủ; nếu có nguyên lý phản ánh đồng đều rằng “nếu PA chứng minh điều gì đó thì điều đó đúng” thì đủ
      Tôi không chắc 100% nguyên lý này có tương đương với ω-nhất quán hay không, nhưng đọc phần sau thì có vẻ như vậy: https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relation_to_other_consistency_principles
      Wikipedia mô tả T là ω-nhất quán là “T + RFN_T + tập hợp mọi mệnh đề đúng là nhất quán”, điều này có vẻ tương đương với “T + RFN_T là đúng”
    • Tôi thích cấu trúc đệ quy này
      Về bản chất, ta tạo một siêu chứng minh về những gì PA chứng minh, và nếu tin PA thì ta cũng sẽ tin siêu chứng minh đó
      Tuy nhiên tôi không rõ PA + “PA là nhất quán” làm sao lại đủ
      Hệ đó có vẻ cho phép các mô hình trong đó định lý Goodstein đúng với các số tự nhiên chuẩn, nhưng sai với một số nguyên phi chuẩn N nào đó, và có vẻ chính ω-nhất quán mạnh hơn sẽ loại trừ trường hợp đó
    • Đáng tiếc là không phải vậy; dường như chỉ với công thức toàn xưng thuần túy thì những thứ khác cũng không làm được
      Tức là đây không phải vấn đề riêng của Con(PA), mà là một hiện tượng tổng quát hơn: https://math.stackexchange.com/questions/5003237/can-goodsteins-theorem-be-proven-in-mathrmpa-conpa
      Liên quan đến câu hỏi đầu tiên, tôi thắc mắc ω-nhất quán được mã hóa thành công thức của PA như thế nào
    • Bài trên Math Exchange nói rằng PA + quy nạp siêu hạn đối với ε₀ chứng minh được tính nhất quán của PA
      Vì vậy có vẻ như PA + “PA là nhất quán” có thể chứng minh quy nạp siêu hạn đối với ε₀
    • Đến đây thì chi tiết đã hơi vượt khỏi phạm vi tôi có thể nói chắc chắn
      ChatGPT nói rằng chỉ PA + “PA là nhất quán” là không đủ, và vì nó hẳn đã tiêu hóa kha khá giáo trình logic học nên có lẽ có thể tin nhận định đó

  • Khi lần đầu dùng số học Peano, tôi khá ngạc nhiên trước sức biểu đạt của nó
    Ban đầu nó trông như một hệ cơ bản, nhưng khi nhận ra có thể mã hóa chính việc tính toán bên trong PA và mô phỏng nhiều loại tính toán, những thứ từng có vẻ phức tạp bắt đầu khớp lại với nhau
    Tôi muốn biết có tài liệu nào giải thích các kỹ thuật mã hóa này một cách thân thiện cho người mới không

  • Điều này rất giống với lý thuyết Boyer-Moore. Lý thuyết này cũng xây dựng toán học từ mức các tiên đề Peano
    Boyer và Moore còn tạo ra một trình chứng minh định lý tự động phù hợp với lý thuyết này, và đặt một bản chạy trên GNU Common Lisp tại https://github.com/John-Nagle/nqthm/tree/master
    Theo cách họ giải thích, sẽ dễ hiểu nếu xem chương trình như một sinh viên toán khá giỏi. Nếu chỉ đưa các tiên đề Peano thì khó kỳ vọng nó chứng minh hay khám phá định lý phân tích ra thừa số nguyên tố, nhưng nếu cùng với các tiên đề Peano ta đưa cho nó danh sách định lý như “hãy chứng minh luật giao hoán của phép cộng”, “hãy chứng minh phép nhân phân phối đối với phép cộng”, “hãy chứng minh kết quả của hàm GCD chia hết cả hai đối số”, thì nó có thể xử lý tốt
    Bài báo: https://www.cs.utexas.edu/~boyer/acl.pdf

  • Bình luận gửi JoJoModding trên Math StackExchange là sai
    Cách giải thích rằng “PA có thể chứng minh rằng nó tạo ra một chứng minh, nhưng có thể không chứng minh được rằng chứng minh đó có độ dài hữu hạn” đã hiểu sai trọng tâm
    Nếu PA chứng minh “PA chứng minh X”, thì PA có thể chứng minh X
    Điểm quan trọng không phải là có các mô hình phi chuẩn, mà là mô hình số tự nhiên chuẩn là một mô hình của PA
    Do đó, nếu PA chứng minh “PA chứng minh X”, thì thực sự tồn tại một số tự nhiên hữu hạn chuẩn tương ứng với chứng minh được mã hóa của “PA chứng minh X”, và từ số tự nhiên đó có thể cấu dựng chứng minh của X bên trong PA

    • Phiên bản ngôn ngữ tự nhiên được đưa ra khá mơ hồ, nên cần phân biệt rõ
      Điều được chứng minh không phải là “PA chứng minh Provable(forall n, G(n))”, mà là “PA chứng minh forall n, Provable(G(n))”
      Nếu là vế trước thì đúng là sẽ suy ra “PA chứng minh forall n, G(n)”, nhưng vế sau thì khác
      Tôi muốn thấy một lập luận không viện dẫn dãy Goodstein, rằng với một mệnh đề tổng quát P, từ việc chứng minh forall n, Provable(P(n)) không thể chứng minh Provable(forall n, P(n))
    • Câu “nếu PA chứng minh ‘PA chứng minh X’ thì PA chứng minh X” không đúng
      Bên trong PA có thể xây dựng một hàm tìm kiếm mọi chứng minh mà PA có thể tạo ra, và dựa trên đó tạo một hàm will-return để phân tích xem một hàm và đầu vào nào đó có trả về hay không
      Điều này giống một nỗ lực giải bài toán dừng nên không phải lúc nào cũng hoạt động, nhưng trong nhiều trường hợp thì hoạt động
      Nếu tạo opposite-return ở đây, ta có thể cấu hình nó để cố trả về khi hàm và đầu vào đã cho không trả về, và không trả về khi chúng trả về
      Xét (opposite-return opposite-return opposite-return) theo cùng cách như chứng minh bài toán dừng tiêu chuẩn, PA có thể chứng minh “nếu PA có thể chứng minh rằng opposite-return trả về thì thực ra nó không trả về”, “nếu PA có thể chứng minh rằng nó không trả về thì thực ra nó trả về”, “nếu PA có thể thực sự chứng minh mọi thứ mà nó chứng minh rằng bản thân nó chứng minh, thì nó phải có chứng minh cho một trong hai mệnh đề trên”, “do đó trong trường hợp ấy PA là không nhất quán”
      Đây là một dạng của định lý bất toàn thứ hai của Gödel, vì vậy cần phân biệt giữa “PA chứng minh” và “PA chứng minh rằng bản thân nó chứng minh”
    • Việc mô hình chuẩn là mô hình của PA chỉ đúng khi PA nhất quán, và PA không thể chứng minh rằng bản thân nó nhất quán. Trừ khi nó không mâu thuẫn, điều đó là bất khả do định lý Gödel
      Vì vậy chứng minh được đề xuất không hoạt động bên trong PA, và ý của bình luận kia dường như chính là điểm đó

  • https://math.stackexchange.com/questions/4408124/what-does-the-kirby-paris-theorem-mean

  • Khi nói chuyện với ai đó về kiểu dữ liệu quy nạp, tôi đã cho xem định nghĩa zero/succ như Nat trong Lean hay Rocq
    Người kia hỏi “Chỉ có thế thôi à? Còn các tiên đề Peano? Có thứ gì nguyên thủy hơn kiểu dữ liệu quy nạp không?”, và điều đó khá thú vị
    Nó khiến tôi nhớ rằng tốt hơn nên xem các tiên đề Peano như một lựa chọn trong nhiều thiết kế, thay vì mặc nhiên coi chúng là thứ nội tại

    • Tôi xem số tự nhiên là nguyên thủy hơn kiểu dữ liệu quy nạp
      Vì mọi kiểu dữ liệu quy nạp đều có thể được cấu dựng bằng cách dùng số tự nhiên cùng với các bộ tạo kiểu nguyên thủy khác, chẳng hạn Π, Σ, =, Ω, v.v.

  • Chỉ riêng phép tính lambda thuần túy cũng đủ. Vì phép tính lambda mã hóa được tính toán

  • Liên quan đến tính nhất quán của PA, có thể chứng minh bên trong PA: https://youtu.be/6pjLmmkZnIA

    • Với người không phải nhà logic học thì rất cần ngữ cảnh
      Định lý bất toàn thứ hai của Gödel cho thấy nếu PA có thể chứng minh tính nhất quán của chính nó, thì PA không nhất quán, và do đó có thể chứng minh bất cứ điều gì, kể cả mệnh đề sai
      Công trình được liên kết không chỉ ra sự không nhất quán của PA, mà định nghĩa một ý nghĩa mới yếu hơn của câu “chứng minh tính nhất quán của chính nó”, rồi cho thấy PA có thể làm việc yếu hơn đó
      Đây là một công trình thú vị, nhưng chỉ có ý nghĩa khi đã biết khá nhiều về logic học

  • Bài này nhận được 123 điểm, trong khi bài SO được liên kết chỉ có 11 lượt ủng hộ

    • Stack Overflow yêu cầu phải có 15 điểm danh tiếng mới được ủng hộ
      Có vẻ như vấn đề danh tiếng rằng đăng bài ở đó dễ bị xóa, cộng thêm giới hạn 15 điểm, khiến nhiều người không thể ủng hộ