>>164
自然数は０項演算０と１項演算後者で自由生成される構造。
証明全体や記号列全体はもっと多くの演算で自由生成される。
どうして後者を走る量化はよくて
前者を走る量化を胡散臭いとみなすのか理解できないよね。