บทพิสูจน์คือโปรแกรม ตรรกะคือการคำนวณ

หลายคนอาจจะเคยได้ยินทฤษฎีบทในตรรกศาสตร์ของ Kurt Gödel (1906-1978) เกี่ยวกับความ “ไม่สมบูรณ์” ของ axiomatic system (“มีความจริงที่พิสูจน์ไม่ได้” ที่ถูกให้ใครต่อใครเอาไปใช้ผิดๆเต็มไปหมด รวมเล่มใน Gödel’s Theorem: An Incomplete Guide to Its Uses and Abuses ของ Torkel Franzén) ผมอยากจะนำเสนอว่าจากมุมมองของทฤษฎีคอมพิวเตอร์ ทฤษฎีบทนี้ (รวมทั้งที่ปรับปรุงโดย Rosser) พิสูจน์ได้ไม่ยุ่งยาก บทพิสูจน์ทั้งหมดในโพสท์นี้มาจาก Scott Aaronson [1] แต่ถ้ามีตรงไหนที่มั่วอันนั้นเป็นความผิดของผมเอง

ทฤษฎีบทของ Gödel

สำหรับคนที่ไม่ชอบเรื่องยุ่งยาก มันจะดีไม่น้อยถ้าเราสามารถค้นพบทุกความจริงได้ด้วยเซ็ตของ “ความจริงพื้นฐาน” ที่เล็กกว่าเซ็ตของความจริงทั้งหมด ในคณิตศาสตร์หมายความว่าเราต้องการความจริง (“axiom”) ที่นิยามด้วยกระบวนการที่สามารถปฏิบัติตามเป็นขั้นๆได้ (ไม่ใช่ตั้งทุกๆความจริงให้เป็น axioms ทั้งที่ไม่รู้ด้วยซ้ำว่าอะไรคือความจริงบ้าง) [2] ที่สามารถนำไปใช้พิสูจน์ทุกความจริงได้เมื่อมีกฎในการพิสูจน์ (อย่างการอุปนัย) เช่น เรามี Peano axioms ของระบบจำนวนเต็ม หรือ axioms ของ ZFC set theory

เราจะรู้ได้อย่างไรว่า axioms เหล่านี้เป็น axioms ของระบบในความเป็นจริง ระบบในความเป็นจริงจะต้องไม่มีข้อขัดแย้งในตัวมันเอง (consistent) (ความขัดแย้งคือมีประพจน์ P ที่สามารถพิสูจน์ได้ทั้งว่าเป็นจริงและเป็นเท็จ (P และ not P))

Gödel พิสูจน์ทฤษฎีบทความสมบูรณ์ (completeness theorem) ที่กล่าวว่า ถ้า axiomatic system A [3] มีความขัดแย้งในตัวมันเอง เราจะสามารถหามันได้ใน axioms หรือกลับกัน ถ้า เราไม่สามารถหาข้อขัดแย้งจาก axioms ได้ ทุกๆ realization ที่มาจาก axioms นั้นก็จะไม่มีข้อขัดแย้ง

แต่ Gödel (1931) ก็ดันพิสูจน์ทฤษฎีบทความไม่สมบูรณ์ (incompleteness theorem) ซึ่งมีสองส่วน เราเชื่อว่าทุกๆประพจน์ใน A ถ้าไม่เป็นจริงก็เป็นเท็จ และเราอาจจะหวังด้วยว่าเราสามารถพิสูจน์มันได้ด้วย axioms (สมบัติที่เรียกว่าความสมบูรณ์ (completeness) [4]) แต่ Gödel บอกว่าความสมบูรณ์ต้องแลกมาด้วย unsoundness ซึ่งแปลว่าสิ่งที่พิสูจน์ได้อาจจะไม่เป็นจริง (พูดอีกแบบคือไม่มี A ที่สามารถพิสูจน์ทุกๆและเฉพาะประพจน์ที่เป็นจริงได้) ซึ่งเราไม่ต้องการในคณิตศาสตร์แน่ๆ อีกอย่างหนึ่งทีเราหวังว่าจะทำได้คือพิสูจน์ว่า A ไม่มีความขัดแย้งจาก axioms ของ A เองได้ (ต่างกับทฤษฎีบทความสมบูรณ์ที่บอกว่าพิสูจน์ว่า A มีความขัดแย้งจาก axioms ได้) แต่ Gödel ก็บอกอีกว่า A ที่พิสูจน์ความไม่ขัดแย้งของตัวมันเองได้มีแต่ A ที่มีความขัดแย้งในตัวมันเอง

