形式化された議論であれ非形式的〈インフォーマル〉な議論であれ、命題と規則を区別する必要はあります。「型理論と論理： 非形式シーケント記法 // 規則は命題ではないのだが」において、規則は命題ではないと言ったのですが、混同されるのはそれなりの理由があります。規則から自明に誘導される命題があるので、「規則＝命題」という感じがするのでしょう。
「型理論と論理： 非形式シーケント記法」で述べたシーケント形式を事例に、命題と規則の関係について再考します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in }}
\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\ctxpair}[2]{ \begin{pmatrix}#1 \\ #2\end{pmatrix} }
%\newcommand{\fibot}{\twoheadleftarrow}
\newcommand{\fibto}{\twoheadrightarrow}
\newcommand{\incto}{\hookrightarrow }
\newcommand{\LLE}{\sqsubseteq } % Logical Less or Equal
%
\newcommand{\Rule}{\rightrightarrows}
%
\newcommand{\WF}{\mathbf{WF} }
\newcommand{\tot}{\mathbf{tot} }
\newcommand{\loc}{\mathbf{loc} }
\newcommand{\base}{\mathbf{base} }
\newcommand{\sect}{\mathbf{sect} }
`$
内容：
ナジメイ達の論文
「包括圏はなぜ「包括」圏なのか？」の最後の節において、ナジメイ／ヴァン・デル・ワイド／アーレンス／ノースの論文を引用しました。
- [NWAN25-]
- Title: A Type Theory for Comprehension Categories with Applications to Subtyping
- Authors: Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North
- Submitted: 13 Mar 2025
- Pages: 32p
- URL: https://arxiv.org/abs/2503.10868
「型理論と論理： 非形式シーケント記法 // シーケント形式の解釈」に挙げたシーケント形式とその解釈も、ナジメイ／ヴァン・デル・ワイド／アーレンス／ノース論文 [NWAN25-] を参考にしています。次節の事例も、[NWAN25-] の形式体系〈formal system〉のごく一部を切り取ったものです。
[NWAN25-] では、包括圏を語るための形式体系を構築しているのですが、僕は（今のところ）非形式的な記法としてシーケント形式を使いたいだけです。[NWAN25-] の形式体系を非形式的な用途で使う、というのが僕の目論見です。この記事はその目論見とはあまり関係してませんが、アイディアの借用元はナジメイ達の論文です。
圏を定義する規則
型理論では、圏の対象を $`\Gamma, \Delta`$ などのギリシャ文字大文字で書きますが、これは分野の伝統・習慣であり何の意味もありません。ラテン文字大文字 $`X,Y`$ にしたからといって何も変わりません。ラテン文字を使って、ベース圏を定義する規則を書いてみます。ベース圏の「ベース」はいったん忘れて、単に圏を定義する規則と思っていいです。
$`\quad \vdash^\WF X \\
\Rule\\
\quad X \vdash^\base \id_X : X
`$
横1行ではなくて、何行か使う“縦書き”レイアウトにします。もちろん、レイアウトが変わっても内容は何も変わりません。この規則は $`\id_X`$ という書き方を導入している規則です。シーケント形式を通常の圏論・集合論の記法に直して書けば：
$`\quad X\in |\cat{C}| \\
\Rule\\
\quad \id_X\in \cat{C}(X, X)
`$
$`\Rule`$ を $`\Imp`$ に置き換えると、普通の命題になるので、規則と命題を混同するのも無理もありません。
さて、射の結合〈合成〉に関して次の規則があります。
$`\quad \vdash^\WF X, Y, Z\\
\quad X \vdash^\base f:Y\\
\quad X \vdash^\base g:Z\\
\Rule\\
\quad X \vdash f;g :Z
`$
$`\vdash^\WF X, Y, Z`$ は以下の3つのシーケントをまとめて書いた略記です。
$`\quad \vdash^\WF X\\
\quad \vdash^\WF Y\\
\quad \vdash^\WF Z
`$
左単位律に相当する規則は次です。
$`\quad \vdash^\WF X, Y\\
\quad X \vdash^\base f:Y\\
\Rule\\
\quad X\vdash^\base \id_X ; f = f : Y
`$
規則が定義しようとしているモノ
規則は、既に存在するナニカについてナニゴトかを語っているわけではなくて、これから新しくナニカを作り出すやり方を指示しています。前節の例は、新しく圏を作ろうとしています。圏の対象集合〈the set of objects〉と対象ごとのホムセットに分けて作ろうとしています。
新しく作りだすべき圏の対象集合を $`?O`$ 、対象ごとのホムセットを $`?H(\hyp, \hyp)`$ としましょう。疑問符が付いているのは、まだよく分からない集合であることを示唆しています*1。$`?O, ?H(\hyp, \hyp)`$ を使って前節の規則を書き換えてみます。
恒等の導入
$`\quad X \in {?O} \\
\Rule\\
\quad \id_X \in {?H}(X, X)
`$
結合の導入
$`\quad X, Y, Z \in {?O}\\
\quad f \in {?H}(X,Y)\\
\quad g \in {?H}(Y, Z)\\
\Rule\\
\quad f;g \in {?H}(X, Z)
`$
左単位律
$`\quad X, Y\in {?O}\\
\quad f \in {?H}(X,Y) \\
\Rule\\
\quad \id_X ; f = f \In {?H}(X, Y)
`$
これだけでは圏の定義にならないですが、集合 $`?O`$ と、$`?O`$ の2つの要素でインデックス付けられた集合族 $`?H(\hyp, \hyp)`$ を作ろうとしているのは分かるでしょう。$`\id_\hyp`$ と $`\hyp;\hyp`$ は演算子記号〈関数記号〉です。集合／集合族が組み上がっていくに伴って、演算〈関数〉も定義されていきます。集合／集合族の帰納的構成と、集合／集合族の上の演算〈関数〉の再帰的定義を同時に記述しているわけです。
規則の集合は、集合／集合族と演算の組み合わせである構造を出現させる処方箋を与えます。具体的な処方箋の書き方（メタな構文）は色々あるにしても、使っている方法論はGAT〈generalized algebraic theory〉です。GATについては以下の過去記事で書いています。
別なレベルでのターンスタイルの使用
「型理論と論理： 非形式シーケント記法」で導入してこの記事でも使っているシーケント形式では、シーケントの左辺と右辺の区切り記号にターンスタイル '$`\vdash`$' を使っています。が、前節ではターンスタイルを消して、集合論の所属関係記号 '$`\in`$' を使って所属命題を記述しています。規則（集合の帰納的構成規則）の区切り記号には '$`\Rule`$' を使っています。
シーケント形式で使っていたターンスタイルが消えたので、今はターンスタイルが開放された状態です。「開放された」とは誰も使ってないことです。であるなら、'$`\Rule`$' の代わりに空いているターンスタイルを使ってしまえ、と。そうすると、前節の規則は次のように書けます。
恒等の導入
$`\quad X \in {?O} \vdash \id_X \in {?H}(X, X)
`$
結合の導入
$`\quad X, Y, Z \in {?O}, f \in {?H}(X,Y), g \in {?H}(Y, Z)
\vdash f;g \in {?H}(X, Z)
`$
左単位律
$`\quad X, Y\in {?O}, f \in {?H}(X,Y)
\vdash \id_X ; f = f \In {?H}(X, Y)
`$
こういうことが起きるんですよ。同じ記号が違う目的で、似てるけど違う目的で使われる。あるいは、とても似てるけど違うレベルで使われる。と、そんなことはよく起きます。だから混乱するわけです。原則として、記号は奪い合うものだと思っておいたほうがいいです（以下の過去記事参照）。
作り方から自明な命題
前節や前々節では、規則のなかに登場する集合／集合族の名前に疑問符を付けていました。$`?O`$ とか $`?H`$ とかです。新しく作りだすべき集合／集合族であり、作り終わるまでは未知・未定だから疑問符で目印してます。
規則、つまり帰納的構成規則にのっとって、目的の集合／集合族／関数が作れたとします。そのときは、疑問符を取り除いた名前 $`O, H`$ を使っていいでしょう。そして、作り終わって実在している集合／集合族／関数に関しては以下の命題は成立しています。
$`\quad X \in {O} \Imp \id_X \in {H}(X, X)
`$
$`\quad X, Y, Z \in {O}, f \in {H}(X,Y), g \in {H}(Y, Z)
\Imp f;g \in {H}(X, Z)
`$
$`\quad X, Y\in {O}, f \in {H}(X,Y)
\Imp \id_X ; f = f \In {H}(X, Y)
`$
なぜ成立しているのかというと、成立するように作っているからです。命題の証明は「作り方から明らか」でいいし、それ以上に言うこともないです。
集合／集合族の帰納的構成規則は規則であって命題ではありません。しかし、規則から自明に誘導〈induce | derive〉される命題があります。場合によって、規則と対応する命題が区別しにくい形式〈フォーマット〉で書かれるかも知れません。
以上が規則と命題が混同されて、「規則＝命題」と誤認される事情です。
*1:'$`\id`$' や '$`;`$' も、まだよく分からない関数の名前なので疑問符を付けるべきかも知れません。不徹底ですが、未知・未定の関数〈演算〉の名前はそのままとしています。
