Нет. Применение исключённого третьего здесь иллюзорно, несущественно.

На самом деле док-во выглядит так: предположим от противного, что есть такое док-во; тогда оно (неформально рассуждая) будет верно также в модели ZFC H(k), но в этой модели никаких сильно недостижимых кардиналов нет, противоречие.

Неформальность тут как раз в этой части, а не там, где Вы написали (там как раз всё сразу тривиально, не надо ничего формализовывать -- именно потому, что эта часть не нужна). Чтобы сделать всё формальным, надо последовательно доказывать инвариантность всех понятий, аксиом, ординалов, кардиналов, достижимости итп. при переходе к модели типа H(k). Т.е. что быть ординалом с точки зрения модели эквивалентно быть ординалом и быть внутри модели итп. Несложно, но муторно.

Под неформальностью я имел в виду невыразимость в виде формального доказательства (правильнее было бы назвать это неформализуемостью. "Это неверно, значит, это нельзя доказать" неформализуемо, т.к. не существует формулы 1-го порядка выражающей фразу "x—верная формула". Для формального доказательства нужно доказать метатеорему "любое конечное семейство аксиом ZFC имеет well-founded модель" либо использовать теорему о полноте чтобы показать что у ZFC есть модель. В любом случае из-за теоремы о неполноте доказательство должно кроме ZFC использовать предположение "ZFC не содержит противоречия".

"Это неверно, значит, это нельзя доказать" неформализуемо, т.к. не существует формулы 1-го порядка выражающей фразу "x—верная формула".

Да, но она не существует не из-за каких-то гёделевских осложнений, а просто потому, что у теории множеств нет естественной формальной модели -- как и у теории групп, например. У неё нет естественной формальной семантики, поэтому бессмысленно, с формальной точки зрения, говорить "x - верное утверждение в теории множеств", не понимая под этим доказуемость x. Неформально, будучи платонистом, об этом можно говорить, конечно; но "помеха" формализации этого не глубока, а вполне тривиальна. Гёделевские проблемы сюда не входят.

Как только мы назначаем естественную модель (напр. N в случае теории арифметики), становится возможным говорить о формализации утверждения "x - верное утверждение" (понимая под этим -- верное в данной модели). И тут, конечно, если теория достаточно сложна, униформная формализация такого утверждения не может существовать; но тут, опять-таки, дело не в теоремах о неполноте, а в куда более простой теореме Тарского о неформализуемости истины.

В любом случае из-за теоремы о неполноте доказательство должно кроме ZFC использовать предположение "ZFC не содержит противоречия".

Это предположение в данном случае неявно всё обволакивает, не вмешиваясь в ткань аргумента (поэтому его присутствие не столь важно, как в некоторых других случаях). Грубо говоря, аргумент выглядит так: мы предполагаем, что ZFC доказывает некое утверждение, и приходим к противоречию в ZFC. Поэтому если ZFC непротиворечива, то она не доказывает данное утверждение. Тут, опять-таки, тревожить дух Гёделя совсем не надо: если ZFC противоречива, то она тривиальным образом доказывает всё, включая данное утверждение, поэтому необходимость постулирования непротиворечивости ZFC здесь следует из элементарных соображений, не из гёделевских.

Т.е. из доказываемого утверждения тривиальным образом следует непротиворечивость ZFC, и по теореме Гёделя доказательство не может быть сделано без привлечения дополнительных гипотез. (в данном случае гипотезы о непротиворечивости ZFC).

Да, но это верно не только для утверждения "ZFC не может доказать сущ. сильно недостижимых кардиналов", а и вообще для любого утверждения вида "ZFC не может доказать X". Т.е. никакой прямой нетривиальной связи между гёделевскими теоремами и рассматривамым доказательством нет, на его место может встать любое кол-во как тривиальных, так и глубоких утверждений о самых разных материях.