เหตุผลที่เลขคณิตของ Peano เพียงพอ: PA สามารถเข้ารหัสการคำนวณได้

 (math.stackexchange.com)
1 คะแนน โดย GN⁺ 2025-06-15 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • PA ไม่สามารถพิสูจน์ทฤษฎีบท Goodstein ทั้งหมด ∀n G(n) ได้ แต่สำหรับจำนวนธรรมชาติมาตรฐานแต่ละตัว n สามารถแสดงภายใน PA ได้ว่า มีบทพิสูจน์ของ PA สำหรับ G(n)
  • แก่นสำคัญคือการจัดการเฉพาะหอคอยของกำลัง ω ที่มีความสูงจำกัดเท่าที่จำเป็นสำหรับ n และสร้างบทพิสูจน์ของ อุปนัยทรานส์ไฟไนต์ ภายในช่วงนั้นออกมาโดยกลไก
  • ความสูง m ที่ต้องใช้สอดคล้องกับความสูงของ hereditary base notation ของ n และเป็น O(log*(n)); หากใช้สัญกรณ์ย่อ ω^[m] ความยาวของบทพิสูจน์จะลดลงเหลือระดับ O(m log m)
  • ผลลัพธ์นี้หมายถึง “สร้างบทพิสูจน์สำหรับแต่ละกรณีได้” ไม่ได้หมายความว่า PA พิสูจน์ ทฤษฎีบท Goodstein ทั้งหมด ได้
  • PA สามารถเข้ารหัสจำนวน คู่ ลิสต์ สถานะของโปรแกรม และบทพิสูจน์ตรรกะเชิงรูปแบบทั้งหมดไว้ในจำนวนธรรมชาติหนึ่งตัวได้ จึงสามารถตรวจสอบภายใน PA ได้ด้วยว่าบทพิสูจน์ที่สร้างขึ้นเป็นบทพิสูจน์ของ PA จริงหรือไม่

รูปแบบทางคณิตศาสตร์ของคำถาม

  • สิ่งที่สนใจคือประพจน์ G(n) ที่กล่าวว่าลำดับ Goodstein จะไปถึง 0 ในที่สุด

  • ความแตกต่างที่ทราบกันมีดังนี้

    • PA สามารถพิสูจน์ประพจน์กรณีเฉพาะแต่ละกรณีของจำนวนธรรมชาติมาตรฐาน เช่น G(15), G(268) ได้
    • PA ไม่สามารถพิสูจน์ประพจน์ทั้งหมด ∀n ∈ N: G(n) ได้

  • คำถามคือ PA สามารถพิสูจน์ประพจน์ในรูปต่อไปนี้ได้หรือไม่

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

  • P_PA(p, ⌜φ⌝) หมายความว่า p เป็น โค้ดของบทพิสูจน์ ของ φ ภายใน PA

  • ข้อสรุปคือ ในระดับนี้ PA เพียงอย่างเดียวก็เพียงพอ

สิ่งที่ PA ต้องพิสูจน์

  • สำหรับแต่ละ n สิ่งที่ PA ต้องแสดงให้ได้มีสามอย่างต่อไปนี้
    • สามารถคำนวณ ความยาวของบทพิสูจน์ ที่จำเป็นต่อการพิสูจน์ G(n) ได้
    • กระบวนการสร้างบทพิสูจน์นั้นสิ้นสุด
    • ประโยคสุดท้ายของบทพิสูจน์ที่สร้างขึ้นกล่าวถึงการสิ้นสุดของ G(n)
  • สำหรับแต่ละ G(n) สามารถสร้างบทพิสูจน์ของ PA ที่มีความยาว O(log*(n) log(log*(n))) ได้
  • log* คือ ลอการิทึมแบบทำซ้ำ (iterated logarithm) ซึ่งเป็นฟังก์ชันที่เติบโตช้ามาก
  • เมื่อ n ใหญ่ขึ้น บทพิสูจน์ที่ต้องใช้ก็ยาวขึ้นด้วย ดังนั้นเพียงเท่านี้จึงไม่ได้ทำให้ PA พิสูจน์ทฤษฎีบท Goodstein ทั้งหมดได้

