تز صوری گرا این است که ریاضیات با دستگاه های نمادی صوری سر و کار دارد. در واقع ریاضیات مجموعه ای از آن مباحث مجرد تلقی می شود که در آن اصطلاحات صرفا نمادهایی هستند و احکام قواعدی متضمن این نمادها. پایه غائی ریاضیات در منطق قرار ندارد و بلکه تنها در مجموعه ای نشانه ها و نمادهای پیش منطقی و در مجموعه ای از اعمال با این نشانه ها واقع است. چون از این دیدگاه، ریاضیات عاری از محتوای ملموس و تنها شامل عناصر نمادی آرمانی است، برقراری سازگاری شاخه های مختلف ریاضیات قسمت مهم و لازمی از برنامه صوری گرایی می شود. بدون همراهی چنین برهان سازگاری، تمام مبحث اساس بی معنی خواهد شد. در تز صوری گرایی اصل موضوعی ریاضیات در بیشترین حد دنبال می شود.
مکتب صوری گرایی توسط داوید هیلبرت بعد از اتمام کارش در بررسی اصل موضوعی هندسه تاسیس شد. در مبانی هندسه اش 1899 هیلبرت روش ریاضی را از قالب مبحث اصل موضوعیهای مادی اقلیدس به قالب دقیق تر مبحث اصل موضوعیهای صوری کنونی در آورده بود. دیدگاه صوری گرا بعدا برای مقابله با بحران ناشی از پارادوکسهای نظریه مجموعه ها و به مبارزه طلبیدن ریاضیات کلاسیک به دلیل انتقادهای شهودگرایانه، به وسیله هیلبرت ایجاد شد. گرچه هیلبرت پیش از سال 1904 اصطلاحات صوری گرایانه را به کار برده بود تا بعد از سال 1920 وی و همکارانش برنیس، آکرمان، فون نویمان، و دیگران کار جدی را درباره آنچه امروزه برنامه صوری گرا نامیده می شود آغاز نکردند.
توفیق یا شکست برنامه هیلبرت برای نجات ریاضیات کلاسیک در گرو حل مسئله سازگاری است. بری بودن از تناقض تنها به کمک برهان های ناسازگاری تضمین می شود و برهان های ناسازگاری قدیمی تر مبتنی بر تعابیر و مدل هایی است که مسئله سازگاری را از یک حوزه ریاضیات به حوزه دیگر منتقل می کند. به عبارت دیگر یک برهان سازگاری به روش مدلها صرفا برهانی نسبی است. بدین جهت هیلبرت روش مستقیم جدیدی برای مسئله سازگاری تدبیر کرد. بسیار شبیه به اثبات انچه وضعیت هایی خاص در یک بازی بنابر قواعد آن نمی توانند در بازی پیش آیند هیلبرت امید آن را داشت تا به کمک مجموعه مناسبی ار قواعد عمل برای به دست آوردن فرمول های قابل قبول از نمادهای اساسی ثابت کند که فرمول متناقضی هرگز پیش نمی آید. با نمادهای منطقی یک فرمول متناقض فرمولی که از نوع " F و نه F " است که در آن F فرمول پذیرفته شده ای از دستگاه است. اگر بتوان نشان داد که چنین فرمول متناقضی ممکن نیست آنگاه سازگاری دستگاه ثابت شده است.
بسط افکار فوق برای آزمون مستقیم سازگاری دری ریاضیات توسط هیلبرت، نظریه برهان نامیده شد. برای دستگاه های مقدماتی معینی براهین سازگاری فراهم شدند که آنچه را هیلبرت میل به انجام آن برای همه ریاضیات کلاسیک داشت نشان می دهد ولی در کل مسئله ناسازگاری برای دستگاه بدون چاره ماند.
در حقیقت برنامه هیلبرت حداقل به شکلی که در اصل در ذهن او بود ظاهرا محکوم به شکست بود این حقیقت توسط کورت گودل در سال 1931 عملا قبل از انتشار مبانی ریاضی، آشکار شد. گودل به کمک روش های بی ایراد و قابل قبول برای پیروان هر یک از سه مکتب اصلی فلسفه ریاضیات نشان داد که برای دستگاه قیاسی که به حد کافی صوری شده باشد نظیر دستگاه هیلبرت برای همه ریاضیات کلاسیک اثبات سازگاری دستگاه به کمک روش های متعلق به خود آن دستگاه میسر نیست. این قضیه قابل توجه پیامد قضیه اساسی تری داشت گول ناکامل بودن دستگاه هیلبرت را ثابت کرد یعنی وی وجود مسائل "تصمیم ناپذیر" را در داخل دستگاه که سازگاری دستگاه از آن جمله است نشان داد. این قضایا نشان می دهند که دستگاه های ریاضی که برای استخراج ریاضیات مناسب شناخته شده اند قابل اطمینان نیستند بدین معنی که سازگاری آنها را نمیتوان با روش های متناهی داخل دستگاه صوری شده اند ثابت کرد و حال آنکه هر دستگاهی که از این لحاظ مطمئن تشخیص داده شده نامناسب است.