Unspecifying modal operator in modal axioms

[SnO2WMaN]

認識論理のように複数（可算無限個）の様相演算子を持つ体系や証明可能性述語などのことを考えると、特定のboxおよびdiaではなく、System上の1項様相演算子が公理Kや公理4の性質を満たす、と定義したほうが汎用的な気がする。

例えば認識論理では[∀ i, Axiom.K (boxes i)]のようにしたり、現在のDerivabilityConditionで行われているD1,D2,D3上の実質的な様相論理の計算を使いまわせたりする気がする。