>>434
>でもIUTについては、4年くらい前なんか、分類空間がどうのBGがどうの専門的な数学で盛り上がってた記憶がある

ありがとう。BGは下記のベルナイス＝ゲーデル集合論のことかな？（下記）

望月氏が、当初は IUT VIで”「ZFCG」(ZFCにG つまり グロタンディーク宇宙の公理を加えた）が 保存拡大”と書いていて
”保存拡大ではない”という議論から、”ZFCは 公理図式で ZFCの公理の数は無限個”（下記）で
BG(ベルナイス＝ゲーデル集合論)が"有限公理化できる"（下記）
みたいな議論だったと思う

しかし、それは IUTの外の議論だし
”「ZFCG」(ZFCにG つまり グロタンディーク宇宙の公理を加えた）が 保存拡大”の記述も修正されたよ

(参考)
https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A9%E3%83%B3%E3%83%BB%E3%83%8E%E3%82%A4%E3%83%9E%E3%83%B3%EF%BC%9D%E3%83%99%E3%83%AB%E3%83%8A%E3%82%A4%E3%82%B9%EF%BC%9D%E3%82%B2%E3%83%BC%E3%83%87%E3%83%AB%E9%9B%86%E5%90%88%E8%AB%96
フォン・ノイマン＝ベルナイス＝ゲーデル集合論
数学基礎論において、フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG) とはツェルメロ＝フレンケル集合論＋選択公理 (ZFC)の保存拡大である公理的集合論である。
NBGのキーとなる定理はクラスの存在定理である。クラスの存在定理は、量化子の範囲を集合に限定した論理式それぞれに対して、論理式を満たす集合からなるクラスの存在を述べる。クラスは、クラスの論理式を一つずつ構築することで構成される。すべての集合論的な論理式は2種類の原子論理式（所属関係と等式）と有限個の論理記号から構築されるため、論理式を満足するクラスを構築するには有限個の公理があればよい。NBGが有限公理化できるのは、こうした理由による。

https://mathlog.info/articles/1314
Mathlog
めいぜんおーえす
大学数学基礎
ZFCの公理一覧と誤解しやすいポイント 2020年12月19日
公理図式
ZFCの公理の数は無限個
分出公理図式と置換公理図式は条件を満たす論理式
ごとに一つの公理があって、それを全部集めたものです。
なのでZFCの公理の数は無限個になります。

https://ja.wikipedia.org/wiki/%E3%83%84%E3%82%A7%E3%83%AB%E3%83%A1%E3%83%AD%EF%BC%9D%E3%83%95%E3%83%AC%E3%83%B3%E3%82%B1%E3%83%AB%E9%9B%86%E5%90%88%E8%AB%96
ツェルメロ＝フレンケル集合論
ツェルメロ＝フレンケル集合論（英: Zermelo-Fraenkel set theory）とは、ラッセルのパラドックスなどのパラドックスのない集合論を定式化するために20世紀初頭に提案された公理系である。名前は数学者のツェルメロとフレンケルにちなむ。歴史的に議論を呼んだ選択公理 (AC) を含むツェルメロ＝フレンケル集合論は公理的集合論の標準形式であり、今日では最も一般的な数学の基礎となっている。選択公理を含むツェルメロ＝フレンケル集合論はZFCと略される。