演繹付きインスティチューション

演繹付きインスティチューション〈institution with deduction〉を定義する。

普通のインスティチューションに、指標Σごとの演繹性判断〈deducibility judgement〉|-_Σが付いている。

• |-_Σは、Pow(Sen[Σ])とSen[Σ]のあいだの（二項）関係

演繹性判断は、次の公理を満たす。

1. {a} |- a 反射性
2. A |- a, A⊆B ならば B |- a 単調性
3. A_i |- a_i ならば、∪({a_i}|i∈I) |- b ならば、∪(A_i|i∈I) |- b 推移性

A⊆Sen[Σ]に対して、モデルMod[Σ]の部分圏 (Mod[Σ] s.t. A) を次のように定義する。

• すべてのa∈Aに対して X |= a であるような対象Xの全体を |Mod[Σ] s.t. A| として、この対象類から誘導される充満部分圏を(Mod[Σ] s.t. A)とする。

帰結性判断〈consequence judgement〉 A |⇒ a を次にように定義する。

• (A |⇒ a) iff (すべての X∈|Mod[Σ] s.t. A| に対して、X |= a)

演繹付きインスティチューションにおいて、|-_Σ が健全であることは、次のように定義される。

• A |- a ならば、A |⇒ a

インスティチューションにもともと付いていある充足性判断〈satisfaction judgement〉、充足性判断から導かれる帰結性判断、それとは独立な演繹性判断の3つの判断のあいだの関係を考える。

健全性以外に問題となる性質は、

• 適切性〈adequacy〉
• 完全性（健全かつ適切）
• コンパクト性

コンパクト性は次の意味

• A |- a ならば、Aの有限部分集合A'があり、A' |- a

より強い有限性は、

• A |- a ならば、Aは有限集合

演繹付きインスティチューションとハイパードクトリンを組み合わせると、構文論と意味論の両方を扱えそうだ。ハイパードクトリンを指標の上に展開するのが最初の作業かな。