>>100
>ZFCだろうがZFCGだろうが本質的には自然数論と同じ
>それがPour-elとKripkeの定理の主張

　ここは中高一貫校生も来る可能性があるから 赤ペン先生しておくよ
　うーんと >>86 より
(引用開始)
Pour-elとKripkeの定理
「算術を含むどんな理論も、それら理論の文と文を対応させる原始再帰函数を通じて同型になっている」
この定理に基づけば、ZFCだろうがZFCGだろうが、そこでの証明を自然数論の証明に書き換えられる
Pour-elとKripkeの定理によれば「できる」
Deduction-preserving “recursive isomorphisms” between theories
Marian Boykan Pour-El and Saul Kripke
https://www.ams.org/journals/bull/1967-73-01/S0002-9904-1967-11689-6/home.html
(引用終り)

だった
・いま 思うと 君はGrok に聞いたのだろう？ｗ https://en.wikipedia.org/wiki/Grok_(chatbot)
・さて ZFCと ZFCG（ZFC＋到達不能基数）の差を示す例で 下記 Vitali set 関連の
　ソロヴェイモデルがある
・「ソロヴェイは証明において、到達不可能基数の存在はツェルメロ＝フランケル集合論の他の公理と整合的であり、すなわち矛盾を生じないと仮定した。この仮定は集合論者の間では広く正しいと信じているが、ZFCだけでは証明できない。[ 4 ]
　1980年、サハロン・シェラは、ソロヴェイの結果は到達不可能基数に関する彼の仮定なしには証明できないことを証明した」
　とある。百回音読しよう！

結論として 君は Pour-elとKripkeの定理を 誤解していると思う ；ｐ）

(参考)
https://en.wikipedia.org/wiki/Vitali_set
Vitali set
(google訳)
ヴィタリ集合
選択公理の役割
上に示したヴィタリ集合の構成には選択公理が用いられている。ここで疑問が生じる。ルベーグ測定可能でない集合の存在を証明するために選択公理は必要なのだろうか？答えは「はい」である。ただし、到達不可能基数は集合論における最も一般的な公理化、いわゆるZFCと整合している必要がある。
1964年、ロバート・ソロヴェイは、選択公理を用いずに、実数のすべての集合がルベーグ可測となるツェルメロ＝フランケル集合論のモデルを構築した。これはソロヴェイモデルとして知られている。[ 3 ]ソロヴェイは証明において、到達不可能基数の存在はツェルメロ＝フランケル集合論の他の公理と整合的であり、すなわち矛盾を生じないと仮定した。この仮定は集合論者の間では広く正しいと信じているが、ZFCだけでは証明できない。[ 4 ]
1980年、サハロン・シェラは、ソロヴェイの結果は到達不可能基数に関する彼の仮定なしには証明できないことを証明した。[ 4 ]
参考文献
4 ワゴン、スタン。トムコヴィッチ、グジェゴシュ (2016)。バナッハ・タルスキーのパラドックス(第 2 版)。ケンブリッジ大学出版局。296〜ページ 。