**قضایای ناتمامیت گودل** شامل دو قضیه بنیادین در منطق ریاضی هستند که [[کورت گودل]] در سال ۱۹۳۱ میلادی در مقاله تاریخی خود درباره گزاره‌های تصمیم‌ناپذیر صوری منتشر کرد ((کورت گودل، مقاله Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I در نشریه Monatshefte für Mathematik und Physik، سال ۱۹۳۱ میلادی)). این دو قضیه محدودیت‌های ذاتی و گریزناپذیر تمامی دستگاه‌های اصل‌موضوعه‌ای صوری را که قادر به بیان حساب اعداد طبیعی هستند آشکار ساخته و مسیر [[فلسفه ریاضی]]، منطق و علوم کامپیوتر نظری را برای همیشه دگرگون کردند.
<قضایای ناتمامیت گودل ثابت می‌کنند که «حقیقت ریاضی» فراتر از «اثبات‌پذیری صوری» است و هیچ دستگاه اصل‌موضوعه‌ای واحدی نمی‌تواند تمامی حقایق مربوط به اعداد طبیعی را دربرگیرد.>
# بستر تاریخی و تقابل با برنامه هیلبرت #
در دهه‌های آغازین سده بیستم، به دنبال کشف [[پارادوکس راسل]] در نظریه مجموعه‌های شهودی، ریاضی‌دانان به دنبال بنیانی استوار و عاری از تناقض برای ریاضیات بودند. در یک سو، برتراند راسل و آلفرد نورث وایتهد در کتاب «پرینکیپیا ماتماتیکا» تلاش کردند کل ریاضیات را به منطق فروکاهند ((آلفرد نورث وایتهد و برتراند راسل، کتاب Principia Mathematica، انتشارات دانشگاه کمبریج، ۱۹۱۰ تا ۱۹۱۳ میلادی))؛ و در سوی دیگر، [[داوید هیلبرت]] طرح جاه‌طلبانه‌ای موسوم به [[برنامه هیلبرت]] را پی‌ریزی کرد.
هدف هیلبرت آن بود که کل ریاضیات را در قالب یک دستگاه صوریِ دارای سه ویژگی اصلی صورت‌بندی کند:
1. **تمامیت «Completeness»:** برای هر گزاره ریاضی ${\varphi}$، بتوان یا خودِ ${\varphi}$ یا نقیض آن یعنی ${\neg \varphi}$ را در دستگاه اثبات کرد.
2. **سازگاری «Consistency»:** نتوان هیچ تناقضی به شکل ${\varphi \land \neg \varphi}$ را از اصول موضوعه استنتاج کرد.
3. **اثبات متناهی‌گرایانه سازگاری:** بتوان سازگاری دستگاه‌های بزرگ ریاضی را با روش‌های کاملاً متناهی و بی‌نیاز از فرض‌های نامتناهی به اثبات رساند.
گودل تنها یک سال پس از اثبات [[قضیه تمامیت گودل]] برای [[منطق مرتبه اول]]، با کشف قضایای ناتمامیت نشان داد که تحقق هم‌زمان این اهداف برای نظریه‌های حاوی حساب، از نظر منطقی ناممکن است.
# شرایط و پیش‌فرض‌های دقیق قضایای گودل #
قضایای ناتمامیت گودل در مورد **هر** دستگاه صوری صدق نمی‌کنند، بلکه ناظر بر دستگاه‌های صوری‌ای مانند ${F}$ هستند که دارای سه ویژگی مشخص باشند:
* **اصل‌موضوعه‌پذیری مؤثر «Effective Axiomatization»:** مجموعه اصول موضوعه و قواعد استنتاج دستگاه ${F}$ باید «تصمیم‌پذیر» یا بازگشتی باشند؛ به این معنا که یک الگوریتم مکانیکی بتواند بررسی کند آیا یک دنباله متناهی از فرمول‌ها، اثباتی معتبر در ${F}$ هست یا خیر.
* **غنای بیانی کافی «Sufficient Expressiveness»:** دستگاه ${F}$ باید توانایی بیان و اثبات خواص پایه اعداد طبیعی شامل جمع و ضرب را داشته باشد؛ یعنی دست‌کم به قدرت [[حساب رابینسون]] یا [[حساب پئانو]] باشد.
* **سازگاری «Consistency»:** دستگاه ${F}$ نباید متناقض باشد، یعنی ${F \nvdash \bot}$.
# سازوکار فنی اثبات: حسابی‌سازی نحو #
نبوغ گودل در آن بود که نشان داد یک نظریه ریاضی که درباره «اعداد طبیعی» سخن می‌گوید، می‌تواند به صورت غیرمستقیم درباره «فرمول‌ها و اثبات‌های خودش» نیز سخن بگوید. این فرآیند در سه گام کلیدی انجام می‌شود:
## ۱. شماره‌گذاری گودل «Gödel Numbering» ##
گودل روشی ابداع کرد که به هر نماد پایه، هر فرمول خوش‌ساخت و هر دنباله‌ای از فرمول‌ها در زبان صوری ${F}$، یک عدد طبیعی یکتا نسبت می‌دهد. اگر به نمادهای پایه اعداد فردی اختصاص دهیم، یک فرمول که دنباله‌ای از نمادها با کدهای ${s_1, s_2, \dots, s_k}$ است، با استفاده از تجزیه یکتا به اعداد اول، به عدد طبیعی زیر نگاشت می‌شود:
$$
\operatorname{enc}(s_1, s_2, \dots, s_k) = 2^{s_1} \cdot 3^{s_2} \cdot 5^{s_3} \cdots p_k^{s_k}
$$
عدد حاصل از این نگاشت برای فرمول ${\varphi}$ را «عدد گودل» آن فرمول می‌نامیم و نمادِ ترمِ متناظر با آن در زبان حساب را با ${\ulcorner \varphi \urcorner}$ نمایش می‌دهیم.
## ۲. بازنمایی‌پذیری محمول اثبات ##
گودل ثابت کرد که هر رابطه «بازگشتی ابتدایی» میان اعداد طبیعی، در داخل دستگاه حسابی ${F}$ قابل فرمول‌بندی است. از آنجا که بررسی صحت یک اثبات صوری یک فرآیند کاملاً الگوریتمی و بازگشتی ابتدایی است، می‌توان فرمولی دو متغیره مانند ${\operatorname{Prf}_F(x, y)}$ در زبان حساب ساخت که معنای آن چنین است: «عدد ${x}$ کد گودلِ یک اثبات معتبر در دستگاه ${F}$ برای فرمولی با کد گودل ${y}$ است».
با بستن متغیر ${x}$ توسط سور وجودی، «محمول اثبات‌پذیری» در داخل زبان ${F}$ تعریف می‌شود:
$$
\operatorname{Prov}_F(y) \equiv \exists x \, \operatorname{Prf}_F(x, y)
$$
تفاوت حیاتی در اینجاست که برای یک عدد مشخص ${m}$، رابطه ${\operatorname{Prf}_F(m, \ulcorner \varphi \urcorner)}$ در داخل ${F}$ تصمیم‌پذیر است، اما به دلیل حضور سور وجودی نامقید ${\exists x}$، فرمول ${\operatorname{Prov}_F(\ulcorner \varphi \urcorner)}$ دیگر تصمیم‌پذیر نیست و صرفاً یک فرمول از مرتبه ${\Sigma_1^0}$ در سلسله‌مراتب حسابی محسوب می‌شود.
## ۳. لم قطری‌سازی و ساخت گزاره گودل ##
با الهام از روش قطری کانتور و ساختار [[پارادوکس دروغگو]]، گودل «لم نقطه ثابت» یا «لم قطری‌سازی» را اثبات کرد ((رادولف کارنپ در سال ۱۹۳۴ صورت کلی این لم را برای هر ویژگی نحوی صورت‌بندی کرد)): برای هر فرمول یک‌متغیره ${\psi(x)}$ در زبان ${F}$، گزاره‌ای بسته مانند ${G}$ وجود دارد که در داخل دستگاه ${F}$ هم‌ارز با نسبت دادن ویژگی ${\psi}$ به کد گودلِ خودِ ${G}$ است:
$$
F \vdash G \leftrightarrow \psi(\ulcorner G \urcorner)
$$
حال اگر به جای ${\psi(x)}$، فرمولِ «اثبات‌ناپذیر بودن» یعنی ${\neg \operatorname{Prov}_F(x)}$ را قرار دهیم، به **گزاره گودل** می‌رسیم:
$$
F \vdash G \leftrightarrow \neg \operatorname{Prov}_F(\ulcorner G \urcorner)
$$
<گزاره گودل در زبان ریاضیِ محض ساخته شده است، اما در سطح فرامنطقی دقیقاً می‌گوید: «من در دستگاه صوری ${F}$ قابل اثبات نیستم».>
# قضیه اول ناتمامیت گودل #
با در دست داشتن گزاره ${G}$، قضیه اول ناتمامیت از تحلیل دو حالت ممکن استنتاج می‌شود:
* **حالت اول «اثبات‌ناپذیری خودِ گزاره»:** فرض کنید ${F \vdash G}$. در این صورت اثباتی با کد مشخص برای ${G}$ وجود دارد، پس دستگاه ${F}$ می‌تواند وجود این اثبات را تایید کند، یعنی ${F \vdash \operatorname{Prov}_F(\ulcorner G \urcorner)}$. اما از هم‌ارزیِ نقطه ثابت می‌دانیم ${F \vdash G \to \neg \operatorname{Prov}_F(\ulcorner G \urcorner)}$؛ لذا به تناقضِ ${F \vdash \neg \operatorname{Prov}_F(\ulcorner G \urcorner)}$ می‌رسیم. بنابراین اگر ${F}$ سازگار باشد، حتماً ${F \nvdash G}$.
* **حالت دوم «اثبات‌ناپذیری نقیض گزاره»:** از آنجا که در حالت اول دیدیم ${G}$ در دستگاه ${F}$ اثبات‌پذیر نیست، هیچ عدد طبیعی‌ای مانند ${n}$ کدِ اثباتِ ${G}$ نیست. پس برای هر عدد طبیعی استاندارد ${n \in \mathbb{N}}$ داریم ${F \vdash \neg \operatorname{Prf}_F(\overline{n}, \ulcorner G \urcorner)}$. اگر دستگاه ${F}$ دارای ویژگی «امگا-سازگاری» باشد، نمی‌تواند هم‌زمان با رد کردن تک‌تک مصداق‌های عددی، گزاره وجودی ${\exists x \, \operatorname{Prf}_F(x, \ulcorner G \urcorner)}$ یعنی ${\neg G}$ را اثبات کند؛ بنابراین ${F \nvdash \neg G}$.
در سال ۱۹۳۶ میلادی، بارکلی راسر با اصلاح ظریف گزاره گودل، شرط «امگا-سازگاری» را حذف کرد و نشان داد که صرفِ سازگاری عادی دستگاه ${F}$ برای اثبات‌ناپذیریِ هر دو گزاره کافی است ((بارکلی راسر، مقاله Extensions of some theorems of Gödel and Church در مجله Journal of Symbolic Logic، سال ۱۹۳۶ میلادی)).
$$
\operatorname{Con}(F) \implies \left( F \nvdash G_R \right) \land \left( F \nvdash \neg G_R \right)
$$
نکته شگفت‌انگیز فلسفی این است که چون ${F \nvdash G}$، گزاره ${G}$ که مدعیِ اثبات‌ناپذیریِ خویش است، در **مدل استاندارد اعداد طبیعی** صادق است، یعنی ${\mathbb{N} \models G}$؛ ما حقیقتی ریاضی را در فرامنطق می‌بینیم که خودِ دستگاه ${F}$ از اثبات آن ناتوان است.
# قضیه دوم ناتمامیت گودل #
قضیه دوم ناتمامیت گودل گامی فراتر برمی‌دارد و استدلالِ قضیه اول را در **داخل خودِ دستگاه ${F}$** صورت‌بندی می‌کند. گزاره «دستگاه ${F}$ سازگار است» به زبان حسابی چنین بیان می‌شود که تناقض صوری اثبات‌پذیر نیست:
$$
\operatorname{Con}(F) \equiv \neg \operatorname{Prov}_F(\ulcorner \bot \urcorner)
$$
پاول برنایز و داوید هیلبرت نشان دادند که محمول اثبات‌پذیری ${\operatorname{Prov}_F}$ در هر نظریه شامل [[حساب پئانو]] در سه شرط بنیادی موسوم به «شرایط استنتاج‌پذیری هیلبرت-برنایز-لوب» صدق می‌کند:
1. اگر ${F \vdash \varphi}$، آنگاه ${F \vdash \operatorname{Prov}_F(\ulcorner \varphi \urcorner)}$.
2. ${F \vdash \operatorname{Prov}_F(\ulcorner \varphi \to \psi \urcorner) \to \left( \operatorname{Prov}_F(\ulcorner \varphi \urcorner) \to \operatorname{Prov}_F(\ulcorner \psi \urcorner) \right)}$.
3. ${F \vdash \operatorname{Prov}_F(\ulcorner \varphi \urcorner) \to \operatorname{Prov}_F(\ulcorner \operatorname{Prov}_F(\ulcorner \varphi \urcorner) \urcorner)}$.
با استفاده از این سه شرط، استدلالِ بخش اولِ قضیه ناتمامیت یعنی «اگر ${F}$ سازگار باشد، آنگاه ${G}$ اثبات‌پذیر نیست» به یک قضیه رسمی در داخل خودِ ${F}$ تبدیل می‌شود:
$$
F \vdash \operatorname{Con}(F) \to G
$$
حال اگر دستگاه سازگار ${F}$ بتواند سازگاری خودش را اثبات کند، یعنی ${F \vdash \operatorname{Con}(F)}$، به حکم قاعده وضع مقدم خواهیم داشت ${F \vdash G}$، که صریحاً ناقض قضیه اول ناتمامیت است!
<قضیه دوم ناتمامیت گودل: هیچ دستگاه صوری سازگار، بازگشتی و شامل حساب پئانو نمی‌تواند سازگاری درونی خودش را اثبات کند؛ یعنی ${F \nvdash \operatorname{Con}(F)}$.>
# پیوند با تمامیت، تصمیم‌پذیری و فلسفه ذهن #
قضایای ناتمامیت گودل شبکه وسیعی از نتایج میان‌رشته‌ای را در سده بیستم رقم زدند:
* **پیوند با [[قضیه تمامیت گودل]] و مدل‌های غیراستاندارد:** طبق قضیه تمامیت، اگر ${F \nvdash G}$، پس نظریه ${F \cup \{\neg G\}}$ سازگار است و دارای یک مدل ریاضی مانند ${\mathcal{M}^*}$ است. در این ساختارِ غیراستاندارد، گزاره ${\exists x \, \operatorname{Prf}_F(x, \ulcorner G \urcorner)}$ صادق است؛ یعنی در مدل ${\mathcal{M}^*}$ یک «عدد طبیعی غیراستاندارد و نامتناهی بزرگ» وجود دارد که نقش کد اثبات ${G}$ را بازی می‌کند، در حالی که هیچ عدد طبیعی متناهی و استانداردی در ${\mathbb{N}}$ چنین خاصیتی ندارد.
* **[[مسئله توقف]] و نظریه محاسبه:** در سال ۱۹۳۶ میلادی، [[آلن تورینگ]] با الهام از قطری‌سازی گودل نشان داد که مسئله توقف ماشین تورینگ تصمیم‌ناپذیر است ((آلن تورینگ، مقاله On Computable Numbers, with an Application to the Entscheidungsproblem، سال ۱۹۳۶ میلادی)). در واقع ناتمامیت گودل و توقف‌ناپذیری تورینگ دو روی یک سکه هستند: اگر حساب کامل و تصمیم‌پذیر بود، مسئله توقف نیز حل‌پذیر می‌شد.
* **[[قضیه تعریف‌ناپذیری تارسکی]]:** آلفرد تارسکی با تعمیم روش گودل ثابت کرد که در حالی که «اثبات‌پذیری» در داخل زبان حساب قابل تعریف است، مفهوم «صدق حسابی» هرگز در داخل خودِ زبان قابل تعریف نیست.
* **مباحثات در [[فلسفه ذهن]] و هوش مصنوعی:** متفکرانی چون جان لوکاس و [[راجر پنروز]] با استناد به قضایای گودل استدلال کرده‌اند که ذهن انسان می‌تواند صدق گزاره گودل ${G}$ را دریابد، در حالی که هیچ ماشین الگوریتمیِ معادل با دستگاه صوری ${F}$ قادر به اثبات آن نیست؛ ادعایی که همچنان یکی از چالش‌برانگیزترین مباحث میان فیزیک‌دانان، منطق‌دانان و فیلسوفان ذهن است.