สิ่งที่ Gödel ทำเพื่อพิสูจน์ทฤษฎีบทความไม่สมบูรณ์ส่วนแรกคือเขียนประพจน์ (“ประโยค Gödel”) G=“ประพจน์นี้ไม่สามารถพิสูจน์ใน A ได้” ใน A (ในบทพิสูจน์ของ Gödel A คือ axioms ใน Principia Mathematica ที่ใช้เกือบ 400 หน้าในการพิสูจน์ว่า 1+1=2 ของ Russell และ Whitehead ซึ่งซับซ้อนพอที่จะเขียนประพจน์นี้ได้) นี่คือส่วนที่ยาว แต่เมื่อเขียนได้แล้วคราวนี้เราก็สมมติว่า A สมบูรณ์ ถ้าพิสูจน์ G ได้ G ก็จะพิสูจน์ได้และพิสูจน์ไม่ได้ในเวลาเดียวกัน (มีความขัดแย้ง ซึ่ง implies unsoundness [5]) ถ้าพิสูจน์ not G ““ประพจน์นี้ไม่สามารถพิสูจน์ใน A ได้” สามารถพิสูจน์ใน A ได้” ได้ ถ้า not G ไม่เป็นจริง A ก็จะ unsound ในขณะที่ถ้า not G เป็นจริง A ก็จะพิสูจน์ว่ามันพิสูจน์ G ได้ ถ้ามันพิสูจน์ได้จริงก็วนกลับไปเคสแรก ถ้ามันพิสูจน์ไม่ได้ก็ unsound เพราะมันพิสูจน์ “มันพิสูจน์ G” ที่ไม่เป็นจริงได้

ทั้งหมดที่ว่ามาแปลว่าเราไม่สามารถหาบางสิ่งที่ต้องการในตรรกศาสตร์ได้ แล้วมันเกี่ยวอะไรกับการหาคำตอบของปัญหาที่มีประโยชน์มากกว่านี้หรือเปล่า?

เครื่องจักร Turing

หลังจากนั้นไม่นาน (1936) Alan Turing (1912-1954) ขณะที่กำลังศึกษาระดับ undergraduate ที่ Cambridge ก็พูดถึงคณิตศาสตร์ของคอมพิวเตอร์ ในสมัยนั้นเมื่อยังไม่มีคอมพิวเตอร์แบบในปัจจุบัน ความหมายเดิมของคอมพิวเตอร์คือผู้คำนวณที่ทำตามกระบวนการที่กำหนดไว้แล้วโดยไม่ต้องใช้ความคิดสร้างสรรค์ (คุ้นๆไหม?) ซึ่งกลายเป็นโมเดลของเครื่องจักร Turing (Turing machine) มีหน่วยความจำเป็น bit string แทนแผ่นกระดาษซึ่งทำหน้าที่รับ input และเขียนการคำนวณลงไปได้ จะเขียนอะไรก็ขึ้นอยู่กับชุดคำสั่งและสิ่งที่เขียนอยู่บนหน่วยความจำไว้ก่อนหน้า คอมพิวเตอร์สามารถอ่านหน่วยความจำได้ทีละช่องและถ้าจะเปลี่ยนไปยังช่องไกลๆต้องเคลื่อนที่ผ่านไปทีละช่องๆ นั่นก็คือมันต้องใช้เวลาในการเข้าถึงหน่วยความจำขนาดใหญ่ (คุณสมบัติซึ่งถูกใช้ในการพิสูจน์ “NP-completeness ของปัญหา 3SAT”) นี่คือเครื่องจักร Turing เครื่องจักร Turing ไม่ใช่โมเดลของคอมพิวเตอร์จริงๆ แต่เป็นไอเดียทางทฤษฎี [6] บางคนอาจจะนึกว่ามันต้องเป็นฮาร์ดแวร์แต่มันเป็นตัวแก้ปัญหาจึงจะคิดว่ามันเป็นซอฟต์แวร์หรือโปรแกรมก็ได้ และในที่สุดแล้วทุกอย่างเกี่ยวกับเครื่องจักร Turing สามารถเข้ารหัสเป็น bit string ได้ จึงคิดว่ามันเป็น input ก็ได้เช่นกัน นี่เป็นไอเดียที่ธรรมดามากสำหรับคนยุคนี้ว่าทุกอย่างที่จำลองในคอมพิวเตอร์ได้ก็แค่การคำนวณบน bit string แต่มันไม่ธรรมดาในสมัยนั้น

