09 · Computability
09 · การคำนวณได้
This is the first hearing of Part II. Computation stops being the witness and takes the examiner's chair — and its first question is aimed at itself: what does its own founding limit actually prove?
ภาค II เปิดการไต่สวนครั้งแรกตรงนี้ การคำนวณลุกจากเก้าอี้พยานไปนั่งเก้าอี้ผู้ซักถาม และคำถามแรกพุ่งเข้าใส่ตัวมันเอง: ขีดจำกัดที่เป็นรากฐานของมันพิสูจน์อะไรได้จริง?
What do the limits of computation prove about the limits of reason?
ขีดจำกัดของการคำนวณ พิสูจน์อะไรเกี่ยวกับขีดจำกัดของเหตุผลได้บ้าง?
Two papers settled the same question six weeks apart in 1936, and neither author had read the other's proof. Alonzo Church's "An Unsolvable Problem of Elementary Number Theory" appeared on 15 April in the American Journal of Mathematics (58: 345–363), showing by lambda-definability that no algorithm decides the Entscheidungsproblem — the question, posed by David Hilbert and Wilhelm Ackermann in Grundzüge der theoretischen Logik (1928), of whether a mechanical procedure could certify the validity of any first-order sentence. Alan Turing's own paper, "On Computable Numbers, with an Application to the Entscheidungsproblem," was received by the Proceedings of the London Mathematical Society on 28 May — and reached the identical negative answer by an entirely different route: a human clerk idealized down to a paper tape, a finite set of states, and a table of instructions. Turing, disappointed to learn he had been beaten to publication, added an appendix proving that his machines and Church's lambda-definable functions compute exactly the same class of functions. Two definitions of "mechanical," invented independently, turned out to coincide exactly. That coincidence is the whole of the evidence for what is now called the Church–Turing thesis, and evidence is not the same thing as proof.
สองงานวิจัยในปี 1936 ตอบคำถามเดียวกันห่างกันหกสัปดาห์ โดยผู้เขียนทั้งสองไม่เคยอ่านบทพิสูจน์ของอีกฝ่าย บทความ "An Unsolvable Problem of Elementary Number Theory" ของ Alonzo Church ออกวันที่ 15 เมษายน ใน American Journal of Mathematics (58: 345–363) แสดงด้วย lambda-definability ว่าไม่มีอัลกอริทึมใดตัดสิน Entscheidungsproblem (ปัญหาการตัดสินใจ) ได้ — คำถามที่ David Hilbert กับ Wilhelm Ackermann ตั้งไว้ใน Grundzüge der theoretischen Logik (1928) ว่ากระบวนการเชิงกลไกจะรับรองความสมเหตุสมผลของประโยคอันดับหนึ่ง (first-order sentence) ใดๆ ได้หรือไม่ Proceedings of the London Mathematical Society รับบทความของ Alan Turing เอง "On Computable Numbers, with an Application to the Entscheidungsproblem" วันที่ 28 พฤษภาคม คำตอบเป็นลบอย่างเดียวกันเป๊ะ แต่มาคนละทางโดยสิ้นเชิง: เสมียนมนุษย์ที่ถูกลดรูปเหลือเทปกระดาษ ชุดสถานะจำกัดชุดหนึ่ง และตารางคำสั่ง Turing ผิดหวังที่รู้ว่ามีคนตีพิมพ์ตัดหน้า จึงเติมภาคผนวกพิสูจน์ว่าเครื่องของเขากับฟังก์ชัน lambda-definable ของ Church คำนวณฟังก์ชันคลาสเดียวกันพอดี นิยามของ "เชิงกลไก" สองแบบ คิดขึ้นแยกกันโดยอิสระ กลับทับกันสนิท ความบังเอิญนั้นคือหลักฐานทั้งหมดที่มีให้กับสิ่งที่วันนี้เรียกว่าข้อตั้ง Church–Turing (Church–Turing thesis) และหลักฐานไม่ใช่สิ่งเดียวกับบทพิสูจน์
It cannot be a theorem, because "effectively calculable" was never a formal term before Turing formalized it — you cannot prove an identity between something precise and something that, until that moment, was only an intuition. What Turing actually did was analyze, by exhaustion, everything a human "computer" — a person following fixed instructions with pencil and paper — could do: read a symbol, change an internal state, write a symbol, shift attention. Every rival formalism proposed since — Gödel–Herbrand's general recursive functions, Emil Post's production systems, register machines — has been proven equivalent to Turing's, and Stephen Kleene, who named the conjecture "Church's Thesis" in 1943, treated that convergence as inductive support rather than deductive closure. So the thesis sits in a category Hilbert's program never anticipated: not quite mathematics, not quite empirical science, held up by the fact that everyone who has tried to break it has instead confirmed it.
มันเป็นทฤษฎีบทไม่ได้ เพราะ "คำนวณได้อย่างมีประสิทธิผล" (effectively calculable) ไม่เคยเป็นคำเชิงรูปนัยมาก่อนที่ Turing จะทำให้มันเป็นรูปนัย จะพิสูจน์ความเท่ากันระหว่างสิ่งที่แม่นยำกับสิ่งที่ถึงตอนนั้นยังเป็นแค่สัญชาตญาณย่อมทำไม่ได้ สิ่งที่ Turing ทำจริงๆ คือไล่ให้ครบทุกกรณีว่ามนุษย์ที่ทำหน้าที่ "computer" — คนที่ทำตามคำสั่งตายตัวด้วยดินสอกับกระดาษ — ทำอะไรได้บ้าง: อ่านสัญลักษณ์ เปลี่ยนสถานะภายใน เขียนสัญลักษณ์ ย้ายความสนใจ ฟอร์มัลลิสม์ (formalism) คู่แข่งทุกตัวที่เสนอมาตั้งแต่นั้น — ฟังก์ชันเวียนบังเกิดทั่วไป (general recursive functions) ของ Gödel–Herbrand, ระบบการผลิต (production systems) ของ Emil Post, เครื่องรีจิสเตอร์ (register machines) — ถูกพิสูจน์แล้วว่าเทียบเท่ากับของ Turing และ Stephen Kleene ผู้ตั้งชื่อข้อคาดการณ์นี้ว่า "Church's Thesis" ในปี 1943 อ่านการลู่เข้าหากันนั้นเป็นหลักฐานสนับสนุนเชิงอุปนัย ไม่ใช่การปิดเชิงนิรนัย ข้อตั้งนี้จึงตกอยู่ในหมวดที่โครงการของ Hilbert ไม่เคยคาดถึง: ไม่ใช่คณิตศาสตร์เต็มตัว ไม่ใช่วิทยาศาสตร์เชิงประจักษ์เต็มตัว ยืนอยู่ได้เพราะทุกคนที่พยายามหักล้างมันกลับยืนยันมันแทน
That instability is itself philosophically productive, because the method Turing used to reach it — diagonalization, turning a system's own machinery against itself — outgrew the theorem it built. Cantor used it in 1891 to show no list of real numbers can be complete; Gödel adapted it in 1931 to build an arithmetical sentence that asserts its own unprovability; Turing adapted it again to show no algorithm can decide, for an arbitrary program, whether it halts — feed a hypothetical halting-decider its own description and a contradiction falls out in one line. The same skeleton reappears in Tarski's proof that no sufficiently rich language can define its own truth predicate, and in Frederic Fitch's 1963 paradox of knowability. Diagonalization stopped being a mathematician's trick around the middle of the twentieth century and became philosophy's standard proof that a system cannot fully turn its lights on itself — the argument form this book's own courtroom spine depends on.
ความไม่มั่นคงนั้นเองให้ผลผลิตเชิงปรัชญา เพราะวิธีที่ Turing ใช้ไปถึงมัน — การทแยงมุม (diagonalization) การหันกลไกของระบบกลับมาโจมตีตัวมันเอง — โตเกินทฤษฎีบทที่มันสร้างไปไกล Cantor ใช้มันในปี 1891 แสดงว่าไม่มีรายการจำนวนจริงใดครบถ้วนได้ Gödel ดัดแปลงมันในปี 1931 สร้างประโยคเลขคณิตที่ยืนยันความพิสูจน์ไม่ได้ของตัวเอง Turing ดัดแปลงมันอีกครั้ง แสดงว่าไม่มีอัลกอริทึมใดตัดสินปัญหาการหยุด (halting problem) ได้ สำหรับโปรแกรมใดก็ตามจะบอกไม่ได้ว่ามันจะหยุดทำงานหรือไม่ — ป้อนตัวตัดสิน halting problem สมมติด้วยคำอธิบายของตัวมันเอง ความขัดแย้งโผล่ออกมาในบรรทัดเดียว โครงเดียวกันโผล่ซ้ำในบทพิสูจน์ของ Tarski ที่ว่าไม่มีภาษาใดที่รุ่มรวยพอจะนิยามภาคแสดงความจริง (truth predicate) ของตัวเองได้ และในปฏิทรรศน์ความรู้ได้ (paradox of knowability) ของ Frederic Fitch ปี 1963 ราวกลางศตวรรษที่ 20 diagonalization เลิกเป็นกลเม็ดของนักคณิตศาสตร์ และกลายเป็นบทพิสูจน์มาตรฐานของปรัชญาที่ว่าระบบหนึ่งส่องไฟดูตัวเองให้ทั่วไม่ได้ — รูปแบบข้อโต้แย้งที่แกนห้องพิจารณาคดีของหนังสือเล่มนี้เองพึ่งพาอยู่
It is also the argument form behind the most publicized claim in this territory. J. R. Lucas told the Oxford Philosophical Society in 1959, and then argued in print in "Minds, Machines and Gödel" (Philosophy 36, 1961: 112–127), that Gödel's theorem refutes mechanism: for any consistent formal system F strong enough to encode arithmetic, Gödel's construction yields a true sentence F cannot prove, yet a human reasoner, standing outside F and reflecting on it, can see that the sentence is true — so no single formal system captures everything a mind can know, and minds are therefore not machines. Roger Penrose revived the argument at greater length in The Emperor's New Mind (1989) and defended a reinforced version in Shadows of the Mind (1994). The standard reply, developed across decades of responses from Paul Benacerraf onward, is that the argument smuggles in exactly the certainty Gödel's second incompleteness theorem forbids: to "see" that the Gödel sentence for F is true, the reasoner must already know F is consistent, and no consistent system — human or mechanical — can prove its own consistency from within. The argument also assumes a human mind is well modeled as one single, fixed, consistent formal system in the first place, which nothing here establishes. Computation, examining this claim on its own witness stand, cannot certify it; but philosophy answers back here too, because the machine's own founding thesis has the identical shape of unprovable self-trust — the Church–Turing thesis cannot certify its own domain without appealing to an intuition about "mechanical" that no formalism proves, any more than the human reasoner can certify F's consistency from inside F.
ข้อกล่าวอ้างที่โด่งดังที่สุดในอาณาเขตนี้ยืนบนรูปแบบข้อโต้แย้งอันเดียวกัน J. R. Lucas พูดต่อหน้า Oxford Philosophical Society ในปี 1959 แล้วเขียนโต้แย้งเป็นลายลักษณ์อักษรใน "Minds, Machines and Gödel" (Philosophy 36, 1961: 112–127) ว่าทฤษฎีบทของ Gödel หักล้างกลไกนิยม (mechanism): สำหรับระบบรูปนัย F ที่สมเหตุสมผลใดๆ ที่แข็งแรงพอจะเข้ารหัสเลขคณิตได้ การสร้างของ Gödel ให้ประโยคจริงประโยคหนึ่งที่ F พิสูจน์ไม่ได้ แต่ผู้ให้เหตุผลที่เป็นมนุษย์ ยืนอยู่นอก F และไตร่ตรองมัน กลับเห็นได้ว่าประโยคนั้นจริง — ฉะนั้นไม่มีระบบรูปนัยเดียวใดจับทุกสิ่งที่จิตรู้ได้ครบ และจิตจึงไม่ใช่เครื่องจักร Roger Penrose รื้อฟื้นข้อโต้แย้งนี้ให้ยาวขึ้นใน The Emperor's New Mind (1989) และปกป้องเวอร์ชันที่เสริมกำลังแล้วใน Shadows of the Mind (1994) คำตอบโต้มาตรฐาน สั่งสมมาหลายทศวรรษนับจาก Paul Benacerraf เป็นต้นมา คือข้อโต้แย้งนี้แอบสอดความแน่นอนแบบเดียวกับที่ทฤษฎีบทความไม่สมบูรณ์ข้อที่*สอง*ของ Gödel ห้ามไว้เข้ามาพอดี: การจะ "เห็น" ว่าประโยค Gödel สำหรับ F เป็นจริง ผู้ให้เหตุผลต้องรู้อยู่ก่อนแล้วว่า F สมเหตุสมผล และไม่มีระบบที่สมเหตุสมผล — มนุษย์หรือเครื่องจักรก็ตาม — พิสูจน์ความสมเหตุสมผลของตัวเองจากภายในได้ ข้อโต้แย้งนี้ยังสมมติตั้งแต่แรกว่าจิตมนุษย์ถูกจำลองได้ดีในฐานะระบบรูปนัยหนึ่งเดียว ตายตัว สมเหตุสมผล ซึ่งไม่มีอะไรในที่นี้ยืนยันให้ การคำนวณ เมื่อสอบข้อกล่าวอ้างนี้จากที่นั่งพยานของตัวเอง รับรองมันไม่ได้ แต่ปรัชญาก็ตอบกลับตรงนี้เหมือนกัน เพราะข้อตั้งก่อตั้งของเครื่องจักรเองมีรูปทรงเดียวกันกับความไว้ใจตัวเองที่พิสูจน์ไม่ได้ — Church–Turing thesis รับรองอาณาเขตของตัวเองไม่ได้ถ้าไม่อาศัยสัญชาตญาณเรื่อง "เชิงกลไก" ที่ไม่มีฟอร์มัลลิสม์ใดพิสูจน์ ไม่ต่างจากที่ผู้ให้เหตุผลมนุษย์รับรองความสมเหตุสมผลของ F จากภายใน F ไม่ได้
Turing knew his own thesis had an edge, because he drew it himself. His 1939 Princeton doctoral thesis, "Systems of Logic Based on Ordinals," introduced oracle machines: Turing machines equipped with a black-box oracle answering questions no Turing machine could resolve unaided. B. Jack Copeland and Diane Proudfoot later named the research program built on that opening "hypercomputation," and Copeland has argued that exotic physical setups — closed timelike curves, or the infinite-proper-time computations permitted in a Malament–Hogarth spacetime — might in principle realize an oracle. The honest objection is the verification problem: even if such a device were built, nothing from outside could ever confirm it had computed a genuinely non-Turing-computable function rather than an extremely large Turing-computable one. Here physics, not logic, casts the deciding vote on whether the thesis bounds all possible computation or only computation as our universe happens to permit it.
Turing รู้ว่าข้อตั้งของตัวเองมีขอบ เพราะเขาเป็นคนขีดมันเอง วิทยานิพนธ์ปริญญาเอกที่ Princeton ปี 1939 ของเขา "Systems of Logic Based on Ordinals" เปิดตัวเครื่องออราเคิล (oracle machine): เครื่องทัวริงที่ติดออราเคิลกล่องดำไว้ ตอบคำถามที่เครื่องทัวริงตอบเองไม่ได้ B. Jack Copeland และ Diane Proudfoot ตั้งชื่อโครงการวิจัยที่งอกจากช่องนั้นในภายหลังว่าไฮเปอร์คอมพิวเตชัน (hypercomputation) และ Copeland โต้แย้งว่าโครงสร้างทางฟิสิกส์ที่แปลกประหลาด — closed timelike curve หรือการคำนวณแบบ infinite-proper-time ที่กาลอวกาศแบบ Malament–Hogarth เปิดทางให้ — อาจทำให้ออราเคิลเป็นจริงได้ในหลักการ ข้อคัดค้านที่ตรงไปตรงมาคือปัญหาการตรวจสอบยืนยัน (verification problem): ต่อให้สร้างอุปกรณ์แบบนั้นขึ้นมาได้ ก็ไม่มีอะไรจากภายนอกยืนยันได้ว่ามันคำนวณฟังก์ชันที่ non-Turing-computable แท้ๆ ไม่ใช่ฟังก์ชันที่ Turing-computable แต่ใหญ่โตมโหฬาร ตรงนี้ฟิสิกส์ ไม่ใช่ตรรกศาสตร์ เป็นผู้ลงคะแนนชี้ขาดว่าข้อตั้งนี้ล้อมการคำนวณที่เป็นไปได้ทั้งหมด หรือล้อมแค่การคำนวณเท่าที่เอกภพของเราเผอิญอนุญาต
Gödel himself licensed far less than his popularizers claim. In his 1951 Gibbs Lecture he stated a disjunction and stopped there: either the human mind is not equivalent to any finite machine, or there exist mathematical problems absolutely undecidable by any means — or both — but he refused to say which, remaining a mathematical Platonist who suspected the first disjunct without ever asserting he had proved it. What Gödel proved is a limit inside formal systems; what Lucas, Penrose, and a century of secondary literature have drawn from it is a conclusion about minds that the theorem itself never reaches.
Gödel เองอนุญาตไว้น้อยกว่าที่คนเผยแพร่งานของเขาอ้างมาก ในการบรรยาย Gibbs Lecture ปี 1951 เขาวางเงื่อนไขแบบ "หรือ" (disjunction) ไว้แล้วหยุดตรงนั้น: จิตมนุษย์ไม่เทียบเท่าเครื่องจักรจำกัดใดๆ หรือไม่ก็มีปัญหาทางคณิตศาสตร์ที่ตัดสินไม่ได้เด็ดขาดไม่ว่าด้วยวิธีใด — หรือทั้งสองอย่าง — แต่เขาปฏิเสธที่จะบอกว่าข้อไหน เขายังเป็นนักเพลโตนิยมทางคณิตศาสตร์ที่เอนไปทางข้อแรกโดยไม่เคยยืนยันว่าตนพิสูจน์มันได้ สิ่งที่ Gödel พิสูจน์คือขีดจำกัดภายในระบบรูปนัย สิ่งที่ Lucas, Penrose และวรรณกรรมรองตลอดหนึ่งศตวรรษดึงออกมาจากมัน คือข้อสรุปเรื่องจิตที่ตัวทฤษฎีบทเองไปไม่ถึง
Connections
เชื่อมโยง
Chapter 00 named 1936 as the moment the machine fell out of a philosophical proof; this chapter returns to ask what that moment actually licenses. Chapter 01 owns Gödel and Curry–Howard as logic's shared inheritance. Chapter 04 owns the question the Lucas–Penrose argument tries to settle from outside — whether the mind is what the brain computes. Chapter 10 tightens "in principle" into a measurable resource. Chapter 12 shows what proof assistants do with incompleteness once it is treated as an engineering constraint rather than a philosophical verdict.
บทที่ 00 เรียกปี 1936 ว่าคือช่วงที่เครื่องจักรหล่นออกมาจากบทพิสูจน์เชิงปรัชญา บทนี้ย้อนกลับไปถามว่าช่วงเวลานั้นอนุญาตอะไรไว้จริงๆ บทที่ 01 เป็นเจ้าของ Gödel และ Curry–Howard ในฐานะมรดกร่วมของตรรกศาสตร์ บทที่ 04 เป็นเจ้าของคำถามที่ข้อโต้แย้งของ Lucas–Penrose พยายามตัดสินจากภายนอก — ว่าจิตคือสิ่งที่สมองคำนวณหรือไม่ บทที่ 10 บีบ "ในหลักการ" ให้กลายเป็นทรัพยากรที่วัดได้ บทที่ 12 แสดงว่า proof assistant ทำอะไรกับความไม่สมบูรณ์ เมื่อมันถูกมองเป็นข้อจำกัดเชิงวิศวกรรมแทนคำตัดสินเชิงปรัชญา
Open questions
คำถามที่ยังเปิดอยู่
Is the Church–Turing thesis falsifiable — and would a working hypercomputer refute it, or merely relocate the boundary it draws? Does Gödel's 1951 disjunction ever get resolved, or does it stay open the way the thesis itself does? And if minds turn out to be Turing-equivalent, does that settle functionalism, or only computability — a question this chapter can raise but not answer.
Church–Turing thesis พิสูจน์เท็จได้ (falsifiable) หรือไม่ — และถ้ามี hypercomputer ที่ใช้งานได้จริง มันจะหักล้างข้อตั้งนี้ หรือแค่ย้ายเส้นขอบที่มันขีดไว้? เงื่อนไขแบบ "หรือ" ของ Gödel ในปี 1951 เคยถูกคลี่คลายไหม หรือยังเปิดค้างเหมือนที่ตัวข้อตั้งเองเปิดค้างอยู่? และถ้าจิตกลายเป็นสิ่งที่ Turing-equivalent จริง นั่นยุติข้อถกเถียงเรื่องหน้าที่นิยม (functionalism) หรือยุติแค่เรื่องการคำนวณได้ — คำถามที่บทนี้ตั้งได้แต่ตอบไม่ได้
Go deeper
อ่านต่อ
- B. Jack Copeland, Carl J. Posy, and Oron Shagrir, eds., Computability: Turing, Gödel, Church, and Beyond (Cambridge, MA: MIT Press, 2013).
- Alonzo Church, "An Unsolvable Problem of Elementary Number Theory," American Journal of Mathematics 58 (1936): 345–363; Alan Turing, "On Computable Numbers, with an Application to the Entscheidungsproblem," Proceedings of the London Mathematical Society, ser. 2, 42 (1936–37): 230–265, received 28 May 1936 — doi.org/10.1112/plms/s2-42.1.230.
- Stanford Encyclopedia of Philosophy, "The Church-Turing Thesis" — plato.stanford.edu/entries/church-turing.
- B. Jack Copeland, Carl J. Posy, and Oron Shagrir, eds., Computability: Turing, Gödel, Church, and Beyond (Cambridge, MA: MIT Press, 2013).
- Alonzo Church, "An Unsolvable Problem of Elementary Number Theory," American Journal of Mathematics 58 (1936): 345–363; Alan Turing, "On Computable Numbers, with an Application to the Entscheidungsproblem," Proceedings of the London Mathematical Society, ser. 2, 42 (1936–37): 230–265, received 28 May 1936 — doi.org/10.1112/plms/s2-42.1.230.
- Stanford Encyclopedia of Philosophy, "The Church-Turing Thesis" — plato.stanford.edu/entries/church-turing.