Теоремы Гёделя о неполноте — две теоремы математической логики о принципиальных ограничениях формальной арифметики и, как следствие, всякой достаточно сильной[1] теории первого порядка.

Первая теорема утверждает, что если формальная арифметика непротиворечива, то в ней существует невыводимая и неопровержимая формула.

Вторая теорема утверждает, что если формальная арифметика непротиворечива, то в ней невыводима некоторая формула, содержательно утверждающая непротиворечивость этой теории.

Эти теоремы были доказаны Куртом Гёделем в 1930 году (опубликованы в 1931) и имеют непосредственное отношение ко второй проблеме из знаменитого списка Гильберта.

Теорема Геделя о неполноте — одно из самых важных открытий начала 20 века. Его значение по важности (да и по своему влиянию на развитие всей последующей человеческой мысли ) соизмеримо с открытиями квантовой физики и теориями относительности. 
Если совсем вкратце, то она звучит так (одна из двух теорем — на самом деле их две) — если формальная система высказываний непротиворечива, то она не полна. Это простое, но совсем неочевидное высказывание свело на нет усилия не одного поколения математиков, которые пытались построить весь математический базис "снизу вверх"; используя конечное число аксиом, доказать все остальные математические высказывания в мире. Это достаточно заманчивая и хотя и трудоемкая, но кажущаяся реализуемой попытка — ведь нам кажется именно так рассуждает рациональный человек — беря за основу высказывания, которые он считает очевидными он строит свой "мир" "истинных" высказываний. Но оказалось что это совсем не так, на любом "этаже" аксиоматики можно сформулировать такое высказывание, которое не будет ни истинным ни ложным, либо, что звучит еще более странно — истинным но недоказуемым и для своего доказательства требует совсем других методов. Самым простым и интуитивным примером является запись высказывания на доске "высказывание. записанное на доске — ложно". Но это все эзотерические пассажи — Гедель же доказал что такое высказывание реализуемо в принципе на любой, достаточно сложной и непротеворечимой системе. В совеременной математике существует 2 основных подхода к доказательству этой теоремы, так называемая синтаксическая и семантическая версии.