มีโมเดลในการคำนวณอื่นที่ถูกคิดค้นขึ้นมาในเวลาใกล้เคียงกันโดยเฉพาะ Lambda calculus ของ Alonzo Church Turing จึงถือโอกาสทำงานในระดับ graduate กับ Church ที่ Princeton แต่ปรากฎว่าโมเดลเหล่านี้มีพลังในการคำนวณเท่ากัน(ซึ่งเดี๋ยวก็จะได้เห็นว่าสำหรับจุดประสงค์ของโพสท์นี้แล้วจริงๆเราไม่จำเป็นจะต้องรู้กลไกการทำงานของเครื่องจักร Turing เลย แต่นั่นคือประเด็น ถึงแม้ว่าหลายๆอย่างท้ายที่สุดแล้วจะไม่ขึ้นกับทุกตัวอักษรของนิยามแต่ก็ต้องนิยามถึงจะทำการวิเคราะห์ทางคณิตศาสตร์ได้ โดยเฉพาะถ้าสนใจ computational complexity ต่อ) จึงได้ถือกำเนิดธีสิส (Thesis) ของ Church-Turing (ซึ่ง Stephen Kleene เป็นคนเรียก (1952)) ที่ว่าทุกๆอย่างที่คำนวณได้สามารถคำนวณได้ด้วยเครื่องจักร Turing [7] คำถามก็คือธีสิสนี้ตั้งใจจะมีความหมายแบบไหนกันแน่ มันนิยาม “การคำนวณ” ด้วยเครื่องจักร Turing? หรือมันบอกว่าโมเดลการคำนวณที่เป็นไปได้ตามกฏของธรรมชาติไม่สามารถเอาชนะเครื่องจักร Turing ได้? ถ้าเข้าใจตามแบบหลัง จากความรู้ทั้งหมดที่มีอยู่(รวมทั้งควอนตัมคอมพิวเตอร์)ดูเหมือนว่าธีสิสของ Church-Turing จะเป็นจริง

ในเปเปอร์ปี 1936 Turing พิสูจน์สองอย่าง หนึ่งว่ามีเครื่องจักรของเขาที่อเนกประสงค์ (universal) คือเราไม่จำเป็นต้องสร้างคอมพิวเตอร์แบบหนึ่งเพื่อทำงาน อีกแบบเพื่อฟังเพลง อีกแบบเพื่อเล่นเกม ไอเดียคือการประมวลผลข้อมูลขึ้นอยู่กับกระบวนการเท่านั้นและไม่ขึ้นกับลักษณะทางกายภาพ จะเป็นเครื่องจักรกล สิ่งมีชีวิต ปรากฎการณ์ทางธรรมชาติ กาแล็กซี ก็เป็นคอมพิวเตอร์ได้ถ้ามันมีศักยภาพพอที่จะให้เราเข้ารหัสทำการคำนวณได้ พิสูจน์อย่างที่สองคือมีปัญหาที่เครื่องจักร Turing แก้ไม่ได้ และสิ่งที่เราอยากจะเสนอ (ซึ่งเป็นที่รู้กันทั่วไปในวิทยาศาสตร์คอมพิวเตอร์) คือทฤษฎีบทความไม่สมบูรณ์ของ Gödel เป็นจริงก็เพราะมีปัญหาที่แก้ไม่ได้บนเครื่องจักร Turing นั่นคือเราสามารถพิสูจน์ทฤษฎีบทความไม่สมบูรณ์ของ Gödel ได้ด้วยทฤษฎีคอมพิวเตอร์

