>>294
＞現代数学の基礎論の手続きの中に「議論してるモデルを切り替える宣言」などない。

そもそも証明の手続きの中に「モデル」が出てこない
竹内の本でモデルという言葉すら出てこないのは当然
証明のカット除去の話だから

＞証明中で「真か、偽か」という論述を行うことは許されていて、
＞それは議論してるモデル内部での真偽値を意味している

実は許されていない
いわゆる数学書の中の「Aが真である」、「Aが偽である」は、全部除去できる
具体的には「Aである」「¬Aである」と言い換えられる
したがってモデルとか真偽値とかは全く必要ない

＞それの真偽値判定を切り替える文法など存在しない、
＞モデルは議論の最初から最後まで固定される。

一方で、例えば群について考えるなら、それは群論における１つのモデルだと考えられる
集合論の中で、無数の群を構成することができる　つまり群論のモデルは無数に存在する

群が可換か否か？　群の位数が有限か否か？　等の命題は
当然ながらモデルとなるそれぞれの群に依存する

したがって、
群論は実は群の公理系の理論ではなく群の圏に関する理論であり
位相空間論は位相空間の公理系の理論ではなく位相空間の圏に関する理論であり
多様体論は多様体の公理系の理論ではなく多様体の圏に関する理論である

そういう意味では既に「モデルを切り替える」なんてことは
現代数学では日常的におこなわれているので
とりたてて新しさを強調するようなことではない

IUTでの宇宙の取り換えは、それとは別のことだろうとは思うが
何がいいたいのか、当人以外（実は当人にも）分かってないので
ここでは論じない