เลขคณิตเพียโนเพียงพอแล้ว เพราะเลขคณิตเพียโนสามารถเข้ารหัสการคำนวณได้

• เลขคณิตเพียโน (PA) สามารถแสดง กระบวนการคำนวณเชิงกล ได้ จึงสามารถพิสูจน์การสิ้นสุดของลำดับ Goodstein แต่ละลำดับภายใน PA ได้
• ใช้ รูปแบบมาตรฐานของ Cantor และสัญกรณ์จำนวนอันดับแบบถ่ายทอดทางพันธุกรรม ในการแสดงลำดับ Goodstein และสมบัติการลดลงของมัน ทำให้ สามารถสร้างบทพิสูจน์ที่มีความยาวจำกัดได้
• ผ่าน การอุปนัย (อุปนัยแบบเข้มแข็ง/อุปนัยเหนืออนันต์) สามารถขยายบทพิสูจน์ไปถึงจำนวนอันดับระดับที่กำหนดได้ตามลำดับ
• PA สามารถพิสูจน์ได้ว่า สำหรับทุกจำนวนธรรมชาติ n, “G(n) ไปถึง 0” แต่ไม่สามารถพิสูจน์ทฤษฎีบท Goodstein ทั้งหมดแบบครอบคลุม (สำหรับทุก n) ได้
• PA สามารถเข้ารหัสได้เพียงพอทั้ง การคำนวณ โครงสร้างข้อมูล (เช่น List, Pair) และแม้แต่ภาษาการเขียนโปรแกรม (Lisp) เอง รวมถึงกระบวนการพิสูจน์ของตัวมันเองด้วย

---

บทนำและภูมิหลังของปัญหา

• บทความนี้อธิบายว่า เลขคณิตเพียโน (PA) สามารถพิสูจน์ได้ว่าลำดับ Goodstein “ไปถึง 0 สำหรับแต่ละ n (G(n) terminates)”
• สำหรับนักตรรกศาสตร์ นี่อาจดูเป็นเรื่องชัดเจนอยู่แล้ว แต่มีการอธิบายในมุมมองของ การเข้ารหัสการคำนวณ เพื่อให้โปรแกรมเมอร์เข้าใจได้
• สำหรับแต่ละกรณีของลำดับ Goodstein สามารถ สร้างขั้นตอนการพิสูจน์ที่เป็นรูปธรรม ภายใน PA ได้

Ordinals (จำนวนอันดับ) และลำดับ Goodstein

• สร้าง จำนวนอันดับ (Sets as Ordinals) ด้วยแนวทางของ Von Neumann
  • 0 คือเซตว่าง, 1 คือ {0}, 2 คือ {0,1}, ω คือ {0,1,2,…}, ω+1 คือ {0,1,2,…,ω} เป็นต้น โดยลำดับถูกนิยามไว้อย่างชัดเจน
• ลำดับ Goodstein ถูกอธิบายด้วย สัญกรณ์ฐานแบบถ่ายทอดทางพันธุกรรม โดยใช้รูปแบบมาตรฐานของ Cantor
  • ตัวอย่าง: ω^ω คือ ((1,ω)) หรือก็คือ ((1,(1,1)))
  • ลำดับ < ถูกตัดสินด้วยการเปรียบเทียบแบบลำดับพจนานุกรมของจำนวนอันดับ/สัมประสิทธิ์ในแต่ละพจน์

การอุปนัยและอุปนัยเหนืออนันต์ (Transfinite Induction)

