Теорема Гёделя о неполноте

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

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