>>63
> 一階述語論理に基づいたZFCがLeanライブラリにないのでうまく証明が構成できないということは1年前から言ってる

>>77
>species/mutationの理論において本質的な役割を果たす「不定元のような論理式」（＝特定されていない、「とある論理式Φ」のようなもの）を扱うには、一階述語理論としてのZFCが必要であり

論理式が特定されてないなら必要なのは二階なのでは？
二階述語論理も必ずあると思いますが
ゲーデルの第二不完全性定理で必要なので
違うの？

ちなみに人間が扱うときは面倒なんで
公理の数を無限個にして一階のままやるパターンがあります
全ての論理式ごとに公理を無限個付け加えれば二階にする必要はないので
こういう無限個の公理を扱うプログラムがCoqやLeanにあるのかどうかは知りません