>>600
その条件は厳し過ぎて
「クラスAの論理式φ、の形式的証明が存在するなら、φのクラスBの形式的証明が存在する」
という定理が得られたとしても、論理式のクラスの方も限定され過ぎて、定理としては役に立たないのではありませんか？なんとなくですけど。