証明系付きインスティチューション

証明系を抽象化する目的は、証明系をインスティチューションに組み込みたいから。

Moore閉包を使う定式化もいいのだけど、集合に対する関係|-を基本とすることにする。A|-Bのインフォーマルな意味は、「Aの論理式を全部仮定すれば、Bのどの論理式でも証明できる」。その性質は：

1. A⊆B、A|-C ならば、B|-C （水増し法則）
2. A|-B, B|-C ならば、A|-C （推移性）

インスティチューション(Sign, Sen, Mod, |=)に関して、Senの定義を変更して、σ:Σ→Γ in Signに対して、Sen(σ):Sen(Σ)→Sen(Γ)は単なる写像ではなくて、f:Pow(Sen(Σ))→Pow(Sen(Γ))であって、次を満たすとする。

1. A⊆B ならば、f(A)⊆f(B) （単調）
2. f(∪A_i) = ∪f(A_i) （∪の保存）

2番目（∪の保存）はどちらかというと技術的な要請である。

充当関係 |= も、モデルMと文の集合Aに対して M|=A と定義される。インフォーマルには、「Aのどの文も、Mに対して妥当」ということ。

この状況で、Pow(Sen(Σ))に2項関係|-があって、次の性質を持つとする。

1. σ^*N |= A ⇔ N |= σ_*A （充当関係）
2. A|-B ならば、σ_*A|-σ_*B （証明関係の保存）
3. M|=A, A|-B ならば、 M|=B （健全性）

A⊆Sen(Σ)が閉じていることは、「A|-B ⇒ B⊆A」で定義できる。

で結局、証明系付きインスティチューションは(Sign, Mod, Sen, |=, |-)で、いま述べたような性質を持つものとして定義する。

これから簡単に、証明の借用（borrowing）ができることを示せる。

• σ^*N |= A, A|-B ⇒ N |= σ_*B
• N |= σ_*A, σ_*A|-σ_*B ⇒ σ^*N |= B