べつに俺が指摘する以前にもうとっくにネットでもなんでも指摘されてる。望月論文の推論測?言語体系?では通常の数学の推論では起こりえないことが発生している。べつに標準的な論理体系や言語体系を使いたくないなら好きなもの使えばいいが、しかしそれならそれでどんな言語を用いるのか、どんな推論を用いるのか、最低限をそれを明示しないといけない。もちろんそれでおわりではない。それがほんとに標準の数学の保存拡大になってるかの検証をしてそのうえで使うなら好きにすればいい。しかしそもそもそんなレベルの話ですらなくそもそも

IUtとはどんな言語どんな推論をつかうかの明示的な規定すらない

その状態からスタートしてる。論文で私的城も何も書いてないものは書いてないんだから議論のはじめようすらない。加藤先生もNスぺでなんか言ってたけどそのあとそれ実行したって話ある?ないやろ?もう無理なんだよ。