ลำดับ Goodstein และสัญกรณ์อันดับ

  • ลำดับ Goodstein ใช้ hereditary base notation ซึ่งเชื่อมโยงกับการแทนอันดับในรูป Cantor normal form

  • ในการสร้างแบบ John von Neumann อันดับถูกสร้างเป็นเซต

    • 0 คือเซตว่าง
    • หากมีอันดับ ord แล้ว ord ∪ {ord} ก็เป็นอันดับด้วย
    • หากมีเซตของอันดับ X แล้วผลรวมเซตของ X ก็เป็นอันดับด้วย

  • Cantor normal form แทนอันดับในรูปต่อไปนี้

    ((n1, ord1), (n2, ord2), ..., (nk, ordk))
    • ni แต่ละตัวเป็นจำนวนธรรมชาติบวก
    • ordi แต่ละตัวเป็นอันดับ
    • ord1 > ord2 > ... > ordk

  • สัญกรณ์นี้แทนอันดับต่อไปนี้

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

  • การเปรียบเทียบจัดการด้วย การเปรียบเทียบแบบพจนานุกรม ตามลำดับ ord1, n1, ord2, n2; หากด้านหนึ่งจบก่อน ด้านที่สั้นกว่าจะเล็กกว่า

จากอุปนัยไปสู่อุปนัยทรานส์ไฟไนต์

  • สัจพจน์ข้อที่ห้าของ PA ใหั อุปนัย สำหรับจำนวนธรรมชาติ
    • S(0) เป็นจริง
    • ถ้า S(n) แล้ว S(s n) ก็เป็นจริงด้วย
    • ดังนั้น S จึงเป็นจริงสำหรับจำนวนธรรมชาติทุกตัว
  • จากสิ่งนี้ PA สามารถนิยาม < แบบเวียนเกิด และพิสูจน์ อุปนัยเข้ม ได้ด้วย
    • หากแสดงได้ว่า สำหรับทุก n เมื่อ S เป็นจริงสำหรับทุกจำนวนที่น้อยกว่า n แล้ว S(n) ก็เป็นจริง ก็จะได้ว่า S เป็นจริงสำหรับจำนวนธรรมชาติทุกตัว
  • ใน ZFC สามารถพิสูจน์ อุปนัยทรานส์ไฟไนต์ ซึ่งเป็นอุปนัยเข้มบนอันดับทั้งหมดได้
  • สำหรับวัตถุที่เขียนใน Cantor normal form จะใช้สมบัติสองอย่าง
    • ลำดับลดลงที่เขียนใน Cantor normal form ต้องมีความยาวจำกัด
    • สามารถใช้อุปนัยทรานส์ไฟไนต์กับวัตถุใน Cantor normal form ได้

ขอบเขตของอุปนัยทรานส์ไฟไนต์ที่เป็นไปได้ใน PA

  • PA ไม่สามารถพิสูจน์อุปนัยทรานส์ไฟไนต์สำหรับอันดับทั้งหมดได้
  • แต่ช่วงอันดับที่มีความสูงจำกัดเฉพาะเจาะจงสามารถจัดการได้ภายใน PA
    • เพราะ PA พิสูจน์อุปนัยเข้มได้ จึงจัดการอุปนัยทรานส์ไฟไนต์ได้ถึง ω
    • ด้วยตรรกะแบบเดียวกัน ก็พิสูจน์อุปนัยทรานส์ไฟไนต์สำหรับ ω^ω ได้ด้วย
    • จากนั้นทำซ้ำด้วยวิธีเดียวกันกับหอคอยความสูงจำกัด เช่น ω^(ω^ω), ω^(ω^(ω^ω)) เป็นต้น
  • บทพิสูจน์ในแต่ละขั้นถูก สร้างขึ้นโดยกลไก โดยเปลี่ยนเพียงความสูงของหอคอย
  • หากเขียนหอคอยลำดับที่ m ออกมาตรง ๆ ความยาวบทพิสูจน์รวมจะเป็น O(m^2)
  • หากใช้สัญกรณ์ย่ออย่าง ω^[m] การเขียน m ต้องใช้ความยาวเพียง O(log m) ดังนั้นบทพิสูจน์รวมจะเป็น O(m log m)
  • สำหรับอันดับแต่ละตัวที่ต่ำกว่า ε₀ ทั้งหมด มีบทพิสูจน์อุปนัยทรานส์ไฟไนต์ภายใน PA อยู่ แต่การรวมทั้งหมดให้เป็นบทพิสูจน์เดียวจะต้องใช้บทพิสูจน์ที่มีความยาวอนันต์
  • หาก PA พิสูจน์อุปนัยทรานส์ไฟไนต์สำหรับ ε₀ ได้ ก็จะสามารถพิสูจน์ความสอดคล้องของ PA ได้ ซึ่งขัดกับทฤษฎีบทความไม่สมบูรณ์ข้อที่สองของ Gödel

