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