>>255
Finite order arithmetic (Takeuti, 1987, Part II)
>>257
References
Takeuti, G. (1987). Proof Theory. Elsevier Science Ltd, 2nd edition.

竹内 外史先生だね
https://ja.wikipedia.org/wiki/%E7%AB%B9%E5%86%85%E5%A4%96%E5%8F%B2
竹内 外史（たけうち がいし、1926年1月25日 - 2017年5月10日）
https://en.wikipedia.org/wiki/Gaisi_Takeuti
Gaisi Takeuti (竹内 外史, Takeuchi, Gaishi; January 25, 1926 – May 10, 2017[1]) was a Japanese mathematician, known for his work in proof theory.[2]
Notes
2 Takeuti 2013.
・Takeuti, Gaisi (2013) [1975]. Proof theory (Second ed.). Mineola, New York: Dover Publications. ISBN 978-0-486-49073-1.

なお>>257より
(google訳)
7. PAにおけるフェルマーの最終定理の証明？
私たちは任意のサイトに対してSGA全体を構築しましたが、数論における個々の証明は、算術に近いサイトの低次コホモロジーしか使用していません。
詳細な評価によって、第3.8.4節のように、既存の証明を比較的低いnに対するn階算術に持ち込むことができるかもしれません。これは、マッキンタイア（2011）がフェルマーの最終定理に対して始めたような、困難な論理分析を行うのに適した文脈となるでしょう。
さらに研究を進めることで、PAの保存的拡大（竹内、1978）の範囲内で構成を限定し、フェルマーの最終定理の既存の証明が本質的にPA内で機能することを示すことができるかもしれません。
これは、フリードマン（2010）で予想されているように、証明を指数関数算術（EFA）にさらに還元するのに役立つ可能性があります。
このような評価は困難である可能性が高いです。
これは、真剣な算術を回避するための論理的な抜け道ではありません。
論理への関心に動機づけられているわけではありませんが、キシン（2009b）は（ワイルズ、1995）を拡張および簡略化し、一般的に可換代数よりも幾何学の使用を少なくすることで、集合論への要求を明らかに軽減しています。また、キシン（2009a）は、カーレとヴィンテンベルガーによって発展させられたセールによる戦略を用いて、フェルマーの最終定理の別の証明を完成させています。
(引用終り)

なので、Colin McLarty 先生も 2014版では 「7. PAにおけるフェルマーの最終定理の証明？」で ？マーク付きだｗ （＾＾
2020版でも 同じかな　；ｐ）