برنامه هیلبرت
برنامهٔ هیلبرت (Hilbert's program) که به وسیلهٔ دیوید هیلبرت در دههٔ ۱۹۲۰ (م) فرمول‌بندی شد، بنا بود به بیان صوری (formal) همهٔ نظریّه‌های موجود در آن زمان به شکل یک مجموعهٔ متناهی از اصول موضوع پرداخته، و نیز براهینی ارائه نماید که آن اصول با هم سازگار است.
در ریاضیات، برنامه هیلبرت، که توسط ریاضیدان آلمانی، دیوید هیلبرت، در اوایل قرن ۲۰، تدوین شد، یک راه حل پیشنهادی برای بحران مبانی ریاضیات بود_ زمانی که مشخص شد که تلاش های اولیه برای روشن شدن مبانی ریاضیات از پارادوکس ها و ناسازگاری ها رنج می برد. به عنوان یک راه حل، هیلبرت پیشنهاد کرد که همه نظریه های موجود را با مجموعه ای محدود و کامل از اصول موضوعه پایه گذاری کند و اثبات سازگاری این اصول موضوعه ارائه دهد. هیلبرت پیشنهاد کرد که سازگاری سیستم های پیچیده تر، مانند تحلیل واقعی (real analysis)، برحسب سیستم های ساده تر قابل اثبات است. در نهایت، سازگاری تمام ریاضیات می تواند به حساب پایه (basic arithmetic) کاهش یابد.
قضایای ناتمامیت گودل
گودل نشان‌داد که دستیابی به اغلب اهداف مورد پی‌گیری در برنامهٔ هیلبرت غیرممکن است، یا حدّاقل، چنان‌چه به آشکارترین صورت خود در نظر گرفته شوند، آن‌گونه خواهد بود.
قضیه های ناتمامیت گودل که در سال 1931 منتشر شد، نشان داد كه برنامه هیلبرت برای حوزه های اصلی ریاضیات غیرقابل دستیابی است. گودل در قضیۀ اول خود نشان داد که هر سیستم سازگار با مجموعه اصول موضوعه محاسبه پذیر، که قابلیت بیان حسابی را دارند، هرگز نمی تواند کامل باشد: می توان گزاره ای ساخت و صدق آن قابل نشان دادن باشد، اما نمی توان آن را از قوانین صوری این سیستم استنتاج کرد. در قضیه دوم خود، او نشان داد که چنین سیستمی نمی تواند سازگاری خود را ثابت کند، بنابراین مطمئناً نمی توان از آن برای اثبات سازگاری هر چیز قوی تر با قطعیت (یقین) استفاده کرد. این قضایا، فرضیۀ هیلبرت، مبنی بر اینکه می توان برای اثبات سازگاری خود و به همین دلیل برای هر چیز دیگری، می توان از یک سیستم محدودکننده ای (finitistic system) استفاده کرد، را رد کرد.
به طور کلی، گودل در قضیۀ اول خود، ناتمامیت یک سیستم صوری را نشان می دهد و در قضیۀ دوم، ناسازگاربودن آن را اثبات می کند.