12 · ชนิดกับบทพิสูจน์
บทนี้ถามว่าเกิดอะไรขึ้นกับรางวัลเชิงปรัชญาที่เก่าแก่ที่สุด — ความแน่นอน — เมื่อบทพิสูจน์เองกลายเป็นสิ่งประดิษฐ์ที่ตรวจสอบได้ นี่คือการไต่สวนครั้งที่สี่ของภาค II สามบทก่อนหน้าถามว่าการคำนวณทำอะไรได้ ใช้เวลานานแค่ไหน และเคลื่อนอะไร
ความแน่นอนจะเหลืออะไร เมื่อบทพิสูจน์กลายเป็นสิ่งประดิษฐ์
ปี 1976 ทฤษฎีบทสี่สี (four-color theorem) ถูกพิสูจน์ด้วยโปรแกรมคอมพิวเตอร์ที่ไล่ตรวจการจัดวางแผนที่เกือบหนึ่งพันห้าร้อยแบบ จำนวนที่ไม่มีมนุษย์คนไหนไล่ด้วยมือไหว คนพิสูจน์คือ Kenneth Appel และ Wolfgang Haken บทที่ 03 นั่งอยู่กับแรงสั่นสะเทือนของคำตัดสินนั้นมาแล้ว: บทพิสูจน์ที่ยาวเกินกว่านักคณิตศาสตร์คนใดจะอ่านจบตั้งแต่ต้นจนจบ เกือบสามสิบปีต่อมา Georges Gonthier ปิดอีกคดีหนึ่งของทฤษฎีบทเดียวกัน การทำให้เป็นรูปนัย (formalization) ของเขา เสร็จใน proof assistant ชื่อ Coq และตีพิมพ์เป็น "Formal Proof — The Four-Color Theorem" (Notices of the American Mathematical Society 55, 2008: 1382–1393) ไม่ได้รันข้อโต้แย้งของ Appel กับ Haken ซ้ำเฉยๆ มันสร้างบทพิสูจน์ทั้งชิ้นขึ้นใหม่ ทั้ง combinatorics และการไล่ตรวจกรณี ให้เป็นลำดับขั้นตอนที่ kernel (แกนตรวจสอบ) เล็กๆ ที่ไว้ใจได้รับรองความถูกต้อง และคนคนเดียวตรวจได้ทีละบรรทัดในหลักการ ทฤษฎีบทที่เคยเป็นสัญลักษณ์ของบทพิสูจน์ที่วิ่งพ้นความเข้าใจของมนุษย์ กลายมาเป็นทฤษฎีบท ในมือของ Gonthier ที่แสดงว่าความเข้าใจถูกแทนที่ได้ด้วยบางอย่างที่เข้มงวดกว่าผู้อ่านมนุษย์คนใด: เครื่องจักรที่ไม่อ่านผ่านๆ
สิ่งที่ทำให้ kernel ของ Gonthier ไว้ใจได้คือความสอดคล้อง (correspondence) ที่ถูกค้นพบ ไม่ใช่ถูกออกแบบ และค้นพบซ้ำถึงสองรอบ Haskell Curry สังเกตในปี 1934 ว่าชนิด (type) ที่กำกับ combinator ในตรรกะเชิงการจัด (combinatory logic) อ่านได้ในฐานะ axiom scheme ของตรรกะเชิงเงื่อนไขแบบสัญชานนิยม (intuitionistic) และในปี 1958 ว่าส่วนหนึ่งของระบบพิสูจน์แบบ Hilbert ตรงกับส่วนหนึ่งของตรรกะเชิงการจัดที่มีชนิดกำกับ สามทศวรรษถัดมา William Howard ทำการเทียบเคียงนั้นให้แม่นยำ โดยไม่รู้ประวัติทั้งหมดของ Curry เขาส่งต้นฉบับเวียนอ่านในปี 1969 และมันได้ตีพิมพ์ในที่สุดเป็น "The Formulae-as-Types Notion of Construction" ใน festschrift ปี 1980 ที่ทำขึ้นให้ Curry โดยมี Jonathan Seldin และ J. Roger Hindley เป็นบรรณาธิการ Howard แสดงว่าบทพิสูจน์ที่เขียนในสไตล์การนิรนัยธรรมชาติ (natural deduction) ที่ Gerhard Gentzen เสนอไว้ในปี 1935 กับโปรแกรมที่เขียนในแคลคูลัสแลมบ์ดาที่มีชนิดอย่างง่าย (simply typed lambda calculus) คือวัตถุชิ้นเดียวกันที่มองจากคนละด้าน: ประพจน์คือชนิด บทพิสูจน์ของประพจน์คือโปรแกรมของชนิดนั้น และการลดรูปบทพิสูจน์ — ตัดทางอ้อมทิ้ง — คือการรันโปรแกรม N. G. de Bruijn คิดไอเดียรุ่นเดียวกันนี้ขึ้นเองในเวลาไล่เลี่ยกันแทบพอดี และวางมันลงในระบบ Automath ของเขา ก่อนที่เขากับ Howard จะรู้ว่าอีกฝ่ายทำเรื่องเดียวกันอยู่ นักวิจัยสามคน คนหนึ่งมาจากตรรกศาสตร์ คนหนึ่งมาจาก combinator คนหนึ่งมาจากตัวตรวจสอบบทพิสูจน์อัตโนมัติ ต่างเจอรอยต่อเดียวกันครั้งแล้วครั้งเล่า — หลักฐานที่หนักที่สุดที่หนังสือเล่มนี้มี สำหรับข้อกล่าวอ้างของมันเองว่าปรัชญากับการคำนวณคือโครงการเดียวที่ถูกค้นพบซ้ำ ไม่ใช่สองโครงการที่ยืมของกัน
ความสอดคล้องนี้คือการแก้แค้นของความนอกรีตที่มีอายุนับศตวรรษ บทความปี 1908 ของ L. E. J. Brouwer เรื่อง "The Unreliability of the Logical Principles" ปฏิเสธกฎแห่งไตรวินิจฉัย (law of excluded middle) — ข้อกล่าวอ้างที่ว่าทุกประพจน์เป็นจริงหรือเท็จอย่างใดอย่างหนึ่งเสมอ — สำหรับคณิตศาสตร์ที่วัตถุของมันเป็นสิ่งสร้างทางจิต ไม่ใช่ข้อเท็จจริงที่เป็นอิสระจากจิต ต่อยอดจากโครงการสัญชานนิยม (intuitionism) ที่เขาเปิดไว้ในวิทยานิพนธ์ปี 1907 ตลอดศตวรรษที่ 20 เกือบทั้งศตวรรษ ข้อปฏิเสธนี้ดูเหมือนรสนิยมของคนกลุ่มน้อย เป็นความลังเลใจที่นักคณิตศาสตร์ผู้ทำงานจริงมองข้ามได้อย่างปลอดภัย Curry–Howard อธิบายว่าทำไมมันเลิกเป็นทางเลือกในโลกของ proof assistant: บทพิสูจน์เชิงสร้าง (constructive proof) ที่ว่าบางสิ่งมีอยู่ ภายใต้ความสอดคล้องนี้ ต้องเป็นโปรแกรมที่สร้างสิ่งนั้นออกมา ส่วนบทพิสูจน์เชิงคลาสสิก (classical proof) แบบพิสูจน์โดยข้อขัดแย้ง — สมมติว่าไม่มีวัตถุนั้นอยู่ อนุมานความขัดแย้ง สรุปว่ามันมีอยู่ — ไม่ตรงกับโปรแกรมใดเลย เพราะมันไม่บอกวิธีสร้างอะไรสักอย่าง Coq, Agda และ Lean ที่รากฐานคือการสร้าง (implementation) ของทฤษฎีชนิดสัญชานนิยม (intuitionistic type theory) ไม่ใช่เพราะภักดีทางปรัชญาต่อ Brouwer แต่เพราะมีแต่ส่วนเชิงสร้างเท่านั้นที่คืนโค้ดที่รันได้กลับมาให้ สัญชานนิยมกลายเป็นวิศวกรรมที่แบกน้ำหนักจริง พอดีตรงจุดที่มันเลิกถูกขอให้ปกป้องตัวเองเชิงปรัชญา
พอกลไกนั้นมีอยู่ คณิตศาสตร์ก็ยื่นบทพิสูจน์ที่ยากที่สุดและยาวที่สุดของตัวเองให้มันตรวจ Thomas Hales พิสูจน์ข้อคาดการณ์ของ Kepler (Kepler conjecture) สำเร็จในปี 1998 ว่าไม่มีวิธีอัดทรงกลมขนาดเท่ากันแบบใดแน่นไปกว่ากองผลไม้ที่พ่อค้าเรียงไว้ แต่ข้อโต้แย้ง 250 หน้านั้นเป็นแบบดั้งเดิมครึ่งหนึ่ง ใช้คอมพิวเตอร์ช่วยอีกครึ่งหนึ่ง กินเวลาผู้ตรวจทานสิบสองคนไปสี่ปี และจบลงที่ความมั่นใจเพียง 99 เปอร์เซ็นต์ว่าถูกต้อง Hales ตอบด้วยการเปิดโครงการ Flyspeck ในปี 2003 เพื่อสร้างทุกขั้นตอนขึ้นใหม่ภายใน HOL Light และ Isabelle งานรูปนัยเสร็จในปี 2014 ตรวจสอบและตรวจซ้ำโดยอิสระในปีเดียวกัน ตีพิมพ์เป็น "A Formal Proof of the Kepler Conjecture" (Forum of Mathematics, Pi, 2017) บทตั้ง (lemma) หลายหมื่นข้อของ Flyspeck วางอยู่บน kernel ที่เล็กพอให้คนหยิบมือเดียวตรวจได้ครบทุกบรรทัด แทนผู้ตรวจทานสิบสองคนที่สุ่มอ่านได้เพียงบางส่วนของบทพิสูจน์ที่ยาวเกินกว่าจะอ่านจบ mathlib ของ Lean คลังที่โตขึ้นทุกวันและชุมชนช่วยกันตรวจ ยืนบนรากฐานเดียวกัน วันนี้มันทำผลลัพธ์ทั่วทั้งคณิตศาสตร์ให้เป็นรูปนัยไปพร้อมกับที่ผลลัพธ์เหล่านั้นถูกพิสูจน์ "เรื่องนี้ถูกตรวจสอบแล้วหรือยัง" จึงเลิกเป็นเรื่องของชื่อเสียง และกลายเป็นคำถามที่เครื่องจักรตอบได้
Vladimir Voevodsky ดันตัวรากฐานเองไปอีกขั้น Homotopy Type Theory: Univalent Foundations of Mathematics เล่มรวมที่เขียนโดยโปรแกรมของ Institute for Advanced Study ที่เขาเป็นผู้นำ ตีพิมพ์ปี 2013 เสนอให้อ่านชนิด (type) ไม่ใช่เซตเปล่าๆ แต่เป็นปริภูมิ (space) และอ่านบทพิสูจน์ความเท่ากันระหว่างสมาชิกเป็นเส้นทางระหว่างจุด ภายใต้สัจพจน์เอกค่า (univalence axiom) ของ Voevodsky โครงสร้างที่ isomorphic กันถือเป็นสิ่งเดียวกันได้ คำว่า "เท่ากัน" คำที่เก่าแก่ที่สุดและถูกใช้ผิดหนักที่สุดในคณิตศาสตร์ จึงได้ความหมายที่แม่นยำและตรวจสอบได้ ความหมายที่มันไม่เคยมีจริงๆ มาก่อน
ไม่มีอะไรในนี้ส่งมอบความแน่นอนแบบที่ Hilbert ต้องการในปี 1930 การรับประกันของ proof assistant แข็งแรงเท่า kernel ของมันเท่านั้น kernel วางอยู่บนคอมไพเลอร์ คอมไพเลอร์วางอยู่บนฮาร์ดแวร์ และฮาร์ดแวร์พังได้ — การถอยกลับไม่รู้จบ (regress) อันเดียวกับที่ Wittgenstein กดดันกฎใดๆ ที่อ้างว่าตีความตัวเองได้ และอันเดียวกับที่บทที่ 03 ยกขึ้นมาเป็นปัญหาเก็ตติเยร์ (Gettier problem) ของเซนเซอร์และไปป์ไลน์ สิ่งที่ Curry–Howard ส่งมอบให้แทนคือความแน่นอนที่ถูกออกแบบใหม่เป็นงบประมาณ: แทนที่จะไว้ใจข้อโต้แย้ง 250 หน้ากับผู้ตรวจทานที่เหนื่อยล้าสิบสองคน ให้ไว้ใจ kernel ไม่กี่พันบรรทัด ระบุให้ชัดว่าอะไรต้องพังบทพิสูจน์จึงจะผิด แล้วให้เท่านั้นเป็นความสงสัยที่เหลืออยู่ทั้งหมด ปรัชญาอยากให้บทพิสูจน์ปิดข้อโต้แย้งเด็ดขาดครั้งเดียวจบ ข้อเสนอโต้กลับของการคำนวณคือบทพิสูจน์ที่บอกได้แม่นยำว่าข้อโต้แย้งที่เหลือนั้นเล็กแค่ไหน
เชื่อมโยง
บทที่ 01 แนะนำความสอดคล้อง Curry–Howard (Curry–Howard correspondence) ในฐานะสนธิสัญญาระหว่างสองสาขาวิชาของบทตรรกศาสตร์ บทนี้ทำให้มันครบ บทที่ 03 คือจุดที่ทฤษฎีบทสี่สีก่อแรงสั่นสะเทือนเชิงญาณวิทยาครั้งแรก บทนี้คือคำตอบ บทที่ 09 ให้ผลลัพธ์เรื่องความไม่สมบูรณ์ที่ proof assistant ต้องอยู่ข้างใน ไม่ใช่หนีพ้น Kolmogorov complexity ในบทที่ 11 วัดความยาวของบทพิสูจน์ แบบเดียวกับที่บทนี้วัดความน่าเชื่อถือของมัน
คำถามที่ยังเปิดอยู่
ถ้า kernel เล็กพอให้คนคนเดียวตรวจได้ การถอยกลับไม่รู้จบของการไว้ใจตัวตรวจสอบหยุดลงจริงหรือ หรือแค่ถูกย่อจนเหลือจุดเชื่อมที่สั้นพอจะมองข้าม สัจพจน์เอกค่า (univalence) ยุติความหมายของ "โครงสร้างเดียวกัน" ให้คณิตศาสตร์ทั้งวงการ หรือยุติได้แค่ในบ้านของทฤษฎีชนิดเอง และตอนนี้ที่ mathlib ของ Lean ตรวจผลลัพธ์ใหม่ไปพร้อมกับที่มันถูกพิสูจน์ ความรู้ทางคณิตศาสตร์ยังต้องการชุมชนมนุษย์ของผู้ตรวจทานอยู่หรือไม่ หรือต้องการแค่ชุมชนที่ตัดสินว่าทฤษฎีบทไหนคุ้มค่าแก่การพิสูจน์ตั้งแต่แรก
อ่านต่อ
- Jean-Yves Girard, Yves Lafont, and Paul Taylor, Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7 (Cambridge: Cambridge University Press, 1989) — free edition at paultaylor.eu/stable/prot.pdf.
- William Howard, "The Formulae-as-Types Notion of Construction," in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, ed. J. P. Seldin and J. R. Hindley (New York: Academic Press, 1980), 479–490; Georges Gonthier, "Formal Proof — The Four-Color Theorem," Notices of the American Mathematical Society 55 (2008): 1382–1393 — ams.org/notices/200811/tx081101382p.pdf.
- Stanford Encyclopedia of Philosophy, "Intuitionism in the Philosophy of Mathematics" — plato.stanford.edu/entries/intuitionism.