เราหยุดแล้ว แต่เรายังไม่หยุด

เครื่องจักร Turing ที่จะมีประโยชน์มากคือเครื่องจักร H ที่ตัดสินได้ว่าเมื่อเครื่องจักร Turing ได้รับ input หนึ่งๆเข้าไปจะรันไปโดยไม่มีวันหยุดหรือหยุดและให้คำตอบออกมา ถ้ามีเครื่องจักรนี้ก็จะช่วยในการแก้ปัญหาคณิตศาสตร์ได้อย่างมหาศาล เช่นถ้าจะพิสูจน์ข้อสันนิษฐานของ Goldbach“ทุกจำนวนคู่มากกว่า 2 เป็นผลบวกของสองจำนวนเฉพาะ” ก็แค่เอาเครื่องจักร Turing G ที่ตรวจสอบข้อสันนิษฐานนี้กับจำนวนคู่ทีละตัวๆ แล้วถาม H ว่า G จะหยุดไหม (เข้ารหัสโปรแกรม G เป็น bit string ป้อนให้ H เขียนแทนด้วย H(G)) ถ้าไม่หยุด ข้อสันนิษฐานของ Goldbach ก็เป็นจริง ปัญหาอื่นๆที่ต้องเช็คคุณสมบัติอะไรบางอย่างกับทุกๆสมาชิกก็จะแก้ได้โดยวิธีเดียวกัน

แต่ Turing เข้าใจได้ว่าไม่มีโปรแกรมที่จะแก้ปัญหานี้ได้ ทำไมน่ะเหรอ? อย่างที่บอกว่าเราสามารถป้อนเครื่องจักร Turing หนึ่ง เรียกว่า M ให้กับอีกเครื่องจักร Turing หนึ่งได้ โดยเฉพาะเราสามารถป้อน M ให้กับ M เองได้

M(M(M(…)))

คราวนี้นิยาม H’ ให้ H’(M) รันไปตลอดกาลถ้า M(M) หยุด และ H’(M) หยุดถ้า M(M) รันไปตลอดกาล แล้วก็ป้อน H’ ให้ตัวมันเอง ก็จะได้ว่า H’(H’) ทั้งหยุดทั้งรันไปตลอดกาลในเวลาเดียวกัน เป็นข้อขัดแย้งซึ่งบอกว่าเราไม่สามารถมี H (และ H’) ได้ตั้งแต่แรกแล้ว นี่คือ Halting problem ที่แก้ไม่ได้ซึ่งจะให้ทฤษฎีบทของ Gödel ตามมา

เราจะพิสูจน์โดยการหาข้อขัดแย้ง (proof by contradiction) เริ่มจากสมมติว่าทฤษฎีบทความไม่สมบูรณ์ส่วนแรกไม่เป็นจริง และจะพิสูจน์ว่าเราแก้ halting problem ได้ เราจึงต้องพูดถึงทุกอย่างใน axiomatic system A แต่สิ่งที่ทำให้ง่ายในคราวนี้คือเราไม่ต้องสร้างประโยค Gödel แล้ว (self-reference เกิดไปแล้วในบทพิสูจน์ว่า halting problem แก้ไม่ได้ด้านบน) ประพจน์เกี่ยวกับการหยุดของโปรแกรมก็เป็นแค่ประพจน์เกี่ยวกับ bit string ซึ่งสามารถ express ได้ใน A ที่เข้าใจระบบจำนวนเต็ม เนื่องจาก A สมบูรณ์ ถ้าไม่พิสูจน์ได้ว่าโปรแกรมหนึ่งๆรันตลอดกาลก็ต้องพิสูจน์ได้ว่ามันหยุด สิ่งที่เราต้องทำก็คือเสิร์ชหาบทพิสูจน์นั้น เมื่อหาเจอแล้ว เนื่องจาก A sound สิ่งที่ A พิสูจน์จะต้องเป็นจริง A จึงแก้ halting problem ได้ แต่เรารู้แล้วว่ามันเป็นปัญหาที่แก้ไม่ได้จึงไม่มี A ที่ทำได้ดังที่กล่าวมา

