このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

述語論理: 二重圏的ハイパードクトリン

ハイパードクトリンのベース圏はデカルト圏を仮定するのが普通です。が、デカルト圏の代わりに二重圏をベース圏として採用してみると、これはこれで使いやすい気がします。述語論理系やベック/シュバレー条件が比較的素直に定義できます。[追記]シード付き二重圏の定義が甘すぎたので、「述語論理: シード付き二重圏 -- 訂正と再論」に訂正を書いています。本文中でも、注意を追記しています。[/追記]$`\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\In}{\text{ in } }
\newcommand{\id}{\mathrm{id} }
\newcommand{\hyp}{\text{-} }
\newcommand{\Dwn}[1]{ {#1}\!\!\downarrow}
\newcommand{PPB}{\diamondsuit} % Predicate Pull Back
`$

内容:

関連記事事:

ハブ記事:

ハイパードクトリンのベース圏

ハイパードクトリン〈hyperdoctrine〉に関しては、以下の記事で述べています。

「ハイパードクトリン」という言葉は使ってないのですが(なんか気恥ずかしかったので)、以下の記事達も、内容的にはハイパードクトリンに関するものです。

$`\cat{C}`$ をハイパードクトリンのベース圏とします。通常、$`\cat{C}`$ はデカルト圏であると仮定します。つまり、$`\cat{C}`$ は直積と始対象を持ちます。直積の第一射影 $`\pi_1`$ を単に $`\pi`$ と書くことにします。

$`\quad \pi_{X, Y}: X\times Y \to X \In \cat{C}`$

この射影ごとに述語論理のモデルが構成されます。

ハイパードクトリンでは、デカルト圏 $`\cat{C}`$ の対象 $`X`$ ごとに、$`X`$ 上の述語達からなる“論理代数”を対応させます。論理代数とは、例えば次のようなものです。

  1. 順序集合
  2. 完備束
  3. 分配束
  4. ブール代数
  5. (小さい)デカルト閉圏
  6. (小さい)余完備デカルト閉圏
  7. ハイティング代数
  8. 完備ハイティング代数
  9. BI代数*1

これらはいずれも小さい圏とみなせるので、インデックス付き圏〈indexed category〉$`\cat{P}`$ が作れます。

$`\quad \cat{P}: \cat{C}^\mrm{op} \to {\bf Cat}`$

インデックス付き圏は、圏から“圏の圏”への反変関手です。ここでは、$`{\bf Cat}`$ の2-圏構造は使っていません(話を簡単にするために)。

射影 $`\pi_{X, Y}: X\times Y \to X`$ に反変関手 $`\cat{P}`$ を作用させると:

$`\quad \cat{P}[\pi_{X, Y}] : \cat{P}[X] \to \cat{P}[X\times Y] \In {\bf Cat}`$

関手への引数渡しにブラケットを使っているのは単なる習慣です。$`\cat{P}[\pi_{X, Y}]`$ を $`\PPB_X^Y`$ と略記します。

$`\quad \PPB_X^Y : \cat{P}[X] \to \cat{P}[X\times Y] \In {\bf Cat}`$

$`\PPB_X^Y`$ は、構文的には“述語の変数水増し”(実際には使ってない引数変数を増やす)を意味する関手です。関手 $`\PPB_X^Y`$ に左随伴関手と右随伴関手があるとき、それらを次のように書きます。

$`\quad \exists_X^Y \dashv \PPB_X^Y \dashv \forall_X^Y`$

図式としては次のように描けます。

$`\xymatrix@C+2pc{
\cat{P}[X\times Y]
\ar@/^1.5pc/[r]^{\exists_X^Y}_{\bot}
\ar@/_1.5pc/[r]_{\forall_X^Y}^{\bot}
& \cat{P}[X]
\ar[l]|{\PPB_X^Y}
}`$

これが、ハイパードクトリンにより定義される述語論理のモデル、あるいは述語論理系〈predicate logic system〉です。射影1つに対して述語論理系を1つ作れます。

ハイパードクトリンの条件として、ベック/シュバレー条件〈Beck-Chevalley condition〉がありますが、この条件は次のような引き戻し四角形図式ごとに記述されます。

$`\require{AMScd}
\begin{CD}
X\times Y @>{t \times \id_Y}>> X'\times Y\\
@VV{\pi_{X, Y}}V @VV{\pi_{X', Y}}V\\
X @>{t}>> X'
\end{CD}\\
\text{pullback in }\cat{C}
`$

ハイパードクトリンのベース圏としてデカルト圏を仮定するのは、次の要求があるからです。

  • 述語論理系を作るときに、直積の射影を必要とする。
  • ベック/シュバレー条件を記述するときに、引き戻し四角形を必要とする。

シード付き圏とシード付き二重圏

$`\cat{C}`$ は、デカルト性を仮定しない単なる圏だとします。$`\cat{S}`$ は $`\cat{C}`$ の広い部分圏($`|\cat{S}| = |\cat{C}|`$)だとします。自明な広い部分圏の例は:

  • $`\cat{C}`$ の恒等射だけからなる広い部分圏を $`\cat{S}`$ とする。
  • $`\cat{S} := \cat{C}`$ とする。

部分圏 $`\cat{S}`$ の射をシード射〈seed morphism〉と呼び、ペア $`(\cat{C}, \cat{S})`$ をシード付き圏〈category with seeds〉と呼ぶことにします。

$`\cat{E}`$ がデカルト圏で、有限個の対象(domain of discourse)達 $`\{D_1, \cdots D_n\}`$ から選んだ組の直積(だけ)で生成される $`\cat{E}`$ の部分圏 $`\cat{C}`$ を考えると、第一射影とみなせる射をシード射とするシード付き圏を作れます。このとき、$`s:A \to B`$ がシード射であるとは、次のような対象 $`X, Y`$ が存在することです。

$`\begin{CD}
A @>{s}>> B \\
@V{\cong}VV @VV{\cong}V\\
X\times Y @>{\pi_1}>> X
\end{CD}\\
\text{commutative in }\cat{C}
`$

図式内の同型($`\cong`$ でマークされている)は組み合わせ的に定義されるものに限定しますが、詳細は割愛します。伝統的な述語論理は、このセッティングで議論できます。

$`(\cat{C}, \cat{S})`$ は(デカルト性は仮定しない)シード付き圏として、$`\cat{C}`$ 内の可換四角形が、平行な二辺がシード射であるときシード四角形〈seed square〉と呼ぶことにします。シード射を左右の辺 $`s, s'`$ として描けば:

$`\begin{CD}
A @>{f}>> A'\\
@V{s }VV @VV{s'}V\\
B @>{t}>> B'
\end{CD}\\
\text{commutative in }\cat{C}
`$

[追記]上の図は、縦方向と横方向を逆にしたほうがよかったです。二重圏内で、 $`f, t`$ が縦1-射で、 $`s, s'`$ が横1-射です。[/追記]

シード付き圏 $`(\cat{C}, \cat{S})`$ をもとにして、二重圏 $`D`$ を定義できます。$`\cat{D}`$ がシード付き圏 $`(\cat{C}, \cat{S})`$ 上の二重圏だとは:

  1. $`\cat{D}`$ の二重2-射は、$`(\cat{C}, \cat{S})`$ のシード四角形である。(すべてのシード四角形が二重2-射だとは言ってない。)
  2. $`\cat{D}`$ の縦1-射横1-射の圏は $`\cat{S}`$ である。
  3. $`\cat{D}`$ の二重圏構造は、$`\cat{C}`$ の可換四角形の二重圏構造をそのま流用する。

シード付き圏 $`(\cat{C}, \cat{S})`$ と、その上の二重圏 $`\cat{D}`$ を一緒にした3つ組 $`(\cat{C}, \cat{S}, \cat{D})`$ をシード付き二重圏〈double category with seeds〉と呼ぶことにします。[追記]このシード付き二重圏の定義は特殊過ぎてうまくないです。「述語論理: シード付き二重圏 -- 訂正と再論」参照。[/追記]

二重圏的ハイパードクトリン

$`(\cat{C}, \cat{S}, \cat{D})`$ はシード付き二重圏だとして、この上のハイパードクトリンは次のモノ(構成素)から構成されます。

  1. 論理代数の圏 $`\cat{L}`$
  2. 忠実関手 $`U: \cat{L} \to {\bf Cat}`$
  3. 反変関手 $`P : \cat{C}^\mrm{op} \to \cat{L}`$
  4. $`\cat{P} := P*U`$ とする(アスタリスクは関手の図式順結合、フォントの違いに注意)
  5. シード射 $`s :A \to B`$ ごとの随伴トリプル $`\exists_s \dashv \cat{P}[s] \dashv \forall_s`$
  6. $`\cat{D}`$ の二重2-射ごとのベック/シュバレー条件

以下に補足説明をします。

$`\cat{L}`$ は、先に触れた論理代数、一例としてハイティング代数とその準同型射からなる圏です。論理代数の種類は特定はしません。しかし、論理代数は必ず圏とみなせるとして、圏とみなす関手が $`U`$です。

