01 · ตรรกศาสตร์
การไต่สวนแรกของภาค I เปิดที่สาขาวิชาซึ่งยืนใกล้ห้องพิจารณาคดีที่สุด — ตรรกศาสตร์คือจุดที่ปรัชญากับการคำนวณยังเป็นครอบครัวเดียวกัน ไม่แตกแยก อยู่ชั่วขณะหนึ่ง
กฎแห่งความคิดกลายเป็นเครื่องจักร แล้วเกิดอะไรขึ้น
วันที่ 10 สิงหาคม 1937 นักศึกษาปริญญาโทวัยยี่สิบเอ็ดปีชื่อโคลด แชนนอน ยื่นวิทยานิพนธ์ต่อภาควิชาวิศวกรรมไฟฟ้าของ MIT ข้อเสนอเรียบง่ายจนแทบน่าอาย: พีชคณิตบูล (Boolean algebra) ที่จอร์จ บูลคิดขึ้นในปี 1854 เพื่ออธิบายการให้เหตุผลของมนุษย์ — พีชคณิตของจริงกับเท็จ ของ "และ" "หรือ" และ "ไม่" — ก็คือพีชคณิตของสวิตช์ที่ต่ออนุกรมและขนาน สวิตช์ปิดคือ 1 สวิตช์เปิดคือ 0 สวิตช์สองตัวต่ออนุกรมคำนวณ AND ต่อขนานคำนวณ OR แชนนอนแสดงว่าวงจรรีเลย์ใดๆ ลดรูปได้แบบเดียวกับที่นักตรรกวิทยาลดรูปสูตร และสูตรบูลใดๆ ก็ประกอบขึ้นจากรีเลย์ได้ ฉบับตีพิมพ์ "A Symbolic Analysis of Relay and Switching Circuits" (Transactions of the American Institute of Electrical Engineers 57, 1938: 713–723) ทำให้นักจิตวิทยาฮาวเวิร์ด การ์ดเนอร์ เรียกมันในปี 1985 ว่า "อาจเป็นวิทยานิพนธ์ปริญญาโทที่สำคัญที่สุด และมีชื่อเสียงที่สุด ของศตวรรษ" ("possibly the most important, and also the most famous, master's thesis of the century") (History of Information) สองพันปีที่ผ่านมา ตรรกศาสตร์เป็นคำอธิบายความคิด หลังแชนนอน มันเป็นแผนผังการเดินสายไฟด้วย
การปะทะกันนั้นไม่ใช่เส้นตรง และเส้นตรงที่เล่ากันมาก็ผิด Prior Analytics ของอริสโตเติลตรึงรูปร่างของตรรกศาสตร์ไว้สองพันปี: ซิลโลจิซึม (syllogism) เครื่องจักรสามบรรทัดเป๊ะๆ — "ชาวกรีกทุกคนตาย โสกราตีสเป็นชาวกรีก ฉะนั้นโสกราตีสตาย" — สมเหตุสมผลด้วยรูปแบบล้วนๆ ไม่ว่าถ้อยคำจะหมายถึงอะไร มันรัดกุม และมันก็เกือบแข็งตัว นักตรรกวิทยาใช้เวลาหลายศตวรรษไล่จัดหมวดว่ารูปแบบซิลโลจิซึมแบบไหนสมเหตุสมผล แทนที่จะขยายวิธีการ An Investigation of the Laws of Thought (1854) ของบูลทุบความแข็งตัวนั้นด้วยพีชคณิต: ประพจน์กลายเป็นสมการเหนือ 0 กับ 1 "และ" คือการคูณ "หรือ" คือการบวก อนุมานคือการแก้สมการ มองย้อนกลับไป นี่ดูเหมือนการค้นพบซ้ำความฝันของไลบ์นิซในศตวรรษที่สิบเจ็ดเรื่อง calculus ratiocinator — แคลคูลัสสำหรับยุติข้อโต้แย้ง — และชวนให้เล่าเป็นมรดกที่สืบทอดกันมาไม่ขาดสาย แต่ไม่ใช่ ตอนที่ Laws of Thought ตีพิมพ์ บูลไม่รู้ว่าไลบ์นิซคาดการณ์พีชคณิตของเขาไว้ล่วงหน้า เขารู้ทีหลังจากโรเบิร์ต เลสลี เอลลิส และมีรายงานว่าเขายินดี ไม่ใช่ห่อเหี่ยว ที่พบว่าไลบ์นิซเคยเห็นแวบหนึ่งของดินแดนเดียวกันก่อนหน้าสองศตวรรษ (สารานุกรมปรัชญาสแตนฟอร์ด (SEP), Leibniz's Influence on 19th-Century Logic) กอทท์ล็อบ เฟรเกกลับกัน เขาอ้างเสื้อคลุมของไลบ์นิซอย่างจงใจตอนสร้างชั้นถัดไป ตะเข็บระหว่างสองสาขาวิชาถูกค้นพบใหม่บ่อยพอๆ กับที่ถูกส่งต่อ — หลักฐานอีกครั้งว่าทั้งคู่มาถึงความคิดเดียวกัน เพราะต่างขุดพื้นดินผืนเดียวกันโดยอิสระจากกัน ไม่ใช่ส่งคบเพลิงเล่มเดียวจากมือสู่มือ
Begriffsschrift (1879) ของเฟรเกให้หลักการที่สองที่บทนี้ต้องการ: การบ่งปริมาณ (quantification) พีชคณิตของบูลพูดว่า "มนุษย์บางคนฉลาด" ได้อย่างเงอะงะ ในฐานะข้อเท็จจริงเรื่องคลาสเท่านั้น มันไม่มีทางสะอาดที่จะแสดง "สำหรับทุก x ถ้า x เป็นมนุษย์ x ตาย" เป็นโครงสร้างเดียวที่หยิบมาจัดการได้ โดยมีตัวแปรวิ่งผ่าน เฟรเกสร้างสิ่งนั้นพอดี — สัญกรณ์ที่ต้องยอมรับว่าไม่เหมือนสัญลักษณ์ ∀ กับ ∃ ที่ใช้กันทุกวันนี้เลย แต่แสดงออกได้เทียบเท่ากัน ในนั้นความเป็นสากลกับการมีอยู่กลายเป็นตัวดำเนินการที่ผูกตัวแปรไว้ในสูตร การเคลื่อนไหวเดียวนี้เองที่ทำให้ตรรกศาสตร์กลืนการให้เหตุผลทั้งหมดที่คณิตศาสตร์ทั่วไปใช้ ไม่ใช่แค่เศษเสี้ยวซิลโลจิซึม — และมันเป็นบรรพบุรุษของตัวแปรในทุกภาษาโปรแกรมด้วย ไม่ใช่เรื่องบังเอิญ: ช่องว่างที่ตัวบ่งปริมาณ (quantifier) หรือลูป for วิ่งไล่ผ่าน
หลักการที่สามคือรอยแยกที่วงจรของแชนนอนไม่ได้แก้: การพิสูจน์ไม่ใช่ความจริง ปี 1929 ในวิทยานิพนธ์ปริญญาเอกภายใต้ฮันส์ ฮาห์น เคิร์ท เกอเดิลพิสูจน์ว่าตรรกศาสตร์อันดับหนึ่งสมบูรณ์ (completeness) — ตอบคำถามที่ฮิลแบร์ทกับอัคเคอร์มันน์ตั้งไว้เมื่อปีก่อนหน้า เขาแสดงว่าทุกสูตรที่สมเหตุสมผลเชิงตรรกะในตรรกศาสตร์อันดับหนึ่งมีบทพิสูจน์ในระบบรูปนัย (formal system) และ (คุณสมบัติคู่กันคือความสมเหตุสมผลเชิงตรรกะ (soundness)) ทุกสูตรที่พิสูจน์ได้ก็สมเหตุสมผล สองปีต่อมา ชายคนเดียวกันพลิกอีกด้านของเหรียญให้ดู: ระบบรูปนัยที่สมนัยกันเองใดๆ ที่อุดมพอจะบรรจุเลขคณิตพื้นฐาน ต้องไม่สมบูรณ์ — มันบรรจุข้อความเลขคณิตที่เป็นจริงแต่พิสูจน์ไม่ได้ ตัวตรรกศาสตร์อันดับหนึ่งเองสมบูรณ์ เลขคณิตที่สร้างทับบนมันไม่สมบูรณ์ ผลลัพธ์สองอันนี้ไม่ขัดกัน เพราะตอบคนละคำถามเกี่ยวกับคนละระบบ แต่รวมกันแล้วมันหมายถึงบางอย่างที่แน่นอนและถาวร: การทำให้การอนุมานเป็นกลไก (ความสมเหตุสมผลเชิงตรรกะและความสมบูรณ์ของตรรกศาสตร์) ไม่ใช่โครงการเดียวกับการทำให้ความจริงทางคณิตศาสตร์ทั้งหมดเป็นกลไก (ซึ่งเกอเดิลแสดงแล้วว่าทำให้เสร็จไม่ได้) วงจรตัดสินได้ว่ารูปแบบของข้อโต้แย้งสมเหตุสมผลไหม มันตัดสินไม่ได้ว่าทุกข้อความจริงเกี่ยวกับตัวเลขมีบทพิสูจน์ไหม เพราะบางข้อความไม่มี
หลักการที่สี่เปลี่ยนตรรกศาสตร์จากวิธีตรวจข้อโต้แย้ง เป็นวิธีเขียนโปรแกรม สโลแกนปี 1979 ของโรเบิร์ต โควาลสกี "Algorithm = Logic + Control" (Communications of the ACM 22, no. 7: 424–436) เสนอให้ผ่ากระบวนวิธีใดๆ ออกเป็นสองส่วน: ส่วนตรรกะ — สิ่งที่เป็นจริง ระบุแบบประกาศ (declarative) — กับส่วนควบคุม — เครื่องจักรค้นหามันอย่างไร อาแล็ง กอลเมโรกับฟีลิป รูแซลสร้างการพิสูจน์แนวคิดไว้ก่อนแล้วที่มาร์แซย์ ฤดูร้อนปี 1972 คิดกลยุทธ์การค้นหาแบบบนลงล่างร่วมกับโควาลสกีเองระหว่างที่เขาไปเยือนจากเอดินบะระ: Prolog ภาษาที่โปรแกรมหนึ่งคือชุดอนุประโยคเชิงตรรกะโดยแท้ และการรันโปรแกรมคือการขอให้เครื่องพิสูจน์ทฤษฎีบทจากอนุประโยคเหล่านั้นด้วย resolution (Kowalski, "The Early Years of Logic Programming") การเขียนข้อกำหนดกับการเขียนโปรแกรมที่รันได้ เป็นการกระทำเดียวกันในทางรูปนัยเป็นครั้งแรก
หลักการที่ห้าคือการจับมือที่ลึกที่สุดระหว่างสองศาลตลอดทั้งเล่ม: ความสอดคล้อง Curry–Howard ปี 1934 แฮสเคลล์ เคอร์รีสังเกตว่าชนิด (type) ที่กำหนดให้ตัวรวมของตรรกะเชิงการจัด (combinatory logic) ตรงกันทีละพจน์กับสัจพจน์ของตรรกะสัญชานนิยม (intuitionistic logic) เชิงเงื่อนไข ("Functionality in Combinatory Logic," PNAS 20) วิลเลียม ฮาวเวิร์ดขยายข้อสังเกตนี้ไปถึงการนิรนัยธรรมชาติ (natural deduction) เต็มรูปแบบและแคลคูลัสแลมบ์ดา (lambda calculus) ในปี 1969 แม้บทความที่ทำให้มันมีชื่อเสียง "The Formulae-as-Types Notion of Construction" จะรอถึงปี 1980 จึงได้ตีพิมพ์ ในหนังสือรวมบทความเชิดชูเกียรติเคอร์รี ความสอดคล้องนี้พูดแรงกว่าการเปรียบเทียบ: ประพจน์หนึ่งคือชนิดหนึ่ง บทพิสูจน์ของประพจน์นั้นคือโปรแกรมของชนิดนั้น และการลดรูปบทพิสูจน์ — ตัดทางอ้อมทิ้ง — คือการรันโปรแกรมไปหนึ่งขั้น ตรรกศาสตร์กับการคำนวณไม่ใช่สองสิ่งที่คล้ายกัน ภายใต้ Curry–Howard สำหรับกลุ่มระบบที่กว้างและกำลังขยายตัว มันคือสิ่งเดียวกันที่ถูกอธิบายสองครั้ง proof assistant (ตัวช่วยพิสูจน์) สมัยใหม่ (Coq, Agda, Lean) เป็นภาษาโปรแกรมโดยแท้จริง ที่โปรแกรมที่พิมพ์ถูกต้อง (well-typed) คือใบรับรองว่าทฤษฎีบทหนึ่งเป็นจริง
ผู้คน โดยย่อ บูลเรียนรู้ด้วยตัวเอง เป็นครูใหญ่ในลินคอล์นก่อนได้เก้าอี้ศาสตราจารย์ที่คอร์ก เฟรเกใช้ชีวิตการทำงานเกือบทั้งชีวิตโดยไม่มีใครอ่านผลงาน ตรรกะของเขาเข้าตาคนก็เพราะเบอร์ทรันด์ รัสเซลล์เขียนจดหมายถึงเขาในปี 1902 เพื่อชี้ข้อขัดแย้งในนั้น เคิร์ท เกอเดิลทำงานอย่างโดดเดี่ยวเกือบสิ้นเชิงในเวียนนาและต่อมาที่พรินซ์ตัน ระแวงจนอดอาหารตัวเองตายในปีสุดท้ายของชีวิต แฮสเคลล์ เคอร์รีกับวิลเลียม ฮาวเวิร์ดแทบไม่เป็นที่รู้จักนอกภาควิชาตรรกศาสตร์ — เหมาะสมดี สำหรับความสอดคล้องที่การตีพิมพ์ของมันเองล่าช้าไปสิบเอ็ดปี ราวกับความคิดในบทนี้ติดนิสัยมาถึงก่อนที่ใครจะพร้อมพิมพ์มัน
เชื่อมโยง
บทที่ 00 คือบทแม่ของบทนี้: สายพานเฟรเก–รัสเซลล์–ฮิลแบร์ท–เกอเดิล–ทัวริงเล่าไว้ครบถ้วนที่นั่น บทนี้อยู่แค่ในเรื่องทะเลาะกันเองในครอบครัวตรรกศาสตร์ บทที่ 09 ย้อนกลับไปปี 1936 เพื่อถามว่าข้อตั้ง Church–Turing อ้างอะไรกันแน่ บทที่ 11 เป็นเจ้าของเรื่องที่แชนนอนตัดความหมายออกจากสารสนเทศในภายหลัง ปี 1948 แชนนอนของบทนี้หยุดที่ปี 1937 ตรงที่วงจรมาบรรจบกับบูล และยังไม่มีใครพูดถึงความหมายเลย บทที่ 12 พาความสอดคล้อง Curry–Howard ลงไปจนสุดความลึก ผ่านตรรกะสัญชานนิยมของบราวเวอร์และคณิตศาสตร์เชิงกลไก
คำถามที่ยังเปิดอยู่
ถ้าบูลกับไลบ์นิซ และภายหลังเฟรเก ต่างเจอตะเข็บเดียวกันโดยอิสระจากกันครั้งแล้วครั้งเล่า ตรรกศาสตร์ที่แปลงเป็นคณิตศาสตร์เป็นสิ่งที่มนุษยชาติต้องค้นพบอยู่ดี เมื่อพีชคณิตกับความสงสัยในซิลโลจิซึมมาบรรจบกันพอดีหรือเปล่า — หรือความบังเอิญนั้นเองก็ไม่แน่นอน และถ้าบทพิสูจน์กับโปรแกรมเป็นวัตถุเดียวกันจริงภายใต้ Curry–Howard สาขาไหนควรนับว่าเป็นฝ่ายค้นพบอีกฝ่าย: การคำนวณค้นพบว่าตัวเองแอบทำตรรกศาสตร์อยู่ หรือตรรกศาสตร์ค้นพบว่าตัวเองแอบรันได้
อ่านต่อ
- Ernest Nagel and James R. Newman, Gödel's Proof, New York University Press, 1958 — ยังคงเป็นคำอธิบายสั้นที่ชัดเจนที่สุด ว่าความสมบูรณ์กับความไม่สมบูรณ์บอกอะไรและไม่บอกอะไร
- Claude Shannon, "A Symbolic Analysis of Relay and Switching Circuits," Transactions of the American Institute of Electrical Engineers 57 (1938): 713–723; William Howard, "The Formulae-as-Types Notion of Construction," in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, eds. J.P. Seldin and J.R. Hindley, Academic Press, 1980 (เขียนขึ้นปี 1969)
- Gödel's Incompleteness Theorems, SEP