แน่นอนว่าจะใช้ปัญหาที่แก้ไม่ได้เกี่ยวกับเครื่องจักร Turing ปัญหาไหนในการพิสูจน์ก็ได้ และจริงๆแล้วทฤษฎี computability มีผลกระทบต่อคณิตศาสตร์สาขาอื่นๆเพราะมีหลายปัญหาที่คนอยากแต่พบว่าแก้ไม่ได้ในทำนองเดียวกันถึงแม้ว่าดูจะไม่มีอะไรที่ “ตลอดกาล” ในปัญหาเหมือน halting problem เช่นใน group theory, เราสามารถกำหนด group ได้ด้วย generators และความสัมพันธ์ระหว่าง generators (relations) สมาชิกของ group อาจจะเขียนในรูปของ generators ได้หลายแบบ (เรียกว่า “คำ” (word)) แต่มี finitely presented group (มี finite generators และ finite relations) ที่ปัญหาว่าคำสองคำแทนสมาชิกตัวเดียวกันหรือไม่ไม่สามารถแก้ได้ (ทฤษฎีบท Novikov-Boone) อีกตัวอย่างใน quantum information เร็วๆนี้คือปัญหาว่าระบบควอนตัมมี “spectral gap” — ช่องว่างระหว่างระดับพลังงานที่ต่ำที่สุดกับระดับถัดขึ้นมา — ใน thermodynamic limit หรือไม่ถูกแสดงว่าแก้ไม่ได้ในกรณีทั่วไป (จริงๆแล้วที่บอกไปไม่ใช่ปัญหาที่เขาพิสูจน์ว่าแก้ไม่ได้ซะทีเดียว ปัญหาของเขามีเงื่อนไขมากกว่านี้)

คราวนี้ลองจินตนาการบทพิสูจน์ด้านบนว่า halting problem แก้ไม่ได้ในเวอร์ชัน “โปรแกรมที่เชื่อบางอย่างเกี่ยวกับตัวมันเอง” สมมติ axiomatic system A ซึ่งเข้าใจประพจน์อีกครั้ง และนิยามให้ H’(M) รันไปตลอดกาลถ้าพิสูจน์ได้ว่า M(M) หยุด และ H’(M) หยุดถ้าพิสูจน์ได้ว่า M(M) รันไปตลอดกาล จะเกิดอะไรขึ้นกับ H’(H’)? ถ้า A พิสูจน์ได้ว่า H’(H’) หยุด H’(H’) จะรันตลอดกาล และถ้าพิสูจน์ได้ว่า H’(H’) รันตลอดกาล H’(H’) จะหยุด แต่ H’(H’) ไม่จำเป็นจะต้องทั้งหยุดทั้งรันตลอดกาลในเวลาเดียวกันเพราะ

โปรแกรมที่หลอกตัวเอง: ถ้า A มีความขัดแย้งในตัวมันเองก็จะ unsound ดังนั้นมันจึงไม่มีปัญหาที่จะพิสูจน์สิ่งที่เป็นเท็จได้ถึงแม้จะเห็นความจริงอยู่ต่อหน้าก็ตาม จึงไม่สามารถสรุปอะไรได้

