>>168
>なんか、当初はIUT4の基礎論のパートは主要定理とは無関係のおまけって話だった気がするんだが。
>別にこれなしでも大丈夫という。
>いつの間にか一番重要なポイントと言い出しているのが気になる。

かなり同意見です
望月さん かなり基礎論おんちですね
例えば
１）まず、プログラミング言語で 予約語というのがあります（下記）
　同様に 数学ではすでに他者が使い出して 広く普及している言葉を
　別の意味で使うときは 注意しないとまずこと（誤解や混乱の原因）になる
　例：宇宙、種 （これ 殆ど予約語ですね）
２）用語 宇宙が混乱を起こしていることは有名ですが
　種も Combinatorial speciesというのがあって、André Joyalが研究していたという（下記）
　以前に これ(Joyal)だと思ったが、どうも違うのではと思いましたね
　いまブログ読むと やっぱりという気がする
３）さらに”「不定元のような論理式」（＝特定されていない、「とある論理式Φ」のようなもの）を扱うには、一階述語理論としてのZFCが必要であり、それはMathLib上ではまだ掲載されていないということが判明しました。”
　”日本のある若手研究者は一階述語理論としてのZFCの形式化を既に実行しており、それはMathLib上では（MathLibの運営委員会による査読を経ていないため）掲載されていませんが、日本の若手研究者の（大きな仕事ではなく）ちょっとした補足的な仕事としてその形式化が既に実行されている”
　辺りを読むと 用語”一階述語理論”から誤解されているような・・
　”一階述語理論としてのZFCが必要であり”と なると 私の頭では 解釈不能です・・

ここら”一階述語理論としてのZFC”とは？ から 望月先生が理解しないと
普通の数学者とは 会話できない気がします

　>>78より再録
https://plaza.rakuten.co.jp/shinichi0329/diary/202601010001/
2026.01.01
Leanによる形式化は、長期的な検証や説明責任を可能にする記録装置となり得るか？
カテゴリ：研究関連の現状報告

https://ja.wikipedia.org/wiki/%E4%BA%88%E7%B4%84%E8%AA%9E
予約語（よやくご、（英: reserved word）とは、プログラミング言語などの人工言語の仕様に定められているもので、ユーザープログラムの開発者が自分で付ける識別名としては利用できない特定の文字列のこと

https://en.wikipedia.org/wiki/Combinatorial_species
Combinatorial species
The theory was introduced, carefully elaborated and applied by Canadian researchers around André Joyal.
The category of species is equivalent to the category of symmetric sequences in finite sets.[1]