Теорема Гёделя о невозможности полной формализации заключается в следующем: для достаточно выразительно «богатых» формальных систем (языков) невозможно задать дедуктику (формализованную систему доказательств), которая одновременно обладала бы свойствами полноты (то есть доказывала бы все содержательно истинные утверждения, которые можно сформулировать с помощью данного языка) и непротиворечивости (то есть не доказывала бы некоторое суждение вместе с его отрицанием). 3

Иными словами, теорема Гёделя утверждает, что в таких формальных языках непременно найдутся истинные, но недоказуемые утверждения. 3 Это означает, что множество «содержательных» истин всегда превосходит по объёму множество истин, доказуемых с помощью любой сколь угодно сложной формализованной системы доказательств. 3

Этот результат показал неосуществимость программы формализации математики, ранее выдвинутой Давидом Гильбертом. 4