หนังสือพยายามอธิบายพื้นฐานและพื้นเพของ paper ที่ยาก ซับซ้อน และโด่งดังปี 1938 ของเกอเดล (ตอนตีพิมพ์เปเปอร์นี้เกอเดลเพิ่งจะ 25) Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme (ว่าด้วยประพจน์ที่ไม่อาจตัดสินได้อย่างเป็นรูปแบบ (หรืออย่าง formal) ของ Principia Mathematica (หมายถึงหนังสือของรัสเซลกับไวท์เฮด) กับระบบทำนองเดียวกัน) ซึ่งแสดง incompleteness theorem พูดง่าย ๆ ก็คือ วิธีการแบบ axiomatic (เช่น วิธีที่ยุคลิดใช้พัฒนาเรขาคณิตอย่างเป็นระบบโดยเริ่มต้นจากเซ็ตของสัจพจน์ หรือ axiom) จะมีขีดจำกัดบางอย่างที่ทำให้สมบัติ (หรือประพจน์) ของระบบบางระบบ เช่น ระบบง่าย ๆ อย่างจำนวนเต็มที่ไม่ติดลบ ไม่สามารถ axiomized ได้
ผู้เขียนเริ่มจากการสำรวจปัญหา consistency ของฮิลแบร์ต ก่อนศตวรรษที่ 19 นะครับ นี่เป็นปัญหาที่ไม่มีใครเอามาขบคิดจริงจังว่า ทฤษฎีบทที่ขัดแย้งกันจะสามารถสร้าง (deduce) ขึ้นมาจากเซ็ตของสัจพจน์เดียวกันได้มั้ย นั่นคือ ยิ่งคณิตศาตร์พัฒนาให้เป็นนามธรรมมากขึ้น ๆ และความคิดที่ว่าความจริงทั้งหมดสามารถอธิบายและพิสูจน์ได้ด้วยการยอมรับสัจพจน์บางอย่าง คำถามคือ เรารู้ได้อย่างไรว่าเซ็ตของสัจพจน์ที่เป็นรากฐานของมันนั้นสอดคล้องกัน (internally consistent) ตัวอย่างเช่น ในเรขาคณิต elliptic ซึ่งแทนที่สัจพจน์ขนานของยุคลิดด้วยสมมติฐานที่ว่า เราไม่สามารถลากเส้นผ่านจุดหนึ่งจุดที่อยู่นอกเส้นอีกเส้นหนึ่งแล้วทำให้เส้นทั้งสองนั้นขนานกันได้ ทีนี้ ตั้งคำถามว่าเซ็ตของสัจพจน์ในเรขาคณิตแบบ elliptic สามารถทำให้เกิดทฤษฎีบทสองอันที่ขัดแย้งกันได้มั้ย แน่นอนว่า เราไม่สามารถยกทฤษฎีบทที่สร้างภายใต้สัจพจน์ของมันที่ไม่ขัดแย้งกันที่เรารู้ตอนนี้แล้วบอกว่า นี่ไง ไม่เห็นขัดแย้งกันเลย เพราะเป็นไปได้ว่าทฤษฎีบทที่เรายังไม่รู้ อาจจะขัดแย้งกับตัวใดตัวหนึ่งก่อนหน้าก็ได้ ทางออกหนึ่งสำหรับปัญหานี้คือการหาโมเดล (หรือการตีความ) สำหรับสัจพจน์ที่เป็นนามธรรมของระบบเพื่อให้แต่ละสัจพจน์ถูกแปลงไปเป็นข้อความที่เป็นจริงเกี่ยวกับโมเดล แต่ทางออกดังกล่าวนี้เป็นเพียงการแก้ปัญหาโดยทำให้ปัญหาหลุดจากโดเมนหนึ่งไปกองอยู่ที่อีกโดเมนหนึ่ง เช่นเราอาจแสดงได้ว่าระบบเรขาคณิตจะ consistent ถ้าพีชคณิต consistent ทางออกนี้จึงไม่ใช่การพิสูจน์ที่สัมบูรณ์ (absolute proof) (นอกจากนี้ยังมีประเด็นปัญหาเกี่ยวกับ finite vs non-finite models เพราะมีคณิตศาสตร์หลายแขนงที่ไม่สามารถจับคู่กับ finite model)
ต่อมา ฮิลแบร์ตก็ได้เสนอวิธีพิสูจน์แบบสัมบูรณ์ (หมายความว่า เราสามารถแสดง consistency ของระบบใด ๆ ได้โดยไม่ต้องพูดว่า ระบบนี้จะ consistent ถ้าระบบโน้น consistent) ขั้นแรกของการสร้าง absolute proof คือการทำให้เป็นระบบ formal ที่สมบูรณ์ (complete formalization) ซึ่งทำได้โดยถอดเอาความหมายทั้งหมดออกไปจากระบบให้เหลือเพียงสัญลักษณ์เปล่า ๆ (เราเรียกระบบของสัญลักษณ์นี้ว่า calculus) ฉะนั้น สัจพจน์หรือทฤษฎีบทของระบบ formal ที่สมบูรณ์ก็คือลำดับของสัญลักษณ์ที่มีความยาวจำกัดซึ่งสามารถสร้างขึ้นมาได้จากกฎการรวมกันของสัญลักษณ์พื้นฐานของระบบ ในแง่นี้ การแสดงการพิสูจน์ (derivation) ของทฤษฎีบทก็คือการแปลง (transformation) จากลำดับของสัญลักษณ์ชุดหนึ่งไปเป็นอีกลำดับนั่นเอง การทำแบบนี้จะเปิดเผยโครงสร้างของระบบ ทีนี้ ถึงแม้ลำดับของสัญลักษณ์เปลือยเปล่าของ formalized mathematics จะไม่ได้บอกอะไรเลย เพราะมันไม่มีความหมายอะไรเลย แต่ก็เป็นไปได้ว่า เราสามารถสร้างประโยคที่เกี่ยวกับลำดับของสัญลักษณ์นั้นที่มีความหมายขึ้นมาได้ แต่ประโยคดังกล่าวไม่ได้เป็นของระบบ ฮิลแบร์ตเรียกประโยคเหล่านี้ว่า meta-mathematics เช่น ลำดับของสัญลักษณ์ 2+3=5 เป็นข้อความในระบบเลขคณิต ส่วนข้อความ '2+3=5' เป็นสูตรเลขคณิต เป็น meta-mathematics
การสร้าง absolute proof of consistency ของฮิลแบร์ตก็อยู่บนการแยกความแตกต่างระหว่าง formal calculus กับ meta-mathematics นี่แหละครับ ฮิลแบร์ตว่า เราสามารถแสดง absolute proof of consistency ของทฤษฎีจำนวนที่ถูก formalized แล้ว (ถ้าเราสามารถสร้างข้อพิสูจน์ดังกล่าวได้นะ) ได้ด้วยการแสดงขั้นตอนผ่าน meta-mathematics (และขึ้นตอนดังกล่าวเป็น finistic หมายถึง เป็นขั้นตอนที่ไม่อ้างถึงอะไรที่เป็นอนันต์) เพื่อแสดงให้เห็นว่าสูตรที่ขัดแย้งกันสองสูตรไม่สามารถสร้างขึ้นจากกฎที่กำหนด (rules of inference) ไว้จากสัจพจน์ หนังสือได้ยกตัวอย่างการพิสูจน์ว่า sentential calculus (หรือ the logic of propositions) เป็นระบบที่ consistent ด้วย absolute proof โดยการแสดงว่า ถ้าระบบไม่ consistent เราสามารถสร้างได้ทั้ง formulas S และ ¬S จากสัจพจน์ ผลที่ตามมาคือ ทำให้ทุกอย่างก็สามารถสร้างได้จากสัจพจน์ เพราะใน sentential calculus เรามีทฤษฎีบท p⊃(¬p⊃q) ซึ่งหลังจากแทน p ด้วย S จะได้ S⊃(¬S⊃q) และในเมื่อ S และ ¬S เป็น formula ที่สร้างได้จากสัจพจน์ ฉะนั้น q ก็เป็นด้วย ฉะนั้น ถ้าเราจะแสดงว่า sentential calculus เป็นระบบที่ consistent เราก็แค่แสดงว่า มี formula อย่างน้อยหนึ่งตัวที่ไม่สามารถสร้างขึ้นมาได้จากสัจพจน์ วิธีทำคือ เราจะให้เหตุผลผ่าน meta-mathematics โดยการมองหาสมบัติเชิงโครงสร้างหรือลักษณะเฉพาะของ formula ที่เป็นไปตามเงื่อนไข 3 ข้อต่อไปนี้ (1) สมบัติดังกล่าวต้องเป็นสมบัติร่วมของสัจพจน์ (ใน sentential calculus มีสัจพจน์เพียง 4 ข้อ คือ 1. (p∨q)⊃p, 2. p⊃(p∨q), 3. (p∨q)⊃(q∨p) และ 4. (p⊃q)⊃((r∨p)⊃(r∨q))), (2) สมบัตินั้นจะต้องถ่ายทอดได้ (hereditary) ภายใต้ transformation rules (ใน sentential calculus คือ rule of substitution กับ modus ponens) และ (3) สมบัติดังกล่าวจะต้องไม่เป็นของ formula ทุกตัวที่สามารถสร้างได้จาก formation rules (คนละอย่างกับ transformation rules นะครับ มันคือตัวที่ใช้บอกว่าลำดับของสัญลักษณ์อันไหนเป็น formula อันไหนไม่เป็น เช่น p∨q เป็น แต่ pq∨ ไม่เป็น) นั่นคือ ถ้าเราสามารถหาสมบัติที่ผ่านเงื่อนไข 3 ข้อนี้ได้ เราก็จะประสบผลสำเร็จในการพิสูจน์ consistency ของ sequential calculus ซึ่งในกรณีนี้ก็ไม่ยากเย็นอะไร เราเลือกสมบัติคือสัจนิรันดร์ (tautology) แล้วพูดว่า p∨q ไม่เป็น tautology จบ นั่นคือ เราแสดงอย่างน้อยหนึ่งสูตรที่ไม่เป็นทฤษฎีบท
เนื่องจากในระบบตัวอย่างนี้ ทุกทฤษฎีบทเป็นความจริงหรือสัจนิรันดร์ จึงชวนให้ตั้งคำถามย้อนกลับว่า ความจริงทุกอย่างที่สามารถเขียนได้ด้วยคำศัพท์ของระบบนี้สามารถพิสูจน์จากสัจพจน์ได้มั้ย (หรือเป็นทฤษฎีบทมั้ย) คำตอบสำหรับคำถามนี้คือได้ (หรือเป็น) นะครับ แต่ไม่ได้พิสูจน์ง่าย ๆ ประเด็นคือ คำถามย้อนกลับดังกล่าวทำให้เกิดความคิดเรื่อง completeness เราจะพูดว่าระบบไหนก็ตาม complete ถ้าเซ็ตของสัจพจน์เพียงพอที่จะสร้างสูตรที่เป็นจริงทั้งหมด และก่อนหน้าเกอเดล นักคณิตศาสตร์เชื่อว่าเซ็ตของสัจพจน์สำหรับทฤษฎีจำนวนนั้นเพียงพอที่จะสร้างทฤษฎีบททั้งหมดในระบบของทฤษฎีจำนวน (หรือถ้าไม่เชื่อแบบนี้ ก็เชื่อว่า ยังไงก็ต้องสามารถเพิ่มสัจพจน์บางข้อเข้าไปในเซ็ต เพื่อทำให้มันสมบูรณ์ได้) แต่สิ่งที่เกอเดลค้นพบ หักล้างความเชื่อดังกล่าวโดยสิ้นเชิง
ข้อสรุปของเกอเดลคือ ระบบอย่างใน Principia หรือระบบที่สามารถพัฒนาเลขคณิตขึ้นมาได้นั้น incomplete พูดอีกอย่างคือ สำหรับ consistent formalization ของทฤษฎีจำนวนใด ๆ จะต้องมีทฤษฎีบททางเลขคณิตที่ไม่สามารถพิสูจน์ได้ภายในระบบ
เนื้อหาสำคัญที่สุดของหนังสือคือความพยายามอธิบายว่าเกอเดลพิสูจน์ข้อสรุปตามย่อหน้าที่แล้วได้อย่างไร ผู้เขียนเกริ่นถึง Richard paradox ซึ่งสไตลด์ที่เกอเดลใช้ในการพิสูจน์จะคล้ายกับ paradox อันนี้แต่สร้างโดยหลีกเลี่ยง fallacy ที่เกิดขึ้นกับ paradox โดยเกอเดลแสดงให้เห็นว่า ข้อความในระดับ meta-mathematics ที่เกี่ยวกับ formalized arithmetical calculus สามารถแสดงได้ด้วยสูตรเลขคณิตภายใน calculus
หนังสือฉบับพิมพ์ใหม่ ได้ Hofstadter (ซึ่งเคยเจอหนังสือเล่มนี้ในร้านหนังสือตอนเป็นเด็ก และเคยอ่านด้วยความชื่นชมมาก่อน) มาเป็น editor ความเห็นรวมถึงข้อความอธิบายเพิ่มเติมจาก Hofstadter ช่วยได้มากครับ ถึงแม้หนังสือจะพยายามทำเรื่องยากให้ง่าย และ self-contained แต่สำหรับเรื่องที่ยากจริง ๆ อย่างวิธีที่เกอเดลใช้พิสูจน์ทฤษฎีบทความไม่สมบูรณ์ มันก็ไม่ได้อ่านง่ายขนาดนั้น สำหรับคนชอบอะไรสนุก ๆ ท้าทาย เชิญครับ
ปล. ถ้าคุณรู้ background ทั้งหมดที่เขียนเล่ามา และอยากให้โอกาสเล่มนี้ในเวลาจำกัด เริ่มที่บทที่ 7 Gödel's Proof ได้เลย