[логика](Не)противоречивость арифметики

[LaTeXScience]

Хочу разобраться с одним вопросом (который не входит в стандартные учебные курсы по математике). Вот есть две теоремы Геделя о неполноте. И в то же время есть какие-то работы Герхарда Генцена, которые доказывают непротиворечивость арифметики и тем самым завершают программу Гильберта по формализации арифметики. Объясните, пожалуйста, как так может быть, ведь кто-то из них, Гедель или Генцен, должен быть не прав, или я что-то неправильно понимаю?

[Xaositect]

Доказательство Генцена использует средства, выходящие за пределы арифметики. Трансфинитную индукцию, наверное, или что-нибудь такого уровня.

[LaTeXScience]

Xaositect
Так что, получается, что ответ на вторую проблему Гильберта зависит от используемой метатеории? В чем ее вообще тогда смысл?
И почему все кругом говорят, что Гильберт ошибался, теоремы Геделя видите ли подрывают идеи формализма и все такое? Как тогда понимать это (Гильберт Д., Бернайс П._Логические исчисления и формализация):

[epros]

Xaositect в сообщении #464284 писал(а):

Трансфинитную индукцию, наверное, или что-нибудь такого уровня.

Трансфинитную индукцию до ординала $\varepsilon_0$. В арифметике первого порядка она нереализуема.