กระบวนการสร้างบทพิสูจน์สำหรับแต่ละ G(n)

  • สำหรับ n เฉพาะตัว ต้องใช้เพียงความสูงของหอคอยใน hereditary base notation เท่านั้น
  • ความสูงนี้เป็น O(log*(n)) และถือเป็นฟังก์ชันที่ PA คำนวณได้ง่าย
  • โปรแกรมสามารถรับอินพุต n แล้วส่งออกสิ่งต่อไปนี้
    • บทพิสูจน์ของข้อเท็จจริงทั่วไปเกี่ยวกับ PA
    • บทพิสูจน์ว่า G(n) ติดตาม ลำดับลดลง ภายใน ω^[m] สำหรับ m บางตัว
    • กระบวนการคำนวณ m และบทพิสูจน์ค่าของ m
    • บทพิสูจน์อุปนัยทรานส์ไฟไนต์สำหรับ ω^[0]
    • บทพิสูจน์ว่าอุปนัยทรานส์ไฟไนต์ของ ω^[i] บ่งชี้อุปนัยทรานส์ไฟไนต์ของ ω^[i+1]
    • บทพิสูจน์อุปนัยทรานส์ไฟไนต์ในแต่ละขั้นตั้งแต่ i = 0 ถึง m-2
    • บทพิสูจน์ว่าอุปนัยทรานส์ไฟไนต์ของ ω^[m-1] บ่งชี้ข้อเท็จจริงที่ว่าลำดับลดลงทั้งหมดใน ω^[m] มีความยาวจำกัด
    • ข้อสรุปว่า G(n) สิ้นสุด
  • PA สามารถพิสูจน์สิ่งต่อไปนี้เกี่ยวกับกระบวนการนี้ได้
    • กระบวนการสิ้นสุด
    • กระบวนการสร้างลิสต์ของประโยค
    • ลิสต์เริ่มต้นด้วยสัจพจน์ของ Peano
    • แต่ละประโยคตามมาอย่างสมเหตุสมผลจากประโยคก่อนหน้า
    • ด้วยอุปนัย ทุกประโยคได้รับการพิสูจน์
    • ประโยคสุดท้ายคือ “G(n) สิ้นสุด”
  • ดังนั้น PA จึงพิสูจน์ได้ว่า สำหรับจำนวนธรรมชาติใด ๆ n PA พิสูจน์การสิ้นสุดของ G(n) ได้

วิธีที่ PA เข้ารหัสการคำนวณ

  • “การเข้ารหัส” คือวิธีการกำหนดให้จำนวนธรรมชาติบางตัวหมายถึงโครงสร้างเฉพาะอย่างหนึ่ง
  • วัสดุพื้นฐานของ PA มีดังนี้
    • 0
    • ฟังก์ชันตัวถัดไป (s n)
    • ความเท่ากัน
    • ตัวก่อนหน้า (p n) สำหรับจำนวนที่ไม่ใช่ 0
    • นิยามเวียนเกิดที่รองรับด้วยอุปนัย
    • คำสั่งเงื่อนไขที่แยกกรณีตาม 0 หรือ 1
  • ภายใน PA สามารถนิยามฟังก์ชันเลขคณิตพื้นฐานต่อไปนี้แบบเวียนเกิดได้
    • <
    • min, max
    • +
    • *
    • การยกกำลัง
    • เศษเหลือ %
    • การหารจำนวนเต็ม //
  • สมบัติพื้นฐานของฟังก์ชันเหล่านี้พิสูจน์ได้ภายใน PA ด้วยอุปนัย

การสร้างโครงสร้างข้อมูลด้วยจำนวนธรรมชาติหนึ่งตัว

  • การเข้ารหัสจำนวนธรรมชาติสองตัวให้เป็นจำนวนธรรมชาติหนึ่งตัวสามารถใช้วิธีสลับวางบิตฐานสองได้
    • บิตตำแหน่งคี่คือ head
    • บิตตำแหน่งคู่คือ tail
  • จากคู่ที่สร้างแบบนี้ สามารถดึง head และ tail กลับออกมาได้
  • เมื่อสร้างคู่ได้ ก็สามารถแทน ลิงก์ลิสต์ ได้ด้วย
    • ใช้ 0 เป็น nil
    • ลิสต์ว่าง
    • เพิ่มองค์ประกอบไว้ด้านหน้า
    • อ่านหัวและหาง
    • คำนวณความยาว
    • เข้าถึงตำแหน่งใด ๆ
    • แทรกและลบ
  • เมื่อมีจำนวน คู่ และลิสต์ ก็สามารถแทนโครงสร้างอย่างสแตก คิว ต้นไม้ เอกสารข้อความ และเครื่องเสมือนด้วยจำนวนธรรมชาติหนึ่งตัวได้

