"yields falsehood when preceded by its quotation" yields falsehood when preceded by its quotation
Время - первая треть 20 века. Уже вполне оформилось и общепринято представление, что есть продукт деятельности математиков: строго доказанные утверждения. А строго доказанные - значит, полученные из общепринято верных утверждений ("аксиом") с помощью небольшого набора правил вывода. Конечно, в реальности никто (кроме отдельных попыток Пеано и Рассела) в формальном виде доказательство не выписывает, пользуются обычным языком. Но в принципе это возможно, и формально записанное доказательство из небольшого обозримого набора аксиом - вполне строго определенный объект, из числа как раз таких, которые изучает математика.

Большой соблазн: изучить такие объекты, и сразу узнать, что может быть доказано в математике, а что не может. Например, очень охота доказать, что никакое противоречие доказано быть не может: что наши аксиомы и правила вывода дают непротиворечивую систему. А в идеале - что любое верное утверждение может быть доказано.
Вот эти две надежды Гедель и рассеял, причем в самом безобидном месте, в арифметике натуральных чисел.

Понятно, что любое утверждение (цепочка символов из заданного заранее алфавита) можно закодировать натуральным числом. И любое доказательство (цепочка утверждений, т.е. опять же цепочка символов). Причем это можно сделать так, что свойства вроде "утверждение Х грамматически правильно построено", "цепочка Ц есть доказательство утверждения У" итп. - можно представить в виде не слишком сложных арифметических формул от кодов Х,Ц,У. Гедель это сделал длинно и аккуратно; нам, привычным к программированию, достаточно понять, что это очевидно так, и никаких подводных камней здесь быть не может.

Например, можем написать формулу от трех натуральных переменных Ф(У, х, Д), которая означает: У есть код утверждения от одной переменной, а Д есть код доказательства для У(х) (если это так, то она выдает истину, а если что-то не так, то ложь).
А теперь внимательно, начинается хитрый трюк!
Сделаем формулу от одной переменной Щ(х)=(не существует Д): Ф(х,х,Д). Она означает: если в формулу от одной переменной с кодом х подставить ее собственный код, то у того, что получится, не существует доказательства. Например, если у формулы (а=5) оказался код 10000, то Щ(10000) верно (а то бы мы нашли доказательство, что 10000=5).
И второй кувырок: у формулы Щ есть код, пусть Х. Построим утверждение Щ(Х).
Оно означает, если немного подумать, что у Щ(Х) нет доказательства. Если бы оно было ложным, то это бы значило, что у Щ(Х) есть доказательство - а это полный бардак; доказательство ложного утверждения. Значит, оно истиннно - но тогда, значит, у него нет доказательства.

(Те, кому довелось писать программу, печатающую собственный текст, этот кувырок узнали. А кому не довелось, могут узнать его в английской фразе: "yields an unprovable statement when preceded by its quotation" yields an unprovable statement when preceded by its quotation.)

Вторая теорема Геделя - что не надо париться, строя это Щ(Х). Достаточно взять утверждение, что арифметика непротиворечива. Уже оно не имеет доказательства. В предыдущих терминах можно, например, взять то же самое Щ(10000). Она получается как следствие первой.

Вот что доказал Гедель. А как на это накинулись философы, а также как с тех пор все усложнилось в самой математике, вы, может быть, узнаете в другой раз.

UPD Впрочем, не обязательно ждать другого раза. Можно и прямо сейчас порыться вот здесь или здесь.