形式化の話

数学の形式化について - yoriyukiの日記

ただこれは集合論の言語がダメである、という証左と考えることもできるわけです。確かLawvereはそういう意見だったと思います。(初等埋め込みではなく、圏論に関してですが)

そういう考え方はできると思いますが、私が述べたかったのは数学者が現在どう数学をやっているかという次元の問題なので。
それと、truthのundefinabilityっていう大きいハードルがあるので、いずれにしても何かしらを捨てざるを得ないのではないかと思うのですが。その範囲内では、集合論のやり方は比較的直感的かと思います。もちろん、長年その世界に浸っているために感覚がねじれている危険はありますが。