形式的証明＝数学の証明か？という問題を考える上で意味のある、形式的証明の複雑さの基準はないのだろうか。
しかも「クラスAの論理式φ、の形式的証明が存在するなら、φのクラスBの形式的証明が存在する」が成り立つような。