• หลักอุปนัยของเลขคณิตเพียโน: ถ้าเป็นจริงสำหรับ 0 และเป็นจริงจาก n→n+1 ก็จะเป็นจริงสำหรับจำนวนธรรมชาติทั้งหมด
• อุปนัยแบบเข้มแข็ง ก็สามารถพิสูจน์ได้ใน PA เช่นกัน
• อุปนัยเหนืออนันต์ (Transfinite induction): ใน ZFC เป็นต้น สามารถขยายไปยังจำนวนอันดับอนันต์ได้ และใช้กับจำนวนที่เขียนในรูปแบบมาตรฐานของ Cantor ได้
  • ทฤษฎีบท 1: ลำดับลดลงที่อยู่ในรูปแบบมาตรฐานของ Cantor จะต้องมีความยาวจำกัดเสมอ
  • ทฤษฎีบท 2: สามารถใช้อุปนัยเหนืออนันต์กับจำนวนในรูปแบบมาตรฐานของ Cantor ได้

อุปนัยเหนืออนันต์ใน PA และความยาวของบทพิสูจน์ลำดับ Goodstein

• PA สามารถ สร้างบทพิสูจน์การสิ้นสุดของลำดับ Goodstein สำหรับ n ใด ๆ ก็ได้
  • สามารถสร้างบทพิสูจน์ตามความสูงของทาวเวอร์ในรูปแบบมาตรฐานของ Cantor ที่ m=O(log* n) (iterated log)
  • ในแต่ละขั้นสามารถประกอบบทพิสูจน์จำนวน m ครั้ง ทำให้ความยาวรวมของบทพิสูจน์เป็น O(m^2) หรือย่อให้เหลือ O(m log m) ได้เมื่อใช้สัญกรณ์พิเศษ (ω[m])
• อย่างไรก็ตาม บทพิสูจน์ของทฤษฎีบท Goodstein ทั้งหมด (สำหรับทุก n) นั้นเป็นไปไม่ได้ใน PA (ไม่สามารถทำอุปนัยเหนืออนันต์จนถึง ε0 ได้)
  • หากทำได้ ก็จะทำให้สามารถพิสูจน์ความสอดคล้องของ PA ได้ด้วย ซึ่งขัดกับทฤษฎีบทความไม่สมบูรณ์ข้อที่ 2 ของ Gödel

การเข้ารหัสโปรแกรมและโครงสร้างข้อมูลใน PA

