مسئله تصمیم‌ناپذیر
مثال‌هایی از گزاره‌های غیرقابل حل

دو معنای متفاوت از کلمه غیرقابل حل در استفاده امروزی، وجود دارد. اولین معنا در رابطه با نظریه‌های گودل استفاده می‌شود بدین معنا که یک گزاره در سیستم استنباطی خاصی نه اثبات پذیر و نه رد کردنی است. دومین معنا در ارتباط با نظریه محاسبه استفاده می‌شود در مورد گزاره‌ها به کار نمی‌رود، بلکه در مورد مسائل حل شدنی به کار می‌رود که از نظر قابل شمارش بودن، مجموعه‌های بی پایانی از سوالاتی هستند که هر کدام به یک جواب بله یا نه نیاز دارند. به چنین مسئله‌ای غیرقابل حل گفته می‌شود اگر عملیات محاسبه که به درستی به هر سؤال در مجموعه مسئله پاسخ دهد، وجود نداشته باشد. ارتباط بین این دو معنا این است که اگر مسئله حل شدنی قابل حل نباشد (در معنای تئوری بازگشتی) پس دستگاه رسمی مؤثر محکی که ثابت کند برای هر سؤال A در مسئله یا «جواب A بله است یا جواب A خیر ست» وجود ندارد.
به خاطر این دو، معنای کلمه غیرقابل حل، واژه مستقل، گاهی به جای غیرقابل حل بودن، معنای «نه اثبات پذیر نه رد کردنی» استفاده می‌شود. به هر حال استعمال واژه «مستقل» نیز مبهم است: این واژه می‌تواند فقط معنای «غیرقابل اثبات» دهد در حالی که فضا را برای برداشت آن که یک گزاره مستقل ممکن است رد کردنی باشد، را نیز باز بگذارد.
غیرقابل حل بودن یک گزاره در یک دستگاه استنباطی خاص در دستگاه خودش، به این سؤال اشاره می‌کند که آیا صحت مدار گزاره به خوبی تعریف شده یا آیا می‌تواند با شیوه‌های دیگری تعیین شود. عدم قطعیت فقط اشاره به این دارد که دستگاه استنباطی خاص مورد نظر صحت یا عدم صحت گزاره را ثابت نمی‌کند. هر چند وجود گزاره‌های به اصطلاح کاملاً غیرقابل حل که صحت مقدار آن‌ها یا شناخته شده نیست یا غیر مشخص است، موضوع بحث‌برانگیزی در بین مدارس مختلف فلسفه است.
یکی از اولین مسائلی که مشکوک به غیرقابل حل هستند در معنای دوم واژه، کلمه مسئله برای گروه‌ها است که اولین بار به وسیلهٔ Max Dehn در سال۱۹۱۱ مطرح شد، که از وجود یک گروه ارائه شده پایان پذیر می‌پرسد که برای آن‌ها الگوریتمی وجود ندارد تا تعیین کند آیا دو کلمه ارز هستند یا نه.
این مسئله در سال۱۹۵۲ مطرح شد.
کار ترکیبی گودل و پاول کوهن، دو مثال دقیق از گزاره‌های غیرقابل حل (در معنای اول کلمه) ارائه می‌دهد: فرضیه سلسله که در ZFC (بدیهی سازی استاندارد تئوری مجموعه) نه اثبات و نه رد می‌شود، و اصل بدیهی انتخاب که در ZF (که همگی به جزء اصل بدیهی گزینه، اصول بدیهی ZFC هستند) نه اثبات و نه رد می‌شود.
این نتایج در تئوری ناقص مورد نیاز نیستند. گودل در سال۱۹۴۰ ثابت کرد که هیچ‌یک از این گزاره‌ها در تئوری مجموعه XFC یا XF نمی‌توانند غیرقابل اثبات باشند.
در سال۱۹۶۰، کوهن اثبات کد که هیچ‌یک از گزاره‌های XF قابل اثبات نیستند و فرضیه زنجیره نمی‌تواند از تئوری مجموعه XFC اثبات شود.
در سال۱۹۷۰، ریاضیدان روس یوری ماتیاسویچ نشان داد که مسئله دهم هیلبرت که در سال۱۹۰۰ به عنوان چالشی در برابر ریا ضی دانان قرن آینده مطرح شده بود، قابل حل نبود. چالش هیلبرت به دنبال الگوریتمی بود که همه راه حل‌های معادله Diophantine را پیدا کند. معادله Diophantine مورد کلی‌ترین از نظریه آخر Fermal بود، ما به دنبال ریشه‌های عدد صحیح یک چند جئی د هر عدد متغیر با ضرایب عدد صحیح هستیم؛ بنابراین با داشتن فقط یک معادله اما با n متغیر و وجود راه حل‌های بی پایان بسیاری (که به آسانی یافت می‌شوند) در طرح پیچیده، مسئله با تمرکر فقط بر روی راه حل‌های مقادیر عدد صحیح، دشوار می‌شود.
ماتیاسوویچ با رسم معادله Diophantine، با یک مجموعه محاسبه‌ای برگشتی و با متوسل شدن به نظریه ناقص گودل، نشان که این مسئله غیرقابل حل است.
در سال۱۹۳۶، آلن تورینگ ثابت کد که مسئله پایان ناپذیر – پرسیدن از این که آیا یک تورینگ به برنامه داده شد، خاتمه پیدا می‌کند یا نه – در معنای دوم کلمه غیرقابل حل است. این نتیجه بعدها به وسیلهٔ نظریه رایس عمومیت داده شد.
در سال۱۹۷۳ نشان داده شد که مسئله Whitehead در نظریه گروه، در معنای اول واژه در نظریه مجموعه استاندارد غیرقابل حل است.
در سال۱۹۷۷ پاریس و هارینتگتون ثابت کردند که اصل پاریس – هارینگتون، نسخه‌ای از نظریه رامسی در بدیهی سازی عددی فرض شده به وسیله اصول بدیهی Peano غیرقابل حل هست. اما می‌توان اثبات کرد که در دستگاه بزرگ‌تر عددی نوع دوم درست باشد.
نظریه نمودار درختی کروسکال که در علوم کامپیوتر کاربردهایی دارد نیز از اصول بدیهی Peano غیرقابل حل است اما در نظریه مجموعه قابل اثبات است. در حقیقت نظریه نمودار درختی کروسکال (یا شکل پایان پذیر آن) در یک دستگاه بسیار قوی تر که به وسیله اصول مورد قبولی که بر پایه فلسفه ریاضیات معروف به گزاره اتمی هستند، غیرقابل حل هست.
نظریه گودرتین، گزاره دربارهٔ نظریه رامسی از اعداد طبیعی است که کیربی و پاریس در Peano نشان دادند که غیرقابل حل است.
گریگوری چایتین، گزاره‌هایی غیر قطعی از نظریه اطلاعات الگوریتمی فراهم کرد و نظریه ناقص بودن دیگری در آن زمینه ثابت کرد. نظریه چایتین بیان می‌کند که برای هر نظریه‌ای که بتوان علم اعداد کافی ارائه کرد، C مسلم بالاتری وجود دارد به طوری که عدد خاصی وجود نداشته باشد که در آن نظریه ثابت شده باشد که پیچیدگی کولکوگرو بزرگ‌تر از C داشته باشد. در حالی که نظریه گودل به تناقض گویی کذاب liar و نتایج چایتین به تناقض گویی Berry مربوط است.
در سال۲۰۰۷ محققان کورثر و سایمون با تکیه بر کار اولیه جی.اچ. کانوی در سال۱۹۷۰، ثابت کردند که تعمیم طبیعی مسئله کولاتز، غیرقابل حل است.