01 · Logic
01 · ตรรกศาสตร์
This is Part I's first hearing, the discipline standing closest to the courtroom itself — logic is where philosophy and computing were still, for a while, one undivided family.
การไต่สวนแรกของภาค I เปิดที่สาขาวิชาซึ่งยืนใกล้ห้องพิจารณาคดีที่สุด — ตรรกศาสตร์คือจุดที่ปรัชญากับการคำนวณยังเป็นครอบครัวเดียวกัน ไม่แตกแยก อยู่ชั่วขณะหนึ่ง
What happened when the laws of thought became a machine?
กฎแห่งความคิดกลายเป็นเครื่องจักร แล้วเกิดอะไรขึ้น
On 10 August 1937, a twenty-one-year-old graduate student named Claude Shannon submitted a master's thesis to MIT's electrical engineering department. Its claim was almost embarrassingly simple to state: the algebra George Boole had invented in 1854 to describe human reasoning — an algebra of true and false, of "and," "or," and "not" — was also the algebra of switches wired in series and parallel. A closed switch is 1; an open switch is 0. Two switches in series compute AND; two in parallel compute OR. Shannon showed that any relay circuit could be simplified the way a logician simplifies a formula, and that any Boolean formula could, in turn, be built out of relays. The published version, "A Symbolic Analysis of Relay and Switching Circuits" (Transactions of the American Institute of Electrical Engineers 57, 1938: 713–723), led the psychologist Howard Gardner, in 1985, to call it "possibly the most important, and also the most famous, master's thesis of the century" (History of Information). Logic had been a description of thought for two thousand years. After Shannon, it was also a wiring diagram.
วันที่ 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) สองพันปีที่ผ่านมา ตรรกศาสตร์เป็นคำอธิบายความคิด หลังแชนนอน มันเป็นแผนผังการเดินสายไฟด้วย
That collision was not a straight line, and the straight line usually told is wrong. Aristotle's Prior Analytics had fixed logic's shape for two millennia: the syllogism, a machine of exactly three lines — "All Greeks are mortal; Socrates is a Greek; therefore Socrates is mortal" — valid by form alone, regardless of what the words meant. It was rigorous, and it was also nearly frozen; logicians spent centuries cataloguing which syllogistic figures were valid rather than extending the method. Boole's An Investigation of the Laws of Thought (1854) broke the freeze by algebraizing it: propositions became equations over 0 and 1, "and" became multiplication, "or" became addition, and inference became solving. This looks, in hindsight, like a rediscovery of Leibniz's seventeenth-century dream of a calculus ratiocinator — a calculus for settling arguments — and it is tempting to tell the story as an unbroken inheritance. It was not. Boole did not know of Leibniz's anticipations of his algebra when Laws of Thought appeared; he learned of them afterward, from Robert Leslie Ellis, and was reportedly delighted rather than deflated to find Leibniz had glimpsed the same terrain two centuries earlier (SEP, Leibniz's Influence on 19th-Century Logic). Gottlob Frege, by contrast, did claim Leibniz's mantle deliberately when he built the next floor. The seam between the two disciplines was rediscovered at least as often as it was handed down — evidence, again, that both keep arriving at the same idea because they are excavating the same ground independently, not passing a single torch hand to hand.
การปะทะกันนั้นไม่ใช่เส้นตรง และเส้นตรงที่เล่ากันมาก็ผิด 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) กอทท์ล็อบ เฟรเกกลับกัน เขาอ้างเสื้อคลุมของไลบ์นิซอย่างจงใจตอนสร้างชั้นถัดไป ตะเข็บระหว่างสองสาขาวิชาถูกค้นพบใหม่บ่อยพอๆ กับที่ถูกส่งต่อ — หลักฐานอีกครั้งว่าทั้งคู่มาถึงความคิดเดียวกัน เพราะต่างขุดพื้นดินผืนเดียวกันโดยอิสระจากกัน ไม่ใช่ส่งคบเพลิงเล่มเดียวจากมือสู่มือ
Frege's Begriffsschrift (1879) is the second principle this chapter needs: quantification. Boole's algebra could say "some men are wise" only clumsily, as a fact about classes; it had no clean way to express "for every x, if x is a man, x is mortal" as a single manipulable structure with a variable running through it. Frege built exactly that — a notation, admittedly nothing like the ∀ and ∃ symbols used today, but expressively equivalent to them, in which generality and existence become operators binding a variable inside a formula. This is the single move that let logic swallow the reasoning used throughout ordinary mathematics, not just its syllogistic fragment — and it is also, not incidentally, the ancestor of the variable in every programming language: a slot that a quantifier, or a for loop, ranges over.
Begriffsschrift (1879) ของเฟรเกให้หลักการที่สองที่บทนี้ต้องการ: การบ่งปริมาณ (quantification) พีชคณิตของบูลพูดว่า "มนุษย์บางคนฉลาด" ได้อย่างเงอะงะ ในฐานะข้อเท็จจริงเรื่องคลาสเท่านั้น มันไม่มีทางสะอาดที่จะแสดง "สำหรับทุก x ถ้า x เป็นมนุษย์ x ตาย" เป็นโครงสร้างเดียวที่หยิบมาจัดการได้ โดยมีตัวแปรวิ่งผ่าน เฟรเกสร้างสิ่งนั้นพอดี — สัญกรณ์ที่ต้องยอมรับว่าไม่เหมือนสัญลักษณ์ ∀ กับ ∃ ที่ใช้กันทุกวันนี้เลย แต่แสดงออกได้เทียบเท่ากัน ในนั้นความเป็นสากลกับการมีอยู่กลายเป็นตัวดำเนินการที่ผูกตัวแปรไว้ในสูตร การเคลื่อนไหวเดียวนี้เองที่ทำให้ตรรกศาสตร์กลืนการให้เหตุผลทั้งหมดที่คณิตศาสตร์ทั่วไปใช้ ไม่ใช่แค่เศษเสี้ยวซิลโลจิซึม — และมันเป็นบรรพบุรุษของตัวแปรในทุกภาษาโปรแกรมด้วย ไม่ใช่เรื่องบังเอิญ: ช่องว่างที่ตัวบ่งปริมาณ (quantifier) หรือลูป for วิ่งไล่ผ่าน
The third principle is the split Shannon's circuits do not resolve: proof is not truth. In 1929, in his doctoral dissertation under Hans Hahn, Kurt Gödel proved first-order logic complete — answering a question Hilbert and Ackermann had posed the year before, he showed that every logically valid formula of first-order logic has a formal proof, and (the companion property, soundness) that every provable formula is valid. Two years later, the same man showed the coin's other face: any consistent formal system rich enough to contain elementary arithmetic must be incomplete — it contains true arithmetical statements it cannot prove. First-order logic itself is complete; arithmetic built on top of it is not. The two results are not in tension, because they answer different questions about different systems, but together they mean something exact and permanent: mechanizing inference (soundness and completeness for logic) is not the same project as mechanizing all of mathematical truth (which Gödel showed cannot be finished). A circuit can decide whether an argument's form is valid. It cannot decide whether every true statement about numbers has a proof, because some do not.
หลักการที่สามคือรอยแยกที่วงจรของแชนนอนไม่ได้แก้: การพิสูจน์ไม่ใช่ความจริง ปี 1929 ในวิทยานิพนธ์ปริญญาเอกภายใต้ฮันส์ ฮาห์น เคิร์ท เกอเดิลพิสูจน์ว่าตรรกศาสตร์อันดับหนึ่งสมบูรณ์ (completeness) — ตอบคำถามที่ฮิลแบร์ทกับอัคเคอร์มันน์ตั้งไว้เมื่อปีก่อนหน้า เขาแสดงว่าทุกสูตรที่สมเหตุสมผลเชิงตรรกะในตรรกศาสตร์อันดับหนึ่งมีบทพิสูจน์ในระบบรูปนัย (formal system) และ (คุณสมบัติคู่กันคือความสมเหตุสมผลเชิงตรรกะ (soundness)) ทุกสูตรที่พิสูจน์ได้ก็สมเหตุสมผล สองปีต่อมา ชายคนเดียวกันพลิกอีกด้านของเหรียญให้ดู: ระบบรูปนัยที่สมนัยกันเองใดๆ ที่อุดมพอจะบรรจุเลขคณิตพื้นฐาน ต้องไม่สมบูรณ์ — มันบรรจุข้อความเลขคณิตที่เป็นจริงแต่พิสูจน์ไม่ได้ ตัวตรรกศาสตร์อันดับหนึ่งเองสมบูรณ์ เลขคณิตที่สร้างทับบนมันไม่สมบูรณ์ ผลลัพธ์สองอันนี้ไม่ขัดกัน เพราะตอบคนละคำถามเกี่ยวกับคนละระบบ แต่รวมกันแล้วมันหมายถึงบางอย่างที่แน่นอนและถาวร: การทำให้การอนุมานเป็นกลไก (ความสมเหตุสมผลเชิงตรรกะและความสมบูรณ์ของตรรกศาสตร์) ไม่ใช่โครงการเดียวกับการทำให้ความจริงทางคณิตศาสตร์ทั้งหมดเป็นกลไก (ซึ่งเกอเดิลแสดงแล้วว่าทำให้เสร็จไม่ได้) วงจรตัดสินได้ว่ารูปแบบของข้อโต้แย้งสมเหตุสมผลไหม มันตัดสินไม่ได้ว่าทุกข้อความจริงเกี่ยวกับตัวเลขมีบทพิสูจน์ไหม เพราะบางข้อความไม่มี
The fourth principle turns logic from a way of checking arguments into a way of writing programs. Robert Kowalski's 1979 slogan "Algorithm = Logic + Control" (Communications of the ACM 22, no. 7: 424–436) proposed splitting any procedure into a logic component — what is true, stated declaratively — and a control component — how a machine searches for it. Alain Colmerauer and Philippe Roussel had already built the proof of concept in Marseille in the summer of 1972, working out the top-down search strategy with Kowalski himself during his visits from Edinburgh: Prolog, a language in which a program is literally a set of logical clauses, and running the program means asking the machine to prove a theorem from them by resolution (Kowalski, "The Early Years of Logic Programming"). For the first time, writing a specification and writing an executable were, formally, the same act.
หลักการที่สี่เปลี่ยนตรรกศาสตร์จากวิธีตรวจข้อโต้แย้ง เป็นวิธีเขียนโปรแกรม สโลแกนปี 1979 ของโรเบิร์ต โควาลสกี "Algorithm = Logic + Control" (Communications of the ACM 22, no. 7: 424–436) เสนอให้ผ่ากระบวนวิธีใดๆ ออกเป็นสองส่วน: ส่วนตรรกะ — สิ่งที่เป็นจริง ระบุแบบประกาศ (declarative) — กับส่วนควบคุม — เครื่องจักรค้นหามันอย่างไร อาแล็ง กอลเมโรกับฟีลิป รูแซลสร้างการพิสูจน์แนวคิดไว้ก่อนแล้วที่มาร์แซย์ ฤดูร้อนปี 1972 คิดกลยุทธ์การค้นหาแบบบนลงล่างร่วมกับโควาลสกีเองระหว่างที่เขาไปเยือนจากเอดินบะระ: Prolog ภาษาที่โปรแกรมหนึ่งคือชุดอนุประโยคเชิงตรรกะโดยแท้ และการรันโปรแกรมคือการขอให้เครื่องพิสูจน์ทฤษฎีบทจากอนุประโยคเหล่านั้นด้วย resolution (Kowalski, "The Early Years of Logic Programming") การเขียนข้อกำหนดกับการเขียนโปรแกรมที่รันได้ เป็นการกระทำเดียวกันในทางรูปนัยเป็นครั้งแรก
The fifth principle is the deepest handshake between the two courts in this entire book: the Curry–Howard correspondence. In 1934, Haskell Curry noticed that the types assignable to the combinators of combinatory logic matched, term for term, the axioms of intuitionistic implicational logic ("Functionality in Combinatory Logic," PNAS 20). William Howard extended the observation to full natural deduction and the lambda calculus in 1969, though the paper that made it famous, "The Formulae-as-Types Notion of Construction," was not published until 1980, in a festschrift for Curry. The correspondence says something stronger than analogy: a proposition is a type, a proof of that proposition is a program of that type, and simplifying a proof — removing a detour — is running the program one step. Logic and computation are not two things that resemble each other; under Curry–Howard, for a wide and growing class of systems, they are the same thing described twice. Modern proof assistants (Coq, Agda, Lean) are, quite literally, programming languages in which a well-typed program is a certificate that a theorem is true.
หลักการที่ห้าคือการจับมือที่ลึกที่สุดระหว่างสองศาลตลอดทั้งเล่ม: ความสอดคล้อง 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) คือใบรับรองว่าทฤษฎีบทหนึ่งเป็นจริง
The people, briefly. Boole was self-taught, working as a schoolmaster in Lincoln before a professorship at Cork; Frege spent most of his career unread, his logic noticed chiefly because Bertrand Russell wrote to him in 1902 to point out a contradiction in it. Kurt Gödel worked in near isolation in Vienna and later Princeton, distrustful to the point of starving himself in his final year. Haskell Curry and William Howard are barely names outside logic departments — fitting, for a correspondence whose own publication was delayed eleven years, as if the ideas in this chapter have a habit of arriving before anyone is ready to print them.
ผู้คน โดยย่อ บูลเรียนรู้ด้วยตัวเอง เป็นครูใหญ่ในลินคอล์นก่อนได้เก้าอี้ศาสตราจารย์ที่คอร์ก เฟรเกใช้ชีวิตการทำงานเกือบทั้งชีวิตโดยไม่มีใครอ่านผลงาน ตรรกะของเขาเข้าตาคนก็เพราะเบอร์ทรันด์ รัสเซลล์เขียนจดหมายถึงเขาในปี 1902 เพื่อชี้ข้อขัดแย้งในนั้น เคิร์ท เกอเดิลทำงานอย่างโดดเดี่ยวเกือบสิ้นเชิงในเวียนนาและต่อมาที่พรินซ์ตัน ระแวงจนอดอาหารตัวเองตายในปีสุดท้ายของชีวิต แฮสเคลล์ เคอร์รีกับวิลเลียม ฮาวเวิร์ดแทบไม่เป็นที่รู้จักนอกภาควิชาตรรกศาสตร์ — เหมาะสมดี สำหรับความสอดคล้องที่การตีพิมพ์ของมันเองล่าช้าไปสิบเอ็ดปี ราวกับความคิดในบทนี้ติดนิสัยมาถึงก่อนที่ใครจะพร้อมพิมพ์มัน
Connections
เชื่อมโยง
Chapter 00 is this chapter's parent: the Frege–Russell–Hilbert–Gödel–Turing pipeline is narrated there in full; this chapter stays inside logic's own family quarrel. Chapter 09 returns to 1936 to ask what the Church–Turing thesis actually claims. Chapter 11 owns Shannon's later severing of information from meaning in 1948; this chapter's Shannon stops at 1937, where circuits meet Boole and nothing yet has been said about meaning. Chapter 12 takes Curry–Howard to its full depth, through Brouwer's intuitionism and mechanized mathematics.
บทที่ 00 คือบทแม่ของบทนี้: สายพานเฟรเก–รัสเซลล์–ฮิลแบร์ท–เกอเดิล–ทัวริงเล่าไว้ครบถ้วนที่นั่น บทนี้อยู่แค่ในเรื่องทะเลาะกันเองในครอบครัวตรรกศาสตร์ บทที่ 09 ย้อนกลับไปปี 1936 เพื่อถามว่าข้อตั้ง Church–Turing อ้างอะไรกันแน่ บทที่ 11 เป็นเจ้าของเรื่องที่แชนนอนตัดความหมายออกจากสารสนเทศในภายหลัง ปี 1948 แชนนอนของบทนี้หยุดที่ปี 1937 ตรงที่วงจรมาบรรจบกับบูล และยังไม่มีใครพูดถึงความหมายเลย บทที่ 12 พาความสอดคล้อง Curry–Howard ลงไปจนสุดความลึก ผ่านตรรกะสัญชานนิยมของบราวเวอร์และคณิตศาสตร์เชิงกลไก
Open questions
คำถามที่ยังเปิดอยู่
If Boole and Leibniz, and later Frege, kept independently finding the same seam, is a mathematized logic something humanity was always going to discover once algebra and doubt about the syllogism coincided — or was the coincidence itself contingent? And if proof and program are truly the same object under Curry–Howard, which discipline should be said to have discovered the other: did computing find out it was secretly doing logic, or did logic find out it was secretly executable?
ถ้าบูลกับไลบ์นิซ และภายหลังเฟรเก ต่างเจอตะเข็บเดียวกันโดยอิสระจากกันครั้งแล้วครั้งเล่า ตรรกศาสตร์ที่แปลงเป็นคณิตศาสตร์เป็นสิ่งที่มนุษยชาติต้องค้นพบอยู่ดี เมื่อพีชคณิตกับความสงสัยในซิลโลจิซึมมาบรรจบกันพอดีหรือเปล่า — หรือความบังเอิญนั้นเองก็ไม่แน่นอน และถ้าบทพิสูจน์กับโปรแกรมเป็นวัตถุเดียวกันจริงภายใต้ Curry–Howard สาขาไหนควรนับว่าเป็นฝ่ายค้นพบอีกฝ่าย: การคำนวณค้นพบว่าตัวเองแอบทำตรรกศาสตร์อยู่ หรือตรรกศาสตร์ค้นพบว่าตัวเองแอบรันได้
Go deeper
อ่านต่อ
- Ernest Nagel and James R. Newman, Gödel's Proof, New York University Press, 1958 — still the clearest short account of what completeness and incompleteness do and do not say.
- 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 (written 1969).
- Gödel's Incompleteness Theorems, Stanford Encyclopedia of Philosophy.
- 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