Я пытаюсь понять теоремы Гёделя на достаточно поверхностном уровне,рассматривая их лишь в рамках истории логики.
С точки зрения истории, Гёдель доказал неполноту непротиворечивой теории, язык которой позволяет формулировать утверждения о разложимости натуральных чисел на простые сомножители. Как сказал
Xaositect, такова арифметика Робинсона (теория со сложением и умножением натуральных чисел, но без полноценной индукции), а тем более - арифметика Пеано (теория со сложением и умножением натуральных чисел и индукцией). Контр-примером является арифметика Пресбургера (теория со сложением натуральных чисел, но без умножения), она полна, т.е. доказывает или опровергает любое высказывание в своём языке.
Суть доказательства Гёделя в том, что он строит некоторое утверждение в языке арифметики, которое в силу способа его построения равносильно утверждению о недоказуемости этого же утверждения в рассматриваемой теории. На самом деле это просто утверждение о несуществовании натурального числа, удовлетворяющего неким условиям. Это утверждение не может быть ложным, поскольку это означало бы его доказуемость в рассматриваемой теории, т.е. получилось бы, что непротиворечивая теория доказывает ложное утверждение. Значит оно является истинным, т.е. такого натурального числа не существует, хотя рассматриваемая теория не может этого доказать.
Значение теоремы Гёделя о неполноте в том, что она не только про арифметику, а про
любую теорию, содержащую достаточно богатую арифметику. Например, она исключает надежды физиков на построение "теории всего": Если такая теория умеет оперировать натуральными числами, то в ней можно сформулировать истинное утверждение о несуществовании натурального числа, которое теория не сможет доказать.
Современные доказательства теоремы Гёделя о неполноте строятся несколько иначе, они опираются на понятие алгоритмической вычислимости. Об этом сказал
Anton_Peplov. Но суть та же.