• PA สามารถเข้ารหัสการคำนวณ/โปรแกรม/โครงสร้างข้อมูล (ตัวเลข คู่ ลิสต์ และโครงสร้างอื่นทั้งหมด) ได้อย่างเพียงพอ
• สามารถทำฟังก์ชันต่าง ๆ ได้ด้วยวิธีต่อไปนี้:
  • ตรรกะพื้นฐานและการคำนวณ (+, *, pow, //, %, min, max เป็นต้น)
  • การจับคู่รูปแบบและการแตกแขนงตามเงื่อนไข (if, cond เป็นต้น)
  • เข้ารหัสตัวเลขหนึ่งตัวให้เป็นตัวเลขสองตัว (คู่) หรือขยายต่อจากคู่ไปเป็นลิสต์และโครงสร้างที่ซับซ้อนกว่าได้แบบวนซ้ำ (ลิสต์เชิงเรียกซ้ำ ต้นไม้ ข้อความ เป็นต้น)
• ด้วยการเข้ารหัสโครงสร้างข้อมูลเหล่านี้ จึงสามารถสร้างได้แม้กระทั่ง ตัวแปลความ/อินเทอร์พรีเตอร์ของเครื่องเสมือนหรือภาษาการเขียนโปรแกรมใด ๆ (เช่น Lisp)

การบูตสแตรปสู่ Lisp และการเข้ารหัส

• ใช้ Lisp เป็นตัวอย่างเพื่ออธิบายวิธีสร้าง การคำนวณเชิงตัวเลขและตรรกะพื้นฐาน โครงสร้างข้อมูล และตัวแปลภาษา/อินเทอร์พรีเตอร์
• โครงสร้างของ Lisp (การแมปคำสั่ง/อาร์กิวเมนต์, special forms, macro เป็นต้น) สามารถสร้างได้ใน PA ด้วยการประกอบฟังก์ชันที่เหมาะสม
• ยิ่งไปกว่านั้น ยังสามารถเข้ารหัสและสร้างเชิงสัญลักษณ์ได้แม้กระทั่ง กระบวนการพิสูจน์ของ PA ภายใน PA เอง ขั้นตอนการพิสูจน์ทางตรรกะ และโครงสร้างแบบอ้างอิงตนเอง

การเข้ารหัสตรรกะเองภายใน PA

• ใน ตรรกะคณิตศาสตร์ สามารถเข้ารหัสกระบวนการพิสูจน์ของ First-Order Logic ให้เป็นข้อมูลตัวเลขของ PA ได้
• แต่ละขั้นของบทพิสูจน์/ประพจน์/กฎการอนุมาน/การตรวจสอบความถูกต้องของบทพิสูจน์ สามารถรับรู้และประมวลผลได้ในรูปของฟังก์ชันเชิงตัวเลขและการประมวลผลลิสต์ชุดหนึ่ง
• การเข้ารหัสเชิงเมตาและแบบอ้างอิงตนเองลักษณะนี้เชื่อมโยงไปถึงทฤษฎีความไม่สมบูรณ์ของ Gödel และการพิสูจน์ปัญหา Halting

บทสรุป

• ทั้งการคำนวณ โครงสร้างข้อมูล โปรแกรม และกระบวนการพิสูจน์ทางตรรกะ ล้วนสามารถเข้ารหัส พิสูจน์ และแปลความได้ภายใน PA อย่างเพียงพอ
• ดังนั้น ลำดับ Goodstein ใด ๆ ก็ตาม (คือ G(n) สิ้นสุดสำหรับ n นั้น) สามารถพิสูจน์ได้อย่างเป็นรูปธรรมภายใน PA
• แต่บทพิสูจน์แบบรวมของทฤษฎีบท Goodstein ทั้งหมด (ทุก n) ว่า "PA พิสูจน์ทฤษฎีบท Goodstein ภายใน PA" นั้นเป็นไปไม่ได้เนื่องจากข้อจำกัดของตรรกะ
• ในมุมมองของโปรแกรมเมอร์ PA คือรากฐานทางตรรกะที่สมบูรณ์สำหรับการเข้ารหัสการคำนวณเอง

[GN⁺]

ความคิดเห็นบน Hacker News

• บทความนี้คือโพสต์บล็อกที่ผมทำขึ้นจากคำถามที่เคยถามไว้บน Stack Overflow โดยอธิบายขีดจำกัดของสิ่งที่พิสูจน์ได้ด้วยระบบสัจพจน์ของ Peano และอธิบายว่าจะบูตสแตรป Lisp ภายในระบบสัจพจน์ของ Peano ได้อย่างไร มุกส่วนใหญ่อยู่ในส่วนที่สอง ยินดีรับคำแก้ไขหรือคำถามเพิ่มเติม
  • ตอนอ่านบทความนี้ ผมสังเกตเห็นในส่วน "Why Lisp?" ว่ามีวงเล็บไม่ตรงกันอยู่จุดหนึ่ง (ดูตัวอย่าง (defun not (x) (if x false true) ) พอใครเริ่มใช้วงเล็บ ผมก็จะเผลอตรวจโดยสัญชาตญาณว่าปิดครบไหม พอหลังจากนั้นบทความพูดว่า "การเขียนโปรแกรมให้คอมพิวเตอร์ตรวจสอบความสมดุลของวงเล็บเป็นเรื่องง่าย" ก็ทำเอาผมหัวเราะออกมาดังมาก มุกแบบนี้ตลกจริง ๆ และคอมเมนต์ ; After a while, you stop noticing that stack of closing parens. ในส่วน "Basic Number Theory" ก็ชวนประทับใจมาก ไม่ได้เจอ Lisp มาพักใหญ่แล้ว แต่บทความนี้สนุกจริง ๆ
  • บทความนี้น่าสนใจมาก ผมยังอ่านได้แค่ช่วงเกริ่นนำ แต่ก็รู้สึกว่าน่าสนใจที่ภายในสัจพจน์ Peano (PA) เราพิสูจน์ได้ว่ากรณีพิเศษแต่ละกรณีของลำดับ Goodstein จะไปถึง 0 แต่พิสูจน์ไม่ได้ว่า "ทุก" กรณีจะไปถึง 0 (ถึงจะเป็นผลที่พอคาดได้ก็เถอะ แต่ก็ยังน่าตื่นเต้น) และการที่สัจพจน์ Peano เพียงอย่างเดียวสามารถเข้ารหัสการคำนวณได้ก็แปลกมาก (ในเชิงหลักการอาจจะเป็นเรื่องธรรมดา แต่ก่อนหน้านี้ผมไม่เคยคิดต่อในระดับ self-reference อีกชั้น) บังเอิญช่วงนี้ผมก็เพิ่งกลับไปศึกษาทฤษฎีเซตเพิ่ม และอ่านตำรา Intro to Set Theory มาถึงส่วนลำดับ Goodstein พอดี ถ้าใครมีตำราทฤษฎีเซตขั้นสูงหรือหนังสือที่เจาะลึก Peano arithmetic ที่แนะนำได้จะขอบคุณมาก เป้าหมายเล็ก ๆ ของผมคืออยากเข้าใจว่าทำไม PA ถึงไม่พอสำหรับการพิสูจน์ทฤษฎีบท Goodstein แต่ถ้ามีเส้นทางอื่นที่แนะนำก็ยินดีเช่นกัน
  • มีอยู่สองจุดในบทความที่พูดถึงโอเมกา (omega) แล้วลืมเขียนเป็น \omega
• คล้ายกับทฤษฎีของ Boyer-Moore มาก ซึ่งเป็นการสร้างคณิตศาสตร์ขึ้นมาบนระดับของสัจพจน์ Peano Boyer และ Moore ได้พัฒนาตัวพิสูจน์ทฤษฎีบทอัตโนมัติที่อิมพลีเมนต์ทฤษฎีนี้ และยังมีสำเนาที่ทำงานบน GNU Common LISP ด้วย ลิงก์ไปยังบทความ "A Computational Logic" และอิมพลีเมนต์ nqthm ก็น่าดูมาก ตัวอย่างในบทความที่น่าประทับใจคือ เมื่อเริ่มจากสัจพจน์ Peano ทฤษฎีบทที่ซับซ้อนอย่างการคูณจำนวนเฉพาะจะยาก แต่กฎสลับที่ของการบวก กฎแจกแจงของการคูณ และทฤษฎีบทเกี่ยวกับฟังก์ชัน GCD ยังพิสูจน์ได้สบาย
• ผมมีพื้นฐานทั้งคณิตศาสตร์และการเขียนโปรแกรม และสำหรับผมแล้ว ส่วนที่น่าสนใจกว่าในเรื่องความเป็นอิสระของทฤษฎีบท Goodstein คือมันดูเหมือนจะอ้อมผ่านแบบ self-referential ได้ ผมคิดว่าอาจพิสูจน์ทฤษฎีบท Goodstein ได้ถ้าเพิ่มสมมติฐาน PA+"PA มีความสอดคล้องแบบโอเมกา (omega-consistent)" และเดาว่านั่นน่าจะทำให้ทำ transfinite induction ได้ไปจนถึง epsilon_0 ด้วย EDIT: หรือว่าแค่ "PA มีความสอดคล้อง" ก็น่าจะพอ?
  • น่าเสียดายที่ไม่พอ และไม่ใช่แค่ Con(PA) เท่านั้น แม้แต่สูตรที่มีตัวบ่งปริมาณแบบสากลใด ๆ ก็ยังไม่พอ ดูคำตอบใน Math StackExchange ที่เกี่ยวข้อง สำหรับคำถามแรก ผมสงสัยว่าเราจะเข้ารหัสความสอดคล้องแบบโอเมกาด้วยสูตรของ PA อย่างไร นึกไม่ออกทันทีเลยเลยยิ่งอยากรู้
  • ผมคือคนที่ถามบน Stack Overflow เอง และได้เพิ่มลิงก์ไปยังคำตอบบางส่วนไว้ในคำถามแล้ว โดยแก่นแล้ว แค่ "PA มีความสอดคล้อง" ไม่พอ แต่ถ้ามีหลักการประมาณว่า "อะไรที่พิสูจน์ได้ใน PA ก็เป็นจริง" ซึ่งเป็น "uniform reflection principle" แบบหนึ่ง ก็จะพอ ผมไม่แน่ใจนักว่าหลักการนี้เท่ากับความสอดคล้องแบบโอเมกาทุกประการหรือไม่ แต่จากคำอธิบายในวิกิพีเดีย ดูเหมือนจะใช่ ถ้า T มีความสอดคล้องแบบโอเมกา ก็มีความหมายว่า "T + RFN_T + เซตของสูตรจริงทั้งหมดมีความสอดคล้อง" ซึ่งตีความได้ว่าเทียบเท่ากับ "T + RFN_T เป็นจริง"
  • ผมชอบโครงสร้างเชิงอุปนัย (รีเคอร์ซีฟ) แบบนี้เหมือนกัน สุดท้ายแล้วเราสร้างเมตาพิสูจน์เกี่ยวกับสิ่งที่ PA พิสูจน์ได้ และถ้าเราเชื่อถือ PA ก็เหมือนมีเหตุให้เชื่อถือเมตาพิสูจน์นี้ด้วย ส่วนที่ว่าแค่ "PA มีความสอดคล้อง" ก็พอนั้น ผมยังไม่ค่อยเข้าใจชัดนัก ในความคิดผม PA+"PA สอดคล้อง" ดูเหมือนจะยังอนุญาตให้มีโมเดลที่ทฤษฎีบท Goodstein เป็นจริงบนจำนวนธรรมชาติมาตรฐาน แต่ก็มีโมเดลที่ทฤษฎีบท Goodstein เป็นเท็จสำหรับจำนวนเต็มนอกมาตรฐานบางตัว N ได้พร้อมกัน ผมมองว่าข้อความที่แรงกว่าของความสอดคล้องแบบโอเมกาจะตัดกรณีแบบนี้ออกไป
  • ในโพสต์บน Math Exchange มีการพูดถึงว่าการพิสูจน์ PA+transfinite induction(epsilon_0) นั้นพิสูจน์ PA เองได้ ผมคิดว่า PA+"PA สอดคล้อง" น่าจะพิสูจน์ transfinite induction ได้ถึง epsilon_0
  • ตอนนี้รายละเอียดเริ่มเลยขอบเขตที่ผมจะพูดอย่างมั่นใจได้แล้ว จากที่ ChatGPT บอก คำอธิบายคือแค่ "PA+PA สอดคล้อง" ยังไม่พอ ChatGPT น่าจะอ่านหนังสือตรรกะมาเยอะพอสมควร ถ้าบอกแบบนั้นก็คงพอเชื่อได้
• คอมเมนต์ที่ผมเขียนถึง JoJoModding บน Stack Overflow ไม่ถูกต้อง ผมเคยบอกว่า "ในโมเดล PA แบบนอกมาตรฐานมีจำนวนธรรมชาติอนันต์อยู่ ดังนั้นแม้ PA จะพิสูจน์ได้ว่ามันสร้างบทพิสูจน์อะไรบางอย่างได้ ก็พิสูจน์ไม่ได้ว่าบทพิสูจน์นั้นยาวจำกัด" แต่จริง ๆ แล้วถ้า PA พิสูจน์ว่า "PA พิสูจน์ X ได้" ก็แปลว่า PA พิสูจน์ X เองได้ด้วย ประเด็นสำคัญไม่ใช่การมีอยู่ของโมเดลนอกมาตรฐาน แต่คือการที่โมเดลจำนวนธรรมชาติมาตรฐานเป็นโมเดลของ PA ดังนั้นถ้า "PA พิสูจน์ว่าตนเองพิสูจน์ X ได้" ก็จะมีการสร้างบทพิสูจน์หนึ่งชิ้นที่สอดคล้องกับจำนวนธรรมชาติจำกัดแบบมาตรฐานจริง ๆ และเราสามารถใช้จำนวนนี้สร้างบทพิสูจน์จริงของ X ภายใน PA ได้
  • ผมยังไม่มีเวลาตรวจตราเหตุผลอย่างละเอียด แต่ถ้ามองในภาษาธรรมชาติ จุดต่างสำคัญคือไม่ใช่ "PA พิสูจน์ 'forall n, G(n)'" แต่เป็น "PA พิสูจน์ 'forall n, Provable(G(n))'" ผมไม่ค่อยแข็งแรงด้านตรรกะนัก ถ้าใครช่วยอธิบายแบบเป็นรูปธรรมได้ว่าทำไมการพิสูจน์ forall n, Provable(P(n)) ถึงไม่ทำให้พิสูจน์ Provable(forall n, P(n)) ได้ จะขอบคุณมาก
  • ข้อความที่ว่า "ถ้า PA พิสูจน์ว่า 'PA พิสูจน์ X' ได้ ก็แปลว่า PA พิสูจน์ X ได้" นั้นไม่ถูกต้อง เราสามารถสร้างฟังก์ชันใน PA ที่ไล่ค้นหาบทพิสูจน์ที่เป็นไปได้ทั้งหมดได้ และจริง ๆ ในส่วนท้ายของคำตอบก็มีการสเก็ตช์วิธีนี้ไว้ จากตรงนี้เรายังสร้างฟังก์ชันอย่าง will-return, opposite-return ได้ด้วย ซึ่งสอดคล้องกับบทพิสูจน์มาตรฐานของปัญหาการหยุด พิจารณากรณี opposite-return(opposite-return, opposite-return) ถ้า PA พิสูจน์ได้ว่า opposite-return จะคืนค่า ก็จะพิสูจน์ได้ด้วยว่าจริง ๆ แล้วมันไม่คืนค่า และในทางกลับกัน ถ้าพิสูจน์ว่าไม่คืนค่า ก็จะพิสูจน์ได้ว่ามันคืนค่า ถ้า PA รับเอาข้อความที่แรงกว่าว่า "สิ่งที่พิสูจน์ได้ทั้งหมดพิสูจน์ได้จริง" ในลักษณะนั้น ก็จะกลายเป็นทฤษฎีบทความไม่สมบูรณ์ลำดับที่สองของ Gödel ทันที ซึ่งหมายความว่า PA ขัดแย้งในตัวเอง ดังนั้นต้องแยก "PA พิสูจน์ได้" ออกจาก "PA พิสูจน์ได้ว่าตนเองพิสูจน์ได้" ให้ชัดเจน
• แค่ pure lambda calculus อย่างเดียวก็พอแล้ว เพราะตัว lambda calculus เองก็เข้ารหัสการคำนวณได้
• ผมคุยกับใครคนหนึ่งเรื่องชนิดข้อมูลเชิงอุปนัย แล้วแสดงนิยาม Nat ที่สร้างด้วย zero/succ (แบบที่เห็นใน Lean หรือ Rocq) ให้ดู อีกฝ่ายก็สงสัยว่า "แค่นี้พอแล้วเหรอ?" "จำเป็นต้องใช้สัจพจน์ Peano ไหม? มีอะไรที่ดึกดำบรรพ์กว่าชนิดข้อมูลเชิงอุปนัยอีกหรือเปล่า?" มันทำให้ผมรู้สึกว่าควรเตือนตัวเองบ่อย ๆ ว่าอย่ามองสัจพจน์ Peano ว่าเป็นสิ่งที่ชัดเจนโดยเนื้อแท้ แต่มันก็เป็นแค่หนึ่งในแบบออกแบบเท่านั้น
  • สำหรับคำถามว่า "มีอะไรที่พื้นฐานกว่าชนิดข้อมูลเชิงอุปนัยไหม?" ผมคิดว่าจำนวนธรรมชาตินั้นดั้งเดิมกว่าชนิดข้อมูลเชิงอุปนัยเอง เพราะชนิดข้อมูลเชิงอุปนัยทั้งหมดสามารถสร้างได้จากจำนวนธรรมชาติและตัวสร้างชนิดพื้นฐานอีกไม่กี่ตัว (Π, Σ, =, Ω)
• ดูQ&A เกี่ยวกับทฤษฎีบท Kirby-Paris
• มีการแชร์วิดีโอเกี่ยวกับเรื่องความสอดคล้องของ PA ที่พิสูจน์ได้ภายใน PA เอง ลิงก์ YouTube
  • นี่เป็นจุดที่จำเป็นต้องอธิบายให้คนที่ไม่ใช่นักตรรกะเข้าใจ ตามทฤษฎีบทความไม่สมบูรณ์ลำดับที่สองของ Gödel ถ้า PA พิสูจน์ความสอดคล้องของตัวเองได้ PA ก็จะขัดแย้งในตัวเอง (และจะพิสูจน์อะไรก็ได้แม้แต่เรื่องเท็จ) วิดีโอนี้ไม่ได้พิสูจน์ว่า PA ขัดแย้งในตัวเอง แต่แสดงว่า PA สามารถพิสูจน์ "ความสอดคล้องของตัวเอง" ได้ในความหมายที่อ่อนกว่านั้น ถ้าไม่รู้พื้นฐานตรรกะอาจเข้าใจประเด็นนี้ได้ไม่ครบถ้วน แต่ก็น่าสนใจมากพออยู่ดี
• หัวข้อนี้ได้ 123 คะแนน แต่ตัวโพสต์ต้นฉบับบน SO กลับมีแค่อัปโหวต 11 ครั้ง
  • ใน Stack Overflow ต้องมี 15 คะแนนถึงจะโหวตบวกได้ คนเลยไม่ค่อยอยากโพสต์เพราะเรื่องชื่อเสียงด้วย และข้อจำกัด 15 คะแนนก็ดูเหมือนจะทำให้การอัปโหวตเกิดขึ้นน้อยลง
• แค่ computation อย่างเดียวพอไหม? จำนวนจริงที่คำนวณได้เป็นเพียงสับเซตของจำนวนจริงทั้งหมด
  • ผมคิดว่าชื่อ "จำนวนจริง" เองก็เป็นชื่อที่ชวนให้เข้าใจผิด เพราะมันอาจตีความได้ว่าเป็นอัตราส่วนทางกายภาพที่มีอยู่จริง เช่น ถ้าบอกว่า 180.255 ปอนด์ ก็หมายถึงอัตราส่วนทางกายภาพจริงระหว่างน้ำหนักของ Jones กับปอนด์มาตรฐาน อัตราส่วนแบบนี้ก็มีอยู่จริงทางกายภาพ ดังนั้นจำนวนจริงอาจตีความได้ว่าเป็นอัตราส่วนทางกายภาพ แต่ปัจจุบันคนมักมองตัวเลขเป็นแนวคิดนามธรรมที่แยกจากโลกจริง ซึ่งเป็นมุมมองแบบเพลโตนิยมอย่างหนึ่ง อย่างไรก็ตาม ในโลกจริง เราไม่สามารถวัดหรือแสดงอะไรได้ด้วยความละเอียดไม่สิ้นสุด เช่น การวัดที่แม่นยำเกิน 50 หลักนั้นเป็นไปไม่ได้เพราะข้อจำกัดของกลศาสตร์ควอนตัม ถ้าจะวัดวงโคจรของวัตถุในระบบสุริยะโดยไม่มีความคลาดเคลื่อน พอเกิน 50 หลักก็ต้องคิดถึงผลของมวลดาวฤกษ์ข้างเคียง เกิน 100 หลักก็ต้องจำลองทั้งกาแล็กซี สุดท้ายก็ต้องคำนึงถึงอิทธิพลทางกายภาพที่วัดจริงไม่ได้อยู่ดี ดังนั้นในโลกจริง คณิตศาสตร์ที่ทำได้มีเพียงแบบความละเอียดจำกัดเท่านั้น กล่าวคือ โดยหลักการแล้วทุกอย่างคำนวณได้ แต่เมื่อไปถึงอนันต์ โมเดลทางคณิตศาสตร์เองก็หมดความหมาย
  • แน่ใจหรือ? จริง ๆ แล้วแนวคิดที่ว่าแบบนับไม่ได้ (uncountable) มี "มากกว่า" เริ่มจากความเข้าใจผิด ดูคำอธิบายของผม ถ้าคุณยอมรับว่าแบบนับไม่ได้มีมากกว่า คุณก็ต้องรับจุดยืนที่ถกเถียงกันได้เกี่ยวกับ "การมีอยู่" ด้วย ดูการถกเถียงที่เกี่ยวข้อง ท้ายที่สุด ต่อให้เราไล่เหตุผลไปจนสุด เราก็ยังแทนทุกอย่างบนคอมพิวเตอร์ได้ แม้เพิ่มเซตขนาดใหญ่เข้าไปใน ZFC เราก็ยังสามารถเริ่มจาก PA แล้วอนุมานไปถึงข้อสรุปใด ๆ ได้ทั้งหมด ดังนั้นในทางปฏิบัติผมจึงมองว่า PA เพียงอย่างเดียวก็พอแล้ว ถ้ายังอยากได้อะไรที่โน้มน้าวกว่านี้ ผมแนะนำหนังสือ Gödel, Escher, Bach
  • วิธีคิดของผมต่างออกไปเล็กน้อย จำนวนจริงโดยทั่วไปอาจจัดการไม่ได้เลยไม่ว่าจะด้วยการคำนวณ การทำให้เป็นสัญลักษณ์ หรือการบันทึกในรูปแบบใดก็ตาม แต่ "ข้อความ" เกี่ยวกับจำนวนจริงกลับมักแสดงออกและคำนวณได้อย่างมีประโยชน์ Harvey Friedman หรือผู้เขียนบทความนี้เองก็ทำสิ่งที่น่าสนใจมากด้วยการสร้างค่าที่ซับซ้อนเกินคาดจากระบบที่เรียบง่าย (หมายเหตุ: เว็บไซต์ audiomulch เข้าไม่ได้)
  • ถ้าไม่มีการระบุเป้าหมายต่อท้ายคำว่า "พอ" คำถามนี้ก็คลุมเครือในเชิงนิยาม สิ่งสำคัญคือพอสำหรับอะไร
  • ผมคิดว่าคำถาม "แค่ computation อย่างเดียวพอไหม?" นั้นตั้งคำถามผิด แน่นอนว่าไม่พอ ถ้ามันพอจริง มุมมองของคนบางกลุ่มที่มองโลกเหมือนกลไกนาฬิกาที่เชื่อได้ง่าย ๆ ก็คงถูกต้องทั้งหมด แต่โลกจริงน่าสนใจและซับซ้อนกว่านั้นมาก