>>75
>数セミ
>”フェルマーの最終定理はZFCの下で証明できるか？
>／ グロタンディーク宇宙と到達不可能基数 池上大祐”
>この結論は、分らないと書かれていた

上記の問は
「ZFCGでの証明をZFCでの証明に書き換えられるか」
ということかと

>さて、
>「ZFCから ”無限公理を抜いた”公理系の下で証明できるか？」
>についても 考えてみよう

これまた
「ZFCでの証明を自然数論での証明に書き換えられるか」
ということかと

>そうすると、無限集合が作れないから
>可算の自然数の集合Nが存在しない
>整数環Z、有理数体Q 、実数R、複素数Cも
>同様に存在しない
>そうすると n = 3：
>オイラー 1の原始3乗根 ζ3=(−1±√−3）
>クンマーの理想数
>これら 全部 ”ZFCから 無限公理を抜いた公理系の下”では アウト！

・・・とは言い切れない

Pour-elとKripkeの定理
「算術を含むどんな理論も、それら理論の文と文を対応させる原始再帰函数を通じて同型になっている」

この定理に基づけば、ZFCだろうがZFCGだろうが、そこでの証明を自然数論の証明に書き換えられる

>これ どうすんの？
>無限公理を抜いた公理系で
>”フェルマーの最終定理はZFCの下で証明できるか？”
>の解答は、できないと思うが

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

ちなみにMarianは女性で旧姓がBoykan、Pour-elは夫の姓（夫はイスラエル人）
BoykanはBoykinの訛りで、スラブ系の苗字（おそらく先祖はウクライナ系　当人はNY生まれ）

>その証明は 相当難しいだろうが、

Pour-elとKripkeの定理の証明は読んでない
めんどくさそうだがやればできるんだろう

>無限公理ありのZFCの方が よほど 高等数学向きで 適切だよ
証明の短縮という意味では有用だが
それは”無限回操作”の魔法を使っているからではない
だって算術の証明に書き換えられるから