$`\cat{C}`$ の対象は、述語論理でいう論域〈議論の領域 | domain of discourse〉です。$`P`$ は論域ごとに、その上の述語からなる論理代数を対応させて、論域のあいだの射に述語の引き戻しを対応させます。

$`P`$ と $`P*U`$ は区別しない(オーバーロードする)ことが多いですが、ここではフォントを変えて区別します。カリグラフィー体の $`\cat{P}`$ は $`\cat{C}`$ 上のインデックス付き圏になります。

シード射 $`s:A \to B \In \cat{S} \subseteq \cat{C}`$ があると、述語論理系が作れます。述語論理系は、2つの論域上の2つの論理代数(を圏とみなしたもの)とそのあいだの限量子ペアからなります。それは次のように書けます。

$`\xymatrix@C+2pc{
\cat{P}[A]
\ar@/^1.5pc/[r]^{\exists_s}_{\bot}
\ar@/_1.5pc/[r]_{\forall_s}^{\bot}
& \cat{P}[B]
\ar[l]|{\PPB_s}
}`$

ここで、$`\PPB_s = \cat{P}[s]`$ です。$`\cat{P}[s]`$ は $`s^*`$ と簡略に書かれることもあります。

シード射と述語論理系は1:1に対応します。つまり、シード射の全体 $`\mrm{Mor}(\cat{S})`$ は、このハイパードクトリンに含まれる述語論理系の全体とみなせます。あるいは、シード射でインデックスされた述語論理系の全体がハイパードクトリンを構成するとも言えます。

ベック/シュバレー条件については次節で述べます。

ベック/シュバレー条件

この節では、$`s^* = \cat{P}[s]`$ という簡略な記法を用います。

ハイパードクトリン内の述語論理系とは、随伴トリプル $`\exists_s \dashv s^* \dashv \forall_s`$ のことです。随伴トリプルは、2つの随伴系〈随伴ペア〉を一緒にしたものです。

  • $`\exists_s \dashv s^*\text{ where } s^* : \cat{P}[B] \to \cat{P}[A] \In {\bf Cat}`$
  • $`s^* \dashv \forall_s\text{ where } \forall_s* : \cat{P}[A] \to \cat{P}[B] \In {\bf Cat}`$

随伴系達は全体として二重圏を形成します。そのことは以下の過去記事で書いています。

今回の話に出てくる“随伴系の二重圏”はかなり単純なもので一般論は不要です。

シード付き二重圏 $`\cat{D}`$ の二重2-射(シード四角形)を考えます。

$`\begin{CD}
A @>{f}>> A'\\
@V{s }VV @VV{s'}V\\
B @>{t}>> B'
\end{CD}\\
\text{commutative in }\cat{C}
`$

[追記]上の図は、縦方向と横方向を逆にしたほうがよかったです。二重圏内で、 $`f, t`$ が縦1-射で、 $`s, s'`$ が横1-射です。[/追記]

これに対して、$`{\bf Cat}`$ 内に次のような図式が描けます。

$`\begin{CD}
\cat{P}[A] @<{f^*}<< \cat{P}[A']\\
@V{\exists_s }VV @VV{\exists_{s'}}V\\
\cat{P}[B] @<{t^*}<< \cat{P}[B']
\end{CD}\\
\In {\bf Cat}
`$

この図式が厳密に(等式の意味で)可換であることは要求しませんが、自然同型を介して可換となることを要求します。つまり、次のような関手の同型があるとします。

$`\quad f^* * \exists_s \cong \exists_{s'} * t^* \In [\cat{C}, {\bf Set}]`$

これが、存在限量子 $`\exists_s`$ に関するベック/シュバレー条件〈Beck-Chevalley condition〉です。全称限量子 $`\forall_s`$ に関しても同様なベック/シュバレー条件を要求します。

二重圏 $`\cat{D}`$ のすべての二重2-射(シード四角形)において、ベック/シュバレー条件を課すと、全体として、二重圏 $`\cat{D}`$ から“随伴の二重圏”への二重関手〈double functor〉を定義します。存在限量子の随伴系に起因する二重関手と、全称限量子に起因する二重関手の2つがあります。

ハイパードクトリンの定義に現れる二重関手は、かなり強い条件を持つものですが、いずれにしても2つの二重関手がハイパードクトリンを定義します。

シード付き二重圏と、随伴系の二重圏への2つの二重関手により定義されたハイパードクトリンを二重圏的ハイパードクトリン〈double categorical hyperdoctrine〉と呼ぶことにします。ハイパードクトリンの議論に、二重圏の計算が利用できるようになるので、メリットはありそうです。

*1:https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf の Definition 4.11 参照。BI は bunched implication から。