โปรแกรมที่ไม่เข้าใจตัวเอง: ถ้า A ไม่มีความขัดแย้งในตัวมันเอง มันจะไม่สามารถพิสูจน์ว่า H’(H’) รันไปตลอดกาลได้ เพราะถ้าพิสูจน์ได้ H’(H’) ก็จะหยุดเป็นตัวพิสูจน์ว่า H’(H’) หยุด H’(H’) จึงต้องรันไปตลอดกาล แต่ A ต้องไม่รู้ว่ามันไม่มีความขัดแย้งในตัวมันเองเพราะหาก A พิสูจน์ได้เมื่อไรว่ามันไม่มีความขัดแย้งในตัวมันเองก็เท่ากับพิสูจน์ได้ว่า H'(H’) ต้องรันตลอดกาล ทำให้มันต้องหยุดและเจอกับความขัดแย้งในตัวมันเอง ซึ่งเป็นไปไม่ได้เพราะเราสมมติตั้งแต่ต้นว่ามันไม่มีความขัดแย้งในตัวมันเอง axiomatic system ที่ไม่ความขัดแย้งในตัวเองจึงไม่สามารถพิสูจน์ได้ว่ามันไม่ขัดแย้งในตัวเอง

ทฤษฎีบทความไม่สมบูรณ์ของ Gödel ทั้งสองส่วนจึงพิสูจน์ได้ด้วยไอเดียของ Turing

ทฤษฎีบทของ Rosser

แต่ทฤษฎีบทความไม่สมบูรณ์ของ Gödel ที่ผมมักได้ยินไม่มี unsoundness แต่เป็น “axiomatic system ที่สมบูรณ์ต้องมีความขัดแย้งในตัวมันเอง” แทน ซึ่ง strong กว่าทฤษฎีบทข้างต้นเพราะความขัดแย้งในตัวเอง implies unsoundness ปรากฎว่านี่ไม่ใช่ทฤษฎีบทที่ Gödel พิสูจน์แต่เป็น John Barkey Rosser (1907-1989) ในปี 1936 ปีเดียวกับที่ Turing พูดถึงเครื่องจักร Turing โดยเขียนประพจน์

R = “มีบทหักล้างของประพจน์นี้ที่สั้นกว่าทุกๆบทพิสูจน์ของประพจน์นี้ใน A”

ถ้าพิสูจน์ R ได้ก็จะหาบทหักล้าง (พิสูจน์ not R) ได้เพียงแค่เสิร์ช string ใน A ที่สั้นกว่าบทพิสูจน์ของ R ถ้าเจอก็มีความขัดแย้งใน A ถ้าไม่เจอก็จะเป็นบทพิสูจน์ของ not R เหมือนกัน(“สั้นกว่า”จึงเป็นจุดสำคัญ) ในทางกลับกันน่าสนใจว่าการพิสูจน์ not R ได้ให้ผลที่ mirror การพิสูจน์ R ได้เป๊ะๆ: “มีบทพิสูจน์ของประพจน์นี้ที่สั้นกว่าทุกๆบทหักล้างของประพจน์นี้ใน A” และนำไปสู่ความขัดแย้งด้วยเหตุผลเดียวกัน

ทฤษฎีบทของ Rosser ก็พิสูจน์โดยไม่ต้องสร้าง R ใน axiomatic system ได้! กำหนดปัญหาเรียกว่า Q: โปรแกรมจะ output 0 หรือ 1 หรือรันไปตลอดกาลเมื่อให้ input หนึ่งๆกับมัน? สมมติว่ามีโปรแกรม R ที่แก้ปัญหานี้ได้นิยาม R’ ให้ R’(M) output 0 ถ้า M(M) output 1, R’(M) output 1 ถ้า M(M) output 0, และสุดท้าย R’(M) หยุดและ output อะไรก็ได้ถ้า M(M) ไม่หยุด ไม่มีโปรแกรม R’ (และ R) ที่ทำอย่างนี้ได้

