抽象証明系

証明可能性関係 |- を外から見て公理化したい。とりあえず：

1. f∈A ならば、 A|-f
2. 任意のg∈Bが A|-g であり、B|-hならば、A|-h

この2つは必要だろう。A、Bともに論理式（その全体はL）の集合のとき、A|-Bを、「任意のg∈Bに対してA|-g」として、|-の定義を拡張しておく。

1. A|-A
2. A|-B, B|-C ならば、A|-C

はいえる。最初の定義の言い換えに過ぎない。関係|-はプレ順序になる。これから同値関係を定義して、順序にできる。

集合Aに対して、A~ = {f∈L | A|- f}として演算子~を定義する。

1. A⊆B ならば、A~⊆B~ （単調性）
2. A⊆A~ （増大性；isotonic）
3. A~~ = A~ （ベキ等性）

最初は、次のほぼ自明な補題と同じ。

• A⊆B、A|-f ならば、B|-f

A⊆Bと「f∈AならばA|-f」から、B|-Aが出る。B|-A, A|-fからB|-f。

2番目は、「f∈AならばA|-f」の言い換え。

3番目； A⊆A~と単調性からA~⊆A~~は言えるから、A~~⊆A~が問題。つまり、「A~|- fならばA|-f」のことだが、A|-A~ は定義から出るから、A~|-fと組み合わせて、A|-f。

これら3つの性質を持つ演算子はMoore閉包というそうだ。

一般化して、論理式（と呼ばれる何か）の集合LとPow(L)上のMoore閉包の組を証明系として定義してよいだろう。