次のようなメタ記号を使う。$`\newcommand{\TS}{\mathrel{\,|\!-} }
\newcommand{\TTS}{\mathrel{\,||\!-} }
\newcommand{\TTTS}{\mathrel{\,|||\!-} }
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\In}{\text{ in } }
\newcommand{\cat}[1]{\mathcal{#1} }
%`$
- $`\TS_N`$ 自然演繹システムで証明可能
- $`\TTS_S`$ シーケントシステムで証明可能
- $`\TTTS_\Phi`$ メタシーケント・システム（論理フレームワーク）で証明可能
$`\Gamma`$ は論理式のリストとする。次は、$`\Gamma`$ を仮定して、論理式 $`P`$ が証明可能なこと。
$`\quad \Gamma \TS_N P`$
システム $`N`$ で演繹定理が成立するなら、次と同じ。
$`\quad \TS_N (\land)^*(\Gamma) \Imp P`$
ここで、$`(\land)^*`$ は二項演算をリスト引数化したもの。
自然演繹に対応するシーケント計算があったして、次のメタ定理が欲しい。
$`\quad (\TTS_S \Gamma \to P) (\Iff) (\Gamma \TS_N P)`$
これらのセマンティクスは：
- $`(\TTS_S \Gamma \to P) (\Iff) (\exists d : \Gamma \to P \In \cat{N}. \text{True} )`$
- $`(\Gamma \TS_N P) (\Iff) (\exists d : \Gamma \to P \In \cat{N}. \text{True} )`$
論理フレームワークを $`F`$ とすると、次のメタ定理が欲しい。
$`\quad ( \mathscr{K} \TTS_F \Gamma \to P) (\Iff) (\TTS_S \Gamma \to P)`$
また、メタシーケント計算システム $`\Phi`$ があって、次のメタ定理が欲しい。
$`\quad (\TTTS_\Phi \mathscr{K} \Rightarrow (\Gamma \to P)) (\Iff)
( \mathscr{K} \TTS_F \Gamma \to P)
%`$
セマンティクスは：
$`\exists d: \Gamma \to P \In \mathscr{K}^{*\Phi}
%`$
$`\mathscr{K}^{*\Phi}`$ は、生成系 $`\mathscr{K}`$ から作った自由$`\Phi`$複圏。次も成立する。
$`\quad \mathscr{K}^{*\Phi} = \cat{N}`$
