$`\newcommand{\Within}{\sqsubseteq}
\newcommand{\conc}{\mathop{\#} }
\newcommand{\dmid}{\mathrel{\|} }
\newcommand{\mrm}[1]{\mathrm{#1} }
%`$
- 証明の定式化が欠けている。→ πインスティチューション
- 非論理的指標部分と論理条件が分離されている。一様に扱いたい。
- 関手意味論をうまく表現できない。→ 関手意味論フレームワーク
論理文に関しては、次のアプローチを取る。
- 論理条件＝論理文の集合 の代わりに指標フラグメントを考える。あるいは、指標フラグメントを条件部／法則部と呼ぶ。
- $`M \models_\Sigma \Phi`$ の意味を $`M \in \mrm{Model}(\Sigma \conc \Phi)`$ だとする。
- 指標射に対する、フラグメントの変化に注目して、翻訳関手を定義する。
つまり、指標 $`\Sigma`$ に対して、$`\mrm{Frag}(\Sigma)`$ を定義して、$`\mrm{Sen}(\Sigma)`$ の代わりに使う。
