「セオリー」は使わざるをえないな

直前の記事「リントンの定理： 概要、実例、注意事項」の「注意事項への注意事項」と「セオリー」で述べたように、「セオリー」という言葉を使うのは出来るだけ避けたい。その理由は：$`
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{ \text{ in }}
`$

1. 地の文で使う日常語「理論」と紛らわしい。ただし、テクニカルタームとしての "theory" をカタカナ書き「セオリー」にすれば問題は緩和する。
2. 「セオリー」という言葉から、余計な（ときに有害な）連想をする人がいる。連想が、フォーマルな定義に基づくドライな思考を邪魔する。
3. 「セオリー」は曖昧多義語である。例えば、論理の文脈では、「導出に関して閉じた〈closed under {derivation | inference}〉論理式の集合」という意味でセオリーを使う。
4. ローヴェアのセオリーの理論〈theory of theories〉に限っても、ローヴェア圏をセオリーと呼ぶ人と、指標をセオリーと呼ぶ人がいる。

直前の記事の「セオリー」では、「ローヴェア・セオリー／ローヴェア圏」の代わりに「SAT圏〈SAT category〉」を使えばいいだろうと言いました。以前（例えば「ローヴェア・セオリーとその周辺」で） $`\mbf{LawTh}`$ と書いていた圏は $`\mrm{SAT}\mbf{Cat}`$ と書くことになります。

$`\mrm{SAT}\mbf{Cat}`$ は、SAT圏達からなる圏です。SAT圏はデカルト圏の特別なものなので、次の包含関係が成立します。

$`\quad \mrm{SAT}\mbf{Cat} \subseteq \mbf{CartCat} \In 2\mbf{CAT}`$

自然変換も考えれば、$`\mrm{SAT}\mbf{Cat}`$ と $`\mbf{CartCat}`$（小さいデカルト圏達の2-圏）は2-圏です。自然変換が不要なら、$`\mbf{CAT}`$ 内で考えます。

複圏〈オペラッド〉を使うアプローチを採用するなら、$`\mrm{SAT}\mbf{Multicat}`$ を使います。$`\mrm{SAT}\mbf{Multicat}`$ の対象は複圏ですが、複関手〈1-射〉と複自然変換〈2-射〉（「回路代数とグラフ置換モナド」参照）により2-圏になります。SAT複圏は一般的複圏の特別なものなので、次の包含関係が成立します。

$`\quad \mrm{SAT}\mbf{Multicat} \subseteq \mbf{Multicat} \In 2\mbf{CAT}`$

さて、$`\mrm{SAT}\mbf{Cat}`$ や $`\mrm{SAT}\mbf{Multicat}`$ の対象を総称して呼びたいときは何と呼べばいいでしょうか？ やっぱり「セオリー」と呼ぶしかないようですね。

SAT〈simple algebraic thoery〉は、ローヴェアのオリジナルの“セオリー”ですが、MAT〈many-sorted albebraic theory〉やGAT〈generalized algebraic theory〉もあります。様々な theory of algebraic theories が対象〈subject matter〉としている構造物は、総称的に「セオリー」です。

リントンの定理の主張をあらためて述べてみると：

• セオリー（またはセオリーの生成系である指標）に対するモナドを構成可能で、そのモナドのアイレンベルク／ムーア圏と、セオリーの表現の圏（指標のモデルの圏）が圏同値となる。

前半が“モナド-セオリー対応”で、後半が“代数-モデル対応”です。“代数-モデル対応”が成立するようなモナド（リントン／ローヴェア・モナド）を考えるので、“モナド-セオリー対応”が確立すれば自動的に“代数-モデル対応”は成立するとも言えます。

いずれにしても、モナドとセオリーを考えないとリントンの定理のステートメントを書けないので、困った用語でも「セオリー」を避けることは出来ないようです。