型理論では、コンテキストが必ず出てきます。コンテキストをヘビーに使う割には、あらためて「コンテキストとは何か？」と聞かれると、うまく答えるのは難しいですね。返答に窮するのは、たぶん僕だけではないでしょう。
型理論の圏論的定式化のひとつであるファミリー付き圏〈category with families | CwF〉でも、コンテキストという概念が出てきます。しかしこれは、実際に使っている具体的・構文的なコンテキストを抽象化・意味論化したもので、コンテキストとは単に“とある圏の対象”のことです。いわば、「ベクトルとは何か？」に「ベクトル空間（の台集合）の要素である」と答えるようなものです。
ここでは、「ベクトルとは何か？」に「幾つかの数を並べたものである」と答えるようなスタイルで、抽象化・意味論化される前の、具体的・構文的なコンテキストについて説明します。$`\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\wrld}[1]{\mathscr{#1}}
\newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right] }
\require{color}
\newcommand{\KW}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\ckw}[1]{ {\bf \text{ #1 } } } % classifier keyword
\newcommand{\hmr}{ \rightrightarrows }% horizontal meta rule
\newcommand{\vmr}{ \downdownarrows }% vertical meta rule
\newcommand{\Vvdash}{ |\!\!\vdash }
\newcommand{\Emp}{ \langle\rangle }
\newcommand{\l}[1]{ \mathsf{#1} } % literal
\newcommand{\Rule}[1]{ \textcolor{orange}{\underline{\text{#1}}\: } }
\newcommand{\Q}{ \textcolor{red}{\text{?}} }
`$
内容：
シリーズ・ハブ記事：
コンテキストとは
最初に、型理論で使うコンテキストの直感的でラフな（したがって若干不正確な）説明をします。
変数 $`x`$ と型 $`\alpha`$ をコロンを挟んで並べた $`x:\alpha`$ という形を（変数の）型宣言〈type declaration〉、あるいは単に宣言〈declaration〉と呼びます。幾つかの宣言をカンマで区切って並べたリストを型コンテキスト〈{type | typing} context〉、あるいは単にコンテキスト〈context〉と呼びます。コンテキストは次のように書きます。
$`\quad \langle (x_1 : \alpha_1), (x_2 : \alpha_2), \cdots, (x_n : \alpha_n)\rangle`$
宣言を丸括弧で囲っているのは、“ひとかたまり”として識別しやすくするためで、丸括弧は無きゃ無いでかまいません（識別しにくいときは付けますが）。
$`\quad \langle x_1 : \alpha_1, x_2 : \alpha_2, \cdots, x_n : \alpha_n\rangle`$
リスト全体を山形括弧で囲っているのも、コンテキストであることを強調するためで特に理由はありません（ほぼ気分）。
空リストやただ1つの宣言を含むリストもコンテキストです。
$`\quad \Emp \\
\quad \langle (x : \alpha) \rangle = \langle x : \alpha \rangle
`$
変数は名前で、変数として使っていい名前の集合を $`{\bf Name}`$ とします*1。集合 $`{\bf Name}`$ は前もって固定しておくとします。
さてところで、「構文的モナド」で次のように書きました。
このテの話をするとき困るのが、話題にしている構文的対象物と地の文のなかで使う記号の区別が難しいことです。フォントを変える方法もありますが、基本的には同じ書き方をします（文脈で判断）。どうしても区別したいときは、構文的対象物である算術式はバッククォートで囲むことにします。
今回もこの問題で悩みますが、次のようにします。
- 話題にしている構文的対象物内で使われるホントの名前（集合 $`{\bf Name}`$ の要素）はサンセリフ体で書く。
例えば、次はパターンではない“ホントのコンテキスト”の事例です。名前はすべてサンセリフ体になっています。
$`\quad \langle (\l{t} : \l{U}), (\l{x}:\l{t}\times\l{t}), (\l{n}: \l{N}) \rangle`$
それに対して以下は、コンテキストのパターンをメタ変数〈プレースホルダー〉 $`x, y, z, \alpha, \beta, \gamma`$ を使って表したものです。
$`\quad \langle (x : \alpha), (y: x \times x), ( z: \gamma) \rangle`$
すぐ上のパターンのメタ変数（イタリック体文字）を、下の表のようなホントの名前で置き換えると先の“ホントのコンテキスト”になります。
| メタ変数 | ホントの名前 |
| $`x`$ | $`\l{t}`$ |
| $`y`$ | $`\l{x}`$ |
| $`z`$ | $`\l{n}`$ |
| $`\alpha`$ | $`\l{U}`$ |
| $`\gamma`$ | $`\l{N}`$ |
幾つかのホントの名前の（想定される／意図している）意味を定義しておきます。
- $`\l{U}`$ ： 宇宙〈universe〉（銀河の対象クラス、「最近の型理論： 宇宙より銀河」参照）
- $`\l{N}`$ ： 自然数〈natural number〉型
- $`\l{I}`$ ： 単元集合〈singleton set〉型〈ユニット型〉
- $`\l{B}`$ ： ブーリアン型
先の“ホントのコンテキスト”の（想定される／意図している）意味は：
- $`(\l{t} : \l{U})`$ ： $`\l{t}`$ は、型（宇宙の要素〈インスタンス〉＝銀河の対象）である。
- $`(\l{x}:\l{t}\times\l{t})`$ ： $`\l{x}`$ は、型 $`\l{t}`$ と型 $`\l{t}`$ の直積型のインスタンスである。
- $`(\l{n}: \l{N})`$ ： $`\l{n}`$ は、自然数型のインスタンスである。
規則
型理論や論理ではナントカ規則というのが色々出てきます。が、人によって規則の分類法や命名法が違います。規則の分類・命名は後回しにして、規則記述に使う3つの記号だけ決めておきます。
- $`\vdash`$ ： ターンスタイル記号
- $`\Vvdash`$ ： 縦棒付きターンスタイル記号
- $`\hmr`$ ： 二本矢印
いずれも、前提と結論を区切る矢印類似記号（広義の矢印）です。
他に次のようなキーワードを使います。キーワードは、構文分類子〈syntactic classifier〉で、文法的種別を表します。これで全部ではないですが、必要になったら分類子キーワードを足すことにします。
- $`\ckw{univ-term}`$ 宇宙項（宇宙を表す記号的表現）
- $`\ckw{type-term}`$ 型項（型を表す記号的表現）
- $`\ckw{inst-term}`$ インスタンス項（型のインスタンスを表す記号的表現）
- $`\ckw{ctx}`$ コンテキスト
用語に関する注意事項として； 構文の話をしているときは、宇宙項を単に「宇宙」または「ソート」、型項を単に「型」、インスタンス項を（「インスタンス」ではなくて）単に「項」と呼びます。呼び名が短くなって便利ですが、あくまで構文的対象物〈syntactic object〉であることを強調したいので、ここでは省略せずに「項」を付けます。
ギリシャ文字大文字 $`\Gamma, \Delta`$ などはコンテキストを表すメタ変数とします。次は規則のパターンの一種です。
$`\quad \Gamma \vdash \alpha:\l{U} \ckw{type-term}`$
コンテキスト $`\Gamma`$ を前提として、$`\alpha`$ が宇宙項 $`\l{U}`$ の整形式〈well-formed〉な（構文的に許される）型項であることを主張しています。記号の日本語への翻訳は：
- $`\cdots \vdash \:\sim`$ (日本語→) ‥‥ を前提として ～ である
- $`\cdots \ckw{type-term}`$ (日本語→) ‥‥ は整形式型項
2つの型項から直積を作った形も型項として認めるよ、という規則は次のように書きます。
\hmr \Gamma \vdash \alpha\times \beta :\l{U} \ckw{type-term}
`$
普通は、'$`\hmr`$' ではなくて横線を引くのですが、横線の長さ調整が（LaTeXのマクロなしでは）難しいので、二本矢印 '$`\hmr`$' で代用します。同じことを日本語で書くなら：
同じコンテキスト $`\Gamma`$ を前提として $`\beta`$ も宇宙項 $`\l{U}`$ の整形式型項である
ならば コンテキスト $`\Gamma`$ を前提として $`\alpha\times \beta`$ は宇宙項 $`\l{U}`$ の整形式型項である。
これらの規則は、構文に対する主張や導出を語る道具であり、意味論については何も言ってません。
コンテキストの構文規則
コンテキストの構文規則を書き下しましょう。
`$
これは、「空リストは整形式コンテキストである」と主張しています。
コンテキスト $`\Gamma`$ に含まれる変数（コロンの左側の名前）の集合を $`\mrm{name}(\Gamma)`$ とします。$`\mrm{name}(\Gamma) \subset {\bf Name}`$ です。
既にあるコンテキストに新しい宣言を追加するときの規則を述べます。
\quad \Gamma \vdash u \ckw{univ-term} \quad t \not\in \mrm{name}(\Gamma)\\
\hmr \Vvdash \Gamma \cdot (t:u) \ckw{ctx}
`$
ここで出てきた記号 '$`\cdot`$' は、リストの最後の項目〈成分 | 要素〉として、$`(t: u)`$ を追加するリスト操作を表す中置演算子記号です。この規則が言っていることは：
$`\Gamma`$ を前提として $`u`$ は整形式宇宙項であり、
$`t`$ が $`\mrm{name}(\Gamma)`$ に含まれない
ならば $`\Gamma\cdot (t: u)`$ は整形式コンテキストである。
次の規則も使えます。
\quad \Gamma \vdash u \ckw{univ-term}\\
\quad \Gamma \vdash \alpha : u \ckw{type-term} \quad x\not\in \mrm{name}(\Gamma)\\
\hmr \Vvdash \Gamma \cdot (x:\alpha) \ckw{ctx}
`$
この規則が言っていることは：
$`\Gamma`$ を前提として $`u`$ は整形式宇宙項であり、
$`\Gamma`$ を前提として $`\alpha:u`$ は整形式型項であり、
$`x`$ が $`\mrm{name}(\Gamma)`$ に含まれない
ならば $`\Gamma\cdot (x:\alpha)`$ は整形式コンテキストである。
先に出てきた“ホントのコンテキスト”の事例
$`\quad \langle (\l{t} : \l{U}), (\l{x}:\l{t}\times\l{t}), (\l{n}: \l{N}) \rangle`$
は、$`\l{U}`$ を整形式宇宙項と認める事にして上記の“コンテキストの構文規則”を何度か適用すると、整形式な（構文的に許される）コンテキストだと分かります。導出の詳細は後でまた述べます。
単一宇宙
以下の話を単純化するために、宇宙項は宇宙定数 $`\l{U}`$ だけにします。よって、整形式の宇宙項を生成する規則は次だけです。
`$
空コンテキストを前提とする規則は、どんなコンテキストが前提でも成立する（後述）ので、次の規則が使えると思っていいです。
$`\quad \Gamma \vdash \l{U} \ckw{univ-term}
`$
整形式型項を生成する規則は必ず次の形（宇宙項が $`\l{U}`$）です。
$`\quad \Gamma \vdash \alpha : \l{U } \ckw{type-term}`$
必ず '$`:\l{U}`$' が付くなら省略しても同じことなので、以下 '$`:\l{U}`$' は省略することにします。
$`\quad \Gamma \vdash \alpha \ckw{type-term}`$
これは、単一の宇宙しか考えないことになります。一連のシリーズ記事は「階層化された宇宙達を備えた型理論」がテーマですが、今回は「ただ一つの宇宙だけを備えた型理論」を議論します。
前節で述べた「2つの型項から直積を作った形も型項として認めるよ」の規則は次のように簡素化されます。
\hmr \Gamma \vdash \alpha\times \beta\ckw{type-term}
`$
ちなみに、キーワードをリネームし、記号 '$`\times`$' を '$`\land`$' に書き換えてみると：
\hmr \Gamma \vdash \alpha\land \beta\ckw{prop-formula}
`$
命題〈proposition〉を表す論理式〈formula〉の構文規則と解釈できます（下に日本語記述）。型理論と論理のあいだに対応があるからです。
$`\Gamma`$ を前提として $`\beta`$ も整形式論理式である
ならば $`\Gamma`$ を前提として $`\alpha \land \beta`$ も整形式論理式である。
判断とその推論規則
区切り記号 '$`\vdash`$' と左辺・右辺、区切り記号 '$`\Vvdash`$' と右辺だけからなる規則（記号的表現）を型判断〈{type | typing} judgement〉、または単に判断〈judgement〉と呼びます。
判断を二種類（'$`\vdash`$'使用と'$`\Vvdash`$'使用）に分けたのは、意味論〈セマンティクス〉のときに異なる解釈をするからです。意味論は今回述べませんが、一言だけいっておくと：
- '$`\Vvdash`$'を使用した判断は、ファミリー付き圏〈CwF〉のベース圏の対象・射と解釈する。
- '$`\vdash`$'を使用した判断は、ファミリー付き圏の局所圏〈ファイバー〉の対象・射と解釈する。
記号 '$`\hmr`$' を含む規則（記号的表現）は、既存の判断から新しい判断を作り出す処方箋を与えます。判断を規則と考えるなら、'$`\hmr`$' を含む規則はメタ規則になります。記号 '$`\hmr`$' を含む規則を判断の推論規則〈inference rule〉と呼びます。文法の生成規則〈production rule〉に近いときは形成規則〈formation rule〉とも呼びますが、ここでは推論〈inference〉と形成〈formation〉の区別はしません。
論理との対応で言えば、判断はシーケントに相当し、判断の推論規則はシーケントの推論規則に相当します。推論規則を組み合わせた形は（形式的な）シーケント証明に相当します。が、型理論では「証明」とはあまり呼ばないようです。証明の代わりに導出〈derivation〉と呼び、証明可能シーケント相当物を導出可能判断〈derivable judgment〉と呼ぶのが（たぶん多数派の）習慣です*2。
判断と推論規則のまとめ
コンテキストの作り方に関する規則（判断と推論規則）を述べましょう。既に出した規則も再掲します。下線付きオレンジ色の名前は規則の名前です。まず、空コンテキストはコンテキストです。
\quad \Vvdash \Emp \ckw{ctx}
`$
型変数の宣言を追加してコンテキストを拡張するときは次の規則を使います。括弧に入った $`\Gamma, u, t`$ は、適用時に具体化すべきパラメータ（あるいはプレースホルダー）です。
\quad \Vvdash \Gamma \ckw{ctx}
\quad \Gamma \vdash u \ckw{univ-term} \quad t \not\in \mrm{name}(\Gamma)\\
\hmr \Vvdash \Gamma \cdot (t:u) \ckw{ctx}
`$
インスタンス変数の宣言を追加してコンテキストを拡張するときは次の規則です。
\quad \Vvdash \Gamma \ckw{ctx}
\quad \Gamma \vdash u \ckw{univ-term}\\
\quad \Gamma \vdash \alpha : u \ckw{type-term} \quad x\not\in \mrm{name}(\Gamma)\\
\hmr \Vvdash \Gamma \cdot (x:\alpha) \ckw{ctx}
`$
上記の規則で、一般的な宇宙項が出てきますが、今回は単一宇宙しか考えず、単一の宇宙を表す宇宙項（宇宙定数）は $`\l{U}`$ でした。
\quad \Emp \vdash \l{U} \ckw{univ-term}
`$
単一宇宙におけるコンテキスト拡張〈context extension〉の規則は次のように簡略化できます。
\quad \Vvdash \Gamma \ckw{ctx}
\quad t \not\in \mrm{name}(\Gamma)\\
\hmr \Vvdash \Gamma \cdot (t: \l{U}) \ckw{ctx}
`$
\quad \Vvdash \Gamma \ckw{ctx}
\quad \Gamma \vdash \alpha \ckw{type-term} \quad x\not\in \mrm{name}(\Gamma)\\
\hmr \Vvdash \Gamma \cdot (x:\alpha) \ckw{ctx}
`$
コンテキスト内にある型変数の宣言をそのまま取り出す（射影する）と整形式型項になります。宇宙 $`\l{U}`$ は固定しています。
\quad \Vvdash \Gamma \ckw{ctx}\\
\quad \Vvdash \Gamma \cdot (t:\l{U}) \ckw{ctx}\\
\hmr \Gamma \cdot (t:\l{U}) \vdash t \ckw{type-term}
`$
コンテキスト内にあるインスタンス変数の宣言をそのまま取り出す（射影する）と型付きの整形式インスタンス項になります。
\quad \Vvdash \Gamma \ckw{ctx}\\
\quad \Vvdash \Gamma \cdot (x:\alpha) \ckw{ctx}\\
\hmr \Gamma \cdot (x:\alpha) \vdash x:\alpha \ckw{inst-term}
`$
拡張したコンテキスト〈extended context〉において、もとのコンテキストでの整形式型項はやはり整形式型項です。
\quad \Vvdash \Gamma \ckw{ctx}\\
\quad \Gamma \vdash \xi \ckw{type-term}\\
\quad \Vvdash \Gamma \cdot (x:\alpha) \ckw{ctx}\\
\hmr \Gamma \cdot (x:\alpha) \vdash \xi \ckw{type-term}
`$
拡張したコンテキストにおいて、もとのコンテキストでの型付きの整形式インスタンス項はやはり整形式インスタンス項です。
\quad \Vvdash \Gamma \ckw{ctx}\\
\quad \Gamma \vdash M:\xi \ckw{inst-term}\\
\quad \Vvdash \Gamma \cdot (x:\alpha) \ckw{ctx}\\
\hmr \Gamma \cdot (x:\alpha) \vdash M:\xi \ckw{inst-term}
`$
型構成子記号 '$`\times`$'、'$`\to`$' に関する規則をまとめて挙げます。
\quad \Vvdash \Gamma \ckw{ctx}\\
\quad \Gamma \vdash \alpha \ckw{type-term}\quad \Gamma \vdash \beta \ckw{type-term}\\
\hmr \Gamma \vdash \alpha\times \beta\ckw{type-term}\\
%
\Rule{exp}(\Gamma, \alpha, \beta)\\
\quad \Vvdash \Gamma \ckw{ctx}\\
\quad \Gamma \vdash \alpha \ckw{type-term}\quad \Gamma \vdash \beta \ckw{type-term}\\
\hmr \Gamma \vdash \alpha \to \beta\ckw{type-term}
`$
3つの組み込みの型に関する規則は以下のとおりです。
\quad \Emp \vdash \l{N} \ckw{type-term} \\
\Rule{unit} \\
\quad \Emp \vdash \l{I} \ckw{type-term} \\
\Rule{bool} \\
\quad \Emp \vdash \l{B} \ckw{type-term}
`$
導出の事例
$`\quad \langle \l{t} : \l{U}, \l{x}:\l{t}\times\l{t}, \l{n}: \l{N} \rangle`$ がコンテキストであることを示してみましょう。そのためには、既に知られている判断から、次の判断を導出〈証明〉します。
$`\quad \Vvdash \langle \l{t} : \l{U}, \l{x}:\l{t}\times\l{t}, \l{n}: \l{N} \rangle \ckw{ctx}`$
何段階かに分けます。最初は $`\Vvdash \langle \l{t}:\l{U}\rangle \ckw{ctx}`$ を示します。この判断の導出を簡略に書くなら次のようです。
\KW{have } \l{t}\not\in \mrm{name}(\Emp)\\
\KW{apply } \Rule{ext-type-var}\\
\KW{conclude } \Rule{r1} \Vvdash \langle \l{t} : \l{U} \rangle \ckw{ctx}
`$
これは、既に知られている（持っている〈have〉）判断 $`\Rule{emp-ctx}`$と $`\l{t}\not\in \mrm{name}(\Emp)`$ という事実に、推論規則 $`\Rule{ext-type-var}`$を適用〈apply〉して目的の結論（$`\Rule{r1}`$と名付ける） $`\Rule{r1} \Vvdash \langle \l{t} : \l{U} \rangle \ckw{ctx}`$ が得られた〈concludeされた〉ことを表しています。もう少し丁寧に書くなら：
\quad \Vvdash \Emp \ckw{ctx}\\
\KW{have } \l{t}\not\in \mrm{name}(\Emp)\\
\KW{apply } \Rule{ext-type-var}(\Emp, \l{t})\\
\quad \Vvdash \Emp \ckw{ctx}
\quad \l{t} \not\in \mrm{name}(\Emp)\\
\hmr \Vvdash \Emp \cdot (\l{t}: \l{U}) \ckw{ctx}\\
\KW{conclude } \Rule{r1} \Vvdash \langle \l{t} : \l{U} \rangle \ckw{ctx}
`$
得られた判断 $`\Rule{r1} \Vvdash \langle \l{t} : \l{U} \rangle \ckw{ctx}`$ を使って、以下の判断 $`\Rule{r2} \langle\l{t}:\l{U}\rangle \vdash \l{t} \ckw{type-term}`$ を示せます（導出／証明できる）。
\quad \Vvdash \Emp \ckw{ctx}\\
\KW{have } \Rule{r1} \\
\quad \Vvdash \langle \l{t} : \l{U} \rangle \ckw{ctx}\\
\KW{apply }\Rule{proj-type}(\Emp, \l{t})\\
\quad \Vvdash \Emp \ckw{ctx}\\
\quad \Vvdash \Emp \cdot (\l{t}:\l{U}) \ckw{ctx}\\
\hmr \Emp \cdot (\l{t}:\l{U}) \vdash \l{t} \ckw{type-term}\\
\KW{conclude }\Rule{r2} \langle\l{t}:\l{U}\rangle \vdash \l{t} \ckw{type-term}
`$
さらに、$`\Rule{r3} \langle\l{t}:\l{U}\rangle \vdash \l{t}\times\l{t} \ckw{type-term}`$ を示します。
\quad \Vvdash \langle \l{t} : \l{U} \rangle \ckw{ctx}\\
\KW{have } \Rule{r2} \\
\quad \langle\l{t}:\l{U}\rangle \vdash \l{t} \ckw{type-term}\\
\KW{have } \Rule{r2} \\
\quad \langle\l{t}:\l{U}\rangle \vdash \l{t} \ckw{type-term}\\
\KW{apply } \Rule{prod}(\langle \l{t}:\l{U} \rangle, \l{t}, \l{t})\\
\quad \Vvdash \langle \l{t} : \l{U} \rangle \ckw{ctx}\\
\quad \langle\l{t}:\l{U}\rangle \vdash \l{t} \ckw{type-term}\quad \langle\l{t}:\l{U}\rangle \vdash \l{t} \ckw{type-term}\\
\hmr \langle\l{t}:\l{U}\rangle \vdash \l{t}\times \l{t} \ckw{type-term}\\
\KW{conclude }\Rule{r3} \langle\l{t}:\l{U}\rangle \vdash \l{t}\times\l{t} \ckw{type-term}
`$
次の判断も推論規則 $`\Rule{ext-inst-var}`$を使って導出可能であることはわかるでしょう。
$`\quad \Rule{r4} \Vvdash \langle \l{t}:\l{U}, \l{x}:\l{t}\times \l{t}\rangle \ckw{ctx}`$
コンテキスト水増し規則
前節の導出〈証明〉で、$`\langle \l{t}:\l{U}, \l{x}:\l{t}\times \l{t}\rangle`$ がコンテキストであることは分かりました。が、まだ $`\langle \l{t} : \l{U}, \l{x}:\l{t}\times\l{t}, \l{n}: \l{N} \rangle`$ がコンテキストかどうかは分かってません。が、「同様にやればOK」だと思えるでしょう。
導出の際に、次の推論規則が使えたら便利です。
\quad \Emp \vdash \alpha \ckw{type-term}\\
\quad \Vvdash \Gamma \ckw{ctx}\\
\hmr \Gamma \vdash \alpha \ckw{type-term}
`$
推論規則のパラメータを具体化すると次が得られます（これに推論規則 $`\Rule{ext-inst-var}`$ を適用すれば、目的の結論が得られます）。
\quad \Emp \vdash \l{N} \ckw{type-term}\\
\quad \Vvdash \langle \l{t}:\l{U}, \l{x}:\l{t}\times \l{t}\rangle \ckw{ctx}\\
\hmr \langle \l{t}:\l{U}, \l{x}:\l{t}\times \l{t}\rangle \vdash \l{N} \ckw{type-term}
`$
空コンテキストに限らずに一般化した推論規則として次が考えられます。
\quad \Vvdash \Gamma \ckw{ctx}\\
\quad \Gamma \vdash \alpha \ckw{type-term}\\
\quad \Vvdash \Gamma\odot\Delta \ckw{ctx}\\
\hmr \Gamma\odot\Delta \vdash \alpha \ckw{type-term}
`$
ここで、$`\Delta`$ は宣言のリストですが、それ自体で整形式コンテキストではないかも知れないものです。'$`\odot`$' はリストの連接〈concatenation〉の中置演算子記号です。リストを繋げた $`\Gamma\odot\Delta`$ が整形式コンテキストのとき、結論（'$`\hmr`$' の右側）が保証されます。
上記の推論規則は、一般的な「コンテキスト水増し〈thinnig〉規則」（ある前提で証明できるなら、前提を増やしても証明はできる）です。直感的には当たり前で、認めてもよさそうです。が、コンテキストの水増し規則をキチンと定式化しようとすると意外と難しかったりします。
このあたりを説明するには、構文論だけではなくて意味論も紹介したほうがよさそうなので、次の機会とします。