เนื่องจาก A สมบูรณ์ ถ้าพิสูจน์ไม่ได้ว่า M(M) output 0 ก็ต้องหักล้างได้ เราก็เสิร์ชหาบทพิสูจน์หรือบทหักล้าง ถึงแม้ A จะไม่มีความขัดแย้งในตัวมันเองแต่มันอาจจะ unsound ซึ่งอาจเห็นเป็นปัญหาแต่จริงๆแล้วไม่เป็นเพราะถ้า M(M) หยุด ความไม่ขัดแย้งในตัวเองของ A จะบังคับให้ A ตอบ output ที่ถูกต้องมิฉะนั้น output ของ M(M) จะเป็นบทพิสูจน์หรือหักล้างที่ขัดแย้งกับสิ่งที่ A เชื่อ และเกิด M(M) รันไปตลอดกาล A อยากจะทำอะไรก็เรื่องของมัน สรุปแล้ว: ตอบ 0 เมื่อพิสูจน์ได้และตอบ 1 เมื่อหักล้างได้ว่า M(M) output 0 ก็จะแก้ปัญหา Q ได้ แต่เรารู้แล้วว่ามันเป็นปัญหาที่แก้ไม่ได้จึงไม่มี A ที่ทำได้ดังที่กล่าวมา

ดังนั้นเราอาจจะพูดได้ว่า บทพิสูจน์คือโปรแกรม ตรรกะคือการคำนวณ โดยมีบทพิสูจน์ของทฤษฎีบทความไม่สมบูรณ์ของ Gödel-Rosser ด้วยเครื่องจักร Turing เป็นหลักฐานว่าเราสามารถให้โมเดลของการคำนวณโดยที่ไม่ขึ้นกับ axiomatic system ว่าเราจะยกอะไรให้เป็น “ความจริงพื้นฐาน”ได้ ดังที่ Gödel เองกล่าวไว้ (1946)

[Turing] has for the first time succeeded in giving an absolute definition of an interesting epistemological notion, i.e., one not depending on the formalism chosen.

จากการหาๆดูบนอินเตอร์เน็ต “บทพิสูจน์คือโปรแกรม ตรรกะคือการคำนวณ” มีทฤษฎีที่ลึกกว่านี้เยอะซึ่งสรุปได้ใน Curry-Howard-Lambek isomorphism ซึ่งแสดงความเหมือนของตรรกศาสตร์และการคำนวณที่เข้าถึงเนื้อหาทาง categorical ที่เหมือนกัน (การให้ objects, morphisms, functors ฯลฯ)

อรรถาธิบาย

[1] Scott Aaronson, Quantum Computing Since Democritus Lecture 3: Gödel, Turing, and Friends และ “Rosser’s Theorem via Turing Machines
[2] ตรงนี้ไม่ได้ห้ามให้มีจำนวน axioms เป็นอนันต์
[3] ทฤษฎีบทนี้เฉพาะในระบบที่ใช้ first-order logic แต่ทฤษฎีบทความไม่สมบูรณ์ยังใช้ได้กับ second-order logic และสูงขึ้นไป 
[4] บางคนนิยามความสมบูรณ์ให้ตรงข้ามกับ soundness แทน ความไม่สมบูรณ์ก็จะหมายความว่ามีความจริงที่พิสูจน์ไม่ได้
[5] Soundness implies ความไม่ขัดแย้งในตัวเอง ในทางกลับกัน ความขัดแย้งในตัวเอง implies unsoundness
[6] เครื่องจักร Turing ในทฤษฎีมีเทปที่ยาวไม่รู้จบ แต่ปัญหาที่เราคิดว่าแก้ได้ในทางปฏิบัติไม่จำเป็นต้องใช้เทปยาวไม่รู้จบ (เพราะ “PSPACE เป็นคลาสที่ใหญ่มาก”)
[7] โมเดลที่พลังน้อยกว่าก็มีอย่าง finite state automata กับ pushdown automata ที่ไม่สามารถแก้บางปัญหาที่เครื่องจักร Turing แก้ได้
[8] ชื่อโพสท์ที่คิดขึ้นมาตอนแรกคือ “ตรรกะคือการคำนวณ” ซึ่งทำให้ไปเจอ “บทพิสูจน์คือโปรแกรม” ของ Philip Wadler ในภายหลัง
[9] Stuart Armstrong, “Completeness, incompleteness, and what it all means: first versus second order logic
[10] คำตอบของ Ron Maimon บน Philosophy Stack Exchange