続・到達不能基数ちゃんについて

前回の記事で、いい加減なことを書いてしまいました.
ごめんなさい.
自分に対する戒めも込めて今回の記事を書きます.
また何か間違ったことを書いてしまっていたら, ご指摘いただけると助かります.

定理
(i) 到達不能基数の存在は ZFC から証明できない.
(ii) さらに, 到達不能基数の存在が ZFC と相対的に無矛盾であることを ZFC で証明できない.

証明
簡単のため, 到達不能基数が存在することを意味する命題を I とおきます.
(i)
ZFC+I |- Con(ZFC)
なのです(詳細は省略).
したがって
ZFC |- I → Con(ZFC)
となります.
よって,
ZFC |- I
と仮定すると
ZFC |- Con(ZFC)
となり, これはゲーデルの第二不完全性定理に反します.
以上により,
ZFC |- I
ではない, すなわち, ZFC から到達不能基数の存在が証明できないことが言えます.
(ii)
ZFC |- Con(ZFC) → Con(ZFC+I)
と仮定すると
ZFC+I |- Con(ZFC) → Con(ZFC+I)
です.
さらに
ZFC+I |- Con(ZFC)
であることから
ZFC+I |- Con(ZFC+I)
となり, これもゲーデルの第二不完全性定理に反します.
以上により,
ZFC |- Con(ZFC) → Con(ZFC+I)
ではない, すなわち, ZFC からは到達不能基数の存在の相対的無矛盾性が証明不可能, ということになります.

さて,
ZFC |- Con(ZFC) → Con(ZFC+I)
ではないことを証明してみましたが,
Con(ZFC) → Con(ZFC+I)
は, 到達不能基数の存在の相対的無矛盾性を表していると考えられるので, 言い換えると, 到達不能基数の非存在を証明不可能であることを表している, とも言えます.
そのことが ZFC において証明不可能であることを, 上で証明しました.
このことをもって
(ZFC において)到達不能基数の非存在を証明不可能であることが(ZFC において)証明不可能であることを(メタ数学的に)証明した.
と言えます.
ややこしいですなー.
と, ここまで書いてきましたが, 実は, ここまでの論証の理屈が, 自分にはどうにもよく分からないのです.
例えば, Jech本167ページには, κが到達不能基数ならば V_κ が ZFC のモデルだと書かれているのですが, これがメタ数学的な定理なのか, ZFC 内部での定理なのか分かりません.
メタ数学的な定理だとすると, ZFC で定義されるところの到達不能基数の概念が使われているので, ZFC 内部での定理のような気がします.
しかし, そうなるためには ZFC においてモデルの概念を形式化しないといけないのでは？？？
形式化した上で
ZFC+I |- Con(ZFC)
という結論が得られたのでしょうか.
それから,
ZFC |- Con(ZFC) → Con(ZFC+I)
とはなり得ない件ですが, 何らかのメタ数学的な方法によって, ZFC が無矛盾であれば ZFC+I も無矛盾であるということを証明できる可能性はないのでしょうか.
もし証明できるとすると, I は ZFC から独立な命題であると結論付けることができるような気がします.
強制法を理解しようとしたときもそうだったのですが, 色々な定理がどこを土台にしたものであるのかが, 読んでいてよく分からないのです.
「ZFC における」という言い回しも, ZFC で形式化された文について考えているのか, ZFC の公理を使ってメタ数学的に考えているのかが不明瞭だと感じられることが多いのです.
例えば, コンパクト性定理はメタ数学的な定理ですが, その証明には選択公理が使われています.
これは後者に属します. 多分.
V_κ が ZFC のモデルだというのは, 前者なのか後者なのか.
考えているうちに頭がどんどんこんがらがってきます.
そもそも, 自分が何か重大な勘違いをしているのかもしれませんが.