Moore閉包から抽象証明系

(L, ~)がMoore閉包を持った集合として、A|-Bを B⊆A~ として定義する。 とくに、A|-{f} をA|-fと書く。つまり、A|-f ⇔ f∈A~。

これで、「B⊆AならばA|-B」と「A|-B, B|-C ならば、A|-C」を示してみる。「B⊆AならばB⊆A~」は「A⊆A~」から明らか。B⊆A, C⊆B~のとき、単調性とベキ等性から C⊆B~, B~⊆A~ となるから、C⊆A~、これは A|-C。

「B⊆AならばA|-B」で、B={f}と置けば、「f∈A ならばA|-f」が出る。「A|-B, B|-C ならば、A|-C」で、C={h}と置けば、「任意のg∈Bが A|-g であり、B|-hならば、A|-h」となる。

結局、Moore閉包は証明系の性質をうまく反映していることになる。（Moore閉包って、モナドだし。）