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