初等埋め込みのこと

そういえば、定義可能なクラス関数が初等埋め込みであるというのはZFCの論理式では書けないんですよね。正確に言えば、集合論の言語では。にもかかわらず、集合論の議論では初等埋め込みがめちゃくちゃ頻繁に使われるというのは、数学が形式的に行われているという命題への反証になっているのではないかなと思うわけで。
もちろんより初等的な反例もたくさんあるとは思いますが。

形式主義というのはむしろ、形式的に書きなおせるよということを担保に、開墾をしていくときには直感的なアイデアをふんだんに使うということなのではないかなと。少なくとも現実的には。

集合論における似た感じの例としては無限ゲームが考えられるかと思うのですが、これの話はもう少しちゃんとやりたいのでまた後で。