ところで、 標準的な可証性述語もロッサーの可証性述語も 扱ってる関係は ＞P が論理式 A の T での証明図 であるのに、 それを表現するとされる論理式は、 標準的な可証性述語 ∃ｙProv(y,x） ロッサーの可証性述語 ∃ｙ（Prov(y,x）∧∀ｚ＜ｙ¬Disp(y,ｚ）） で異なってるわけで、
これは、ただ単に、必要な条件を無矛盾である、にするための工夫ということですか
はじめ、標準的な可証性述語の∃ｙProv(y,x）だけ、見てたときには、扱う関係のメタ的な情報を表したものなのかな、くらいに思ってましたが、 ロッサーの可証性述語の∃ｙ（Prov(y,x）∧∀ｚ＜ｙ¬Disp(y,ｚ））の場合は、扱ってる関係（P が論理式 A の T での証明図）とは、あんまり（全部は）関係ありませんよね