Lisp และการเข้ารหัสกระบวนการคำนวณ

  • Lisp ถูกใช้เป็นภาษาที่อธิบายการพาร์สและการตีความได้ง่าย เพราะมีโครงสร้างวงเล็บและรูปแบบ command and arguments
  • จำนวนธรรมชาติภายใน PA สามารถตีความเป็นคู่ (type, value) ได้
    • ตัวเลข
    • บูลีน
    • คู่
    • ลิสต์
    • ข้อความ เป็นต้น
  • จำนวนธรรมชาติบางตัวอาจไม่ใช่ค่าที่ถูกต้องของประเภทใดประเภทหนึ่ง แต่ค่าที่ถูกต้องสามารถแทนโครงสร้างบางอย่างได้อย่างเป็นเอกลักษณ์
  • บนการเข้ารหัสเหล่านี้ สามารถสร้างโครงสร้างข้อมูลของ Lisp, เครื่องเสมือน Lisp และอินเทอร์พรีเตอร์ Lisp ได้
  • เนื่องจาก Lisp เป็น Turing complete จึงสามารถเข้ารหัสกระบวนการที่คำนวณได้ใด ๆ และสถานะของกระบวนการนั้นภายใน PA ผ่านเส้นทางนี้ได้
  • สถานะการคำนวณหลังผ่านจำนวนขั้นตอนเฉพาะก็สามารถแทนและติดตามภายใน PA ได้

PA เข้ารหัสบทพิสูจน์ของ PA เองด้วย

  • บทพิสูจน์ของตรรกะอันดับหนึ่งสามารถมองเป็นลิสต์ของประโยคได้
    • แต่ละประโยคคือขั้นตอนอนุมานหนึ่งขั้น
    • แม้จะเขียนประโยคที่ผิดหรือการอนุมานที่ผิดได้ แต่กระบวนการตรวจสอบสามารถคัดออกได้
  • ภายใน PA สามารถสร้างประเภทอย่าง type-proof และเข้ารหัสบทพิสูจน์เป็นลิสต์ของประโยคได้
  • กระบวนการตรวจสอบต่อไปนี้ก็เข้ารหัสภายใน PA ได้เช่นกัน
    • ตรวจสอบว่าบทพิสูจน์มีรูปแบบถูกต้องหรือไม่
    • ตรวจสอบว่าแต่ละขั้นตอนของบทพิสูจน์ถูกต้องหรือไม่
    • ตรวจสอบว่าสมมติสัจพจน์ใดไว้บ้าง
    • ตรวจสอบว่าข้อสรุปสุดท้ายเป็นประโยคที่ต้องการหรือไม่
  • หากมีบทพิสูจน์ของประโยคใดประโยคหนึ่งจากสัจพจน์ใด ๆ จำนวนธรรมชาติของ PA เฉพาะตัวที่แทนบทพิสูจน์นั้นก็มีอยู่ด้วย
  • PA สามารถแทนการคำนวณที่ตรวจสอบว่าจำนวนนั้นเป็นโค้ดบทพิสูจน์จริงหรือไม่ ดังนั้นจึงสามารถจัดการ “บทพิสูจน์ภายใน PA” เองได้ภายใน PA
  • Gödel เข้ารหัสตรรกะภายใน PA โดยไม่ต้องเข้ารหัสการคำนวณทั้งหมด แต่จากมุมมองของโปรแกรมเมอร์ เส้นทางที่เข้าใจผ่านการเข้ารหัสการคำนวณเป็นวิธีที่เป็นธรรมชาติ

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2025-06-15
ความคิดเห็นจาก Hacker News

  • บทความนี้เป็นการขยายจากคำถามบน Stack Overflow มาเป็นโพสต์บล็อก
    ว่าด้วยขอบเขตของสิ่งที่พิสูจน์ได้ด้วย สัจพจน์ของ Peano และวิธีเริ่มบูตสแตรป Lisp ภายในกรอบนั้น
    มุกแย่ ๆ ทั้งหมดอยู่ในส่วนที่สอง และยินดีรับคำแก้ไขหรือคำถามต่อยอด

    • อ่านจบแล้วพบว่ามีจุดหนึ่งในตัวอย่าง (defun not (x) ...) ในส่วน "Why Lisp?" ที่ วงเล็บจับคู่ไม่ครบ
      เลยยิ่งตลกเมื่อไปเจอส่วนหลังที่เขียนว่า “การให้คอมพิวเตอร์หาวงเล็บที่สมดุลนั้นง่ายมาก” และคอมเมนต์ในส่วน "Basic Number Theory" ที่ว่า “กองวงเล็บปิดจะหายไปจากสายตา” ก็ขำดี
      ถึงจะไม่ได้เขียน Lisp มานานแล้ว แต่ก็ยังตามทันและจับประเด็นได้ เลยคิดว่าบทความนี้เขียนดี
    • ยังอ่านเลยช่วงเกริ่นนำไปไม่มากนัก แต่ตั้งต้นที่ว่าแต่ละกรณีเฉพาะของ ลำดับ Goodstein พิสูจน์ได้ใน PA ว่าจะจบที่ 0 ขณะที่ข้อความว่าทุกลำดับจะจบนั้นพิสูจน์ใน PA ไม่ได้ เป็นแนวคิดที่น่าสนใจ
      การที่เข้ารหัสการคำนวณได้ด้วยสัจพจน์ของ Peano เพียงอย่างเดียวก็ดูน่าพิศวงอย่างประหลาด ราวกับมีชั้นของการอ้างอิงตนเองเพิ่มขึ้นมาอีกชั้น
      ช่วงนี้เพิ่งเริ่มศึกษาทฤษฎีเซตมากขึ้นและได้เจอลำดับ Goodstein เลยอยากได้คำแนะนำหนังสือทฤษฎีเซตขั้นสูงในลำดับถัดไป หรือหนังสือที่เจาะลึก Peano arithmetic
    • Boot Sector Lisp ก็บูตสแตรปตัวเองได้เช่นกัน: https://justine.lol/sectorlisp2/
      Lisp หลายตัวจาก https://t3x.org ก็สร้างตัวเลขและส่วนอื่น ๆ ขึ้นจาก cons cell กับ apply/eval
      meta-circular evaluator ของ John McCarthy คือโค้ดที่ Alan Kay เรียกว่า “สมการแมกซ์เวลล์ของซอฟต์แวร์” และใน SectorLISP ก็ทำออกมาในรูปแบบอย่าง ASSOC EVAL EVCON APPLY EVLIS PAIRLIS
      Forth บางตัวก็คล้ายกัน และ Zenlisp ของ T3X อธิบายโดยเน้นวิธีที่ eval/apply เรียกกันแบบเวียนกลับ: http://t3x.org/zsp/index.html
    • มีเขียนว่า “omega” อยู่สองแห่ง ซึ่งน่าจะเขียนเป็น \omega

  • ในฐานะคนที่ทำทั้งคณิตศาสตร์และโปรแกรมมิง สิ่งที่น่าสนใจกว่าการเข้ารหัสการคำนวณเองคือการที่ ความเป็นอิสระของทฤษฎีบท Goodstein ถูกเลี่ยงได้ด้วยวิธีอ้างอิงตนเองแบบนี้
    ดูเหมือนว่าจะหมายถึง PA + “PA มีความสอดคล้องแบบ ω” สามารถพิสูจน์ทฤษฎีบท Goodstein ได้ และอาจรวมถึงอุปนัยทรานส์ฟินิตถึง ε₀ ได้โดยทั่วไปด้วย
    แก้ไข: ชักสงสัยว่าแค่ PA + “PA สอดคล้อง” ก็เพียงพอแล้วหรือไม่

    • ในฐานะคนที่เป็นคนตั้งคำถาม SO เดิม ผมได้เพิ่มลิงก์คำตอบที่เกี่ยวข้องกับคำถามไว้ไม่กี่อัน
      ประเด็นสำคัญคือแค่ “PA สอดคล้อง” ยังไม่พอ แต่ถ้ามี หลักการสะท้อนแบบสม่ำเสมอ ที่ว่า “ถ้า PA พิสูจน์บางสิ่งได้ สิ่งนั้นก็เป็นจริง” ก็เพียงพอ
      ผมยังไม่มั่นใจ 100% ว่าหลักการนี้สมมูลกับความสอดคล้องแบบ ω หรือไม่ แต่จากสิ่งต่อไปนี้ก็ดูเหมือนจะเป็นเช่นนั้น: https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relation_to_other_consistency_principles
      Wikipedia อธิบายว่า T เป็น ω-consistent ว่า “T + RFN_T + เซตของทุกประพจน์จริงมีความสอดคล้อง” ซึ่งดูเหมือนจะมีความหมายเดียวกับ “T + RFN_T เป็นจริง”
    • ชอบโครงสร้างแบบเรียกซ้ำนี้
      โดยแก่นแล้วคือการสร้าง เมตาพิสูจน์ เกี่ยวกับสิ่งที่ PA พิสูจน์ได้ และถ้าคุณเชื่อถือ PA คุณก็จะเชื่อถือเมตาพิสูจน์นั้นด้วย
      แต่ก็ยังไม่เข้าใจว่า PA + “PA สอดคล้อง” จะเพียงพอได้อย่างไร
      ระบบนั้นน่าจะยอมให้มีโมเดลที่ทฤษฎีบท Goodstein เป็นจริงบนจำนวนธรรมชาติมาตรฐาน แต่เป็นเท็จสำหรับจำนวนเต็มนอกมาตรฐานบางตัว N และดูเหมือนว่าตรงนี้เองที่ ความสอดคล้องแบบ ω ที่แรงกว่าจะตัดทิ้งได้
    • น่าเสียดายที่ไม่ใช่ และดูเหมือนว่าสูตรสากลล้วน ๆ อย่างเดียวก็ทำอย่างอื่นไม่ได้เช่นกัน
      กล่าวคือ นี่ไม่ใช่ปัญหาเฉพาะของ Con(PA) แต่เป็นปรากฏการณ์ทั่วไปกว่านั้น: https://math.stackexchange.com/questions/5003237/can-goodsteins-theorem-be-proven-in-mathrmpa-conpa
      สำหรับคำถามแรก ผมสงสัยว่าจะเข้ารหัส ความสอดคล้องแบบ ω เป็นสูตรของ PA ได้อย่างไร
    • โพสต์ใน Math Exchange บอกว่า PA + อุปนัยทรานส์ฟินิตบน ε₀ พิสูจน์ความสอดคล้องของ PA ได้
      เพราะอย่างนั้นจึงดูเหมือนว่า PA + “PA สอดคล้อง” น่าจะพิสูจน์อุปนัยทรานส์ฟินิตบน ε₀ ได้
    • ตอนนี้รายละเอียดเริ่มออกนอกขอบเขตที่ผมจะพูดอย่างมั่นใจได้แล้ว
      ChatGPT บอกว่า PA + “PA สอดคล้อง” เพียงอย่างเดียวยังไม่พอ และก็น่าจะเชื่อคำกล่าวนั้นได้เพราะมันคงอ่านตำราตรรกะมามากพอ

  • ตอนที่ได้ใช้ Peano arithmetic ครั้งแรก ผมค่อนข้างทึ่งกับพลังในการแสดงออกของมัน
    ตอนแรกมันดูเหมือนเป็นระบบพื้นฐาน แต่พอเข้าใจว่าเราสามารถเข้ารหัสการคำนวณไว้ใน PA เองและเลียนแบบการคำนวณได้หลายชนิด สิ่งที่เคยดูซับซ้อนก็เริ่มเชื่อมต่อกัน
    อยากได้คำแนะนำสื่อที่อธิบายเทคนิคการเข้ารหัสแบบนี้ให้เป็นมิตรกับผู้เริ่มต้น

  • นี่คล้ายกับ ทฤษฎี Boyer-Moore มาก ทฤษฎีนี้ก็สร้างคณิตศาสตร์ขึ้นมาบนระดับของสัจพจน์ Peano
    Boyer และ Moore ยังสร้างตัวพิสูจน์ทฤษฎีบทอัตโนมัติที่ออกแบบมาสำหรับทฤษฎีนี้ด้วย และมีสำเนาที่ทำงานบน GNU Common Lisp อยู่ที่ https://github.com/John-Nagle/nqthm/tree/master
    ตามคำอธิบายของพวกเขา จะเข้าใจได้ง่ายถ้ามองโปรแกรมเหมือนนักเรียนคณิตศาสตร์ที่ค่อนข้างเก่งคนหนึ่ง ถ้าให้แค่สัจพจน์ Peano อย่างเดียว ก็คงยากจะคาดหวังให้มันพิสูจน์หรือค้นพบทฤษฎีบทการแยกตัวประกอบเฉพาะได้ แต่ถ้าให้รายการทฤษฎีบทควบคู่กับสัจพจน์ Peano เช่น “จงพิสูจน์สมบัติการสลับที่ของการบวก”, “จงพิสูจน์ว่าการคูณแจกแจงเหนือการบวก”, “จงพิสูจน์ว่าผลลัพธ์ของฟังก์ชัน GCD หารอาร์กิวเมนต์ทั้งสองลงตัว” ก็สามารถจัดการได้ดี
    บทความ: https://www.cs.utexas.edu/~boyer/acl.pdf

  • คอมเมนต์ที่ตอบ JoJoModding บน Math StackExchange นั้นผิด
    คำอธิบายที่ว่า “PA อาจพิสูจน์ได้ว่าตนสร้างบทพิสูจน์ขึ้นมาได้ แต่พิสูจน์ไม่ได้ว่าบทพิสูจน์นั้นมีความยาวจำกัด” จับประเด็นสำคัญผิดไป
    ถ้า PA พิสูจน์ได้ว่า “PA พิสูจน์ X ได้” แล้ว PA ก็พิสูจน์ X ได้
    จุดสำคัญไม่ใช่ว่ามีโมเดลไม่เป็นมาตรฐานอยู่ แต่เป็นการที่ โมเดลมาตรฐานของจำนวนธรรมชาติ เป็นโมเดลของ PA
    ดังนั้นถ้า PA พิสูจน์ว่า “PA พิสูจน์ X ได้” ก็จะมีจำนวนธรรมชาติจำกัดแบบมาตรฐานจริง ๆ ที่สอดคล้องกับบทพิสูจน์ที่เข้ารหัสของ “PA พิสูจน์ X ได้” และสามารถใช้จำนวนธรรมชาตินั้นสร้างบทพิสูจน์ของ X ภายใน PA ได้

    • เวอร์ชันภาษาธรรมชาติที่ยกมานั้นกำกวม จึงต้องแยกให้ชัด
      สิ่งที่แสดงไว้ไม่ใช่ “PA พิสูจน์ Provable(forall n, G(n))” แต่เป็น “PA พิสูจน์ forall n, Provable(G(n))”
      ถ้าเป็นแบบแรก ก็จะตามมาจริงว่า “PA พิสูจน์ forall n, G(n)” แต่แบบหลังไม่เหมือนกัน
      โดยไม่อ้างถึงลำดับ Goodstein อยากเห็นข้อโต้แย้งว่า สำหรับประพจน์ทั่วไป P การพิสูจน์ forall n, Provable(P(n)) ไม่ได้ทำให้พิสูจน์ Provable(forall n, P(n)) ได้
    • คำกล่าวที่ว่า “ถ้า PA พิสูจน์ว่า ‘PA พิสูจน์ X ได้’ แล้ว PA ก็พิสูจน์ X ได้” นั้นไม่จริง
      ภายใน PA สามารถสร้างฟังก์ชันที่ค้นหาบทพิสูจน์ทั้งหมดที่ PA สร้างได้ และจากนั้นสร้างฟังก์ชัน will-return เพื่อวิเคราะห์ว่าฟังก์ชันหนึ่งกับอินพุตหนึ่งจะคืนค่าหรือไม่
      สิ่งนี้คล้ายกับความพยายามแก้ปัญหาการหยุดทำงาน จึงไม่ได้ใช้ได้เสมอไป แต่ใช้ได้ในหลายกรณี
      จากตรงนี้สามารถสร้าง opposite-return ที่พยายามคืนค่าเมื่อฟังก์ชันและอินพุตที่กำหนดจะไม่คืนค่า และจะไม่คืนค่าเมื่อมันคืนค่า
      ถ้าพิจารณา (opposite-return opposite-return opposite-return) แบบเดียวกับการพิสูจน์ปัญหาการหยุดทำงานมาตรฐาน PA จะพิสูจน์ได้ว่า “ถ้า PA พิสูจน์ได้ว่า opposite-return คืนค่า มันจะไม่คืนค่าจริง”, “ถ้า PA พิสูจน์ได้ว่ามันไม่คืนค่า มันจะคืนค่าจริง”, “ถ้า PA สามารถพิสูจน์ทุกสิ่งที่มันพิสูจน์ว่าตัวเองพิสูจน์ได้จริง ก็ต้องมีบทพิสูจน์ของหนึ่งในสองข้อความก่อนหน้า”, และ “ดังนั้นในกรณีนั้น PA จะไม่สอดคล้องกัน”
      นี่เป็นรูปแบบหนึ่งของ ทฤษฎีบทความไม่สมบูรณ์ลำดับที่สองของ Gödel และเพราะฉะนั้นต้องแยก “PA พิสูจน์” ออกจาก “PA พิสูจน์ว่าตัวเองพิสูจน์”
    • การที่โมเดลมาตรฐานเป็นโมเดลของ PA เป็นจริงก็ต่อเมื่อ PA สอดคล้องกันเท่านั้น และ PA ไม่สามารถพิสูจน์ได้ว่าตัวเองสอดคล้องกัน ถ้ามันไม่ขัดแย้งกันก็เป็นไปไม่ได้เพราะทฤษฎีบทของ Gödel
      ดังนั้นบทพิสูจน์ที่เสนอจึงใช้ไม่ได้ภายใน PA และดูเหมือนว่านั่นคือประเด็นของคอมเมนต์นั้นพอดี

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

  • ระหว่างคุยกับใครบางคนเรื่อง ชนิดข้อมูลแบบอุปนัย ก็ได้แสดงนิยาม zero/succ แบบเดียวกับ Nat ใน Lean หรือ Rocq
    อีกฝ่ายถามว่า “มีแค่นี้เองหรือ? แล้วสัจพจน์ Peano ล่ะ? มีอะไรที่เป็นมูลฐานยิ่งกว่าชนิดข้อมูลแบบอุปนัยอีกไหม?” ซึ่งก็น่าสนใจดี
    มันทำให้นึกได้ว่าควรมองสัจพจน์ Peano เป็นเพียงหนึ่งในหลายทางเลือกการออกแบบ มากกว่าจะถือว่าเป็นสิ่งที่ฝังอยู่โดยปริยาย

    • มองว่าจำนวนธรรมชาติเป็นสิ่งที่มูลฐานกว่าชนิดข้อมูลแบบอุปนัย
      เพราะ ชนิดข้อมูลแบบอุปนัย ทุกชนิดสามารถสร้างได้จากจำนวนธรรมชาติและตัวสร้างชนิดปฐมฐานอย่างจำนวนเฉพาะ เช่น Π, Σ, =, Ω เป็นต้น

  • แค่ แลมบ์ดาแคลคูลัส แบบบริสุทธิ์ก็เพียงพอแล้ว เพราะแลมบ์ดาแคลคูลัสเข้ารหัสการคำนวณได้

  • ในเรื่องความสอดคล้องกันของ PA มีสิ่งที่พิสูจน์ได้ภายใน PA: https://youtu.be/6pjLmmkZnIA

    • สำหรับคนที่ไม่ใช่นักตรรกศาสตร์ จำเป็นต้องมีบริบทจริง ๆ
      ทฤษฎีบทความไม่สมบูรณ์ลำดับที่สองของ Gödel แสดงว่า ถ้า PA สามารถพิสูจน์ความสอดคล้องกันของตัวเองได้ PA ก็จะไม่สอดคล้องกัน และเพราะฉะนั้นจะพิสูจน์อะไรก็ได้รวมถึงข้อความเท็จ
      งานที่ลิงก์ไว้ไม่ได้แสดงว่า PA ไม่สอดคล้องกัน แต่เป็นการนิยามความหมายใหม่ที่อ่อนกว่าสำหรับคำว่า PA “พิสูจน์ความสอดคล้องกันของตัวเอง” แล้วแสดงว่า PA ทำสิ่งที่อ่อนกว่านั้นได้
      เป็นงานที่น่าสนใจ แต่ต้องรู้ตรรกศาสตร์มาพอสมควรอยู่แล้วจึงจะเข้าใจความหมาย

  • โพสต์นี้ได้ 123 คะแนน แต่โพสต์ SO ที่ลิงก์ไว้มีเพียง 11 โหวตบวก

    • บน Stack Overflow ต้องมี ค่าชื่อเสียง 15 แต้ม จึงจะกดโหวตบวกได้
      พอรวมข้อจำกัด 15 แต้มเข้ากับปัญหาด้านชื่อเสียงที่ว่าโพสต์ที่นั่นมีโอกาสโดนลบง่าย ก็ดูเหมือนว่าหลายคนจึงกดโหวตบวกไม่ได้