限量子と代入、ベック／シュバレー条件 - 檜山正幸のキマイラ飼育記 (はてなBlog)

ベック／シュバレー条件〈Beck-Chevalley condition〉の一般的な記述（例えば、nLab項目）は抽象的で何を言ってるのか分かりにくいです。ベック／シュバレー条件の具体例として、述語論理における限量子と代入〈substitution | 置換〉の交換可能性があります。

代入を施した論理式に限量子を付けたものは、限量子を付けた論理式に代入を施したものと同値。

この交換可能性をベック／シュバレー条件の形で記述してみます。「Σ-Δ-Π随伴、もう一言」で述べたΣ-Δ-Π随伴〈随伴トリオ〉とも関係します。

この記事で使っている、カクカクで見栄えが良くないストリング図は、「カリー／ハワード対応のための記法・図法」で述べた方法で描いています。カクカクが気になるかたは、手描きか頭のなかでなめらかに補正してください。

説明不十分な記事ですが、とりあえず投稿した理由はこのリンクが参照している過去記事の冒頭と同じ意図です。

内容：

述語論理のモデル
ベック／シュバレー条件

述語論理のモデル

述語論理の（構文ではなくて）モデルについて説明します。古典的真偽値の集合を B = {0, 1} とします。0は偽で、1は真を表します。0 ＜ 1 という順序を入れておきます。Pred(X) := Map(X, B) と定義します。Pred(X) は集合X上の述語〈命題関数〉の集合です。Pred(X) に所属する述語達を考えるとき、Xを論域〈domain of discourse | 議論の領域〉と呼びます。述語の“主語”となのるのは、論域の要素です。

Pred(X) は順序集合になります。順序集合は自然に圏となるので、必要なら Pred(X) は圏とみなします。f:X → Y in Set に対して、Pred(f) = f^*(p) := f;p = p$`\circ`$f と定義すると、Pred:Set → Ord は反変関手になります。

限量子を考えるには、2つの論域（つまり集合） X, Y と写像 f:X → Y をひとつのシステムと考えます。Pred(f) = f^*(p) を Δ_f:Pred(Y) → Pred(X) in Ord とも書くことにして、順序集合に関するΣ-Δ-Π随伴を考えます。

$` \Delta_f:Pred(Y) \to Pred(X) \mbox{ in }{\bf Ord}`$
$` \Pi_f:Pred(X) \to Pred(Y) \mbox{ in }{\bf Ord}`$
$` \Sigma_f:Pred(X) \to Pred(Y) \mbox{ in }{\bf Ord}`$
$` \Delta_f \dashv \Pi_f `$
$` \Sigma_f \dashv \Delta_f `$

fとしては、Y = 1 のときの !_X:X → 1 in Set と、X = A×B, Y = A のときの π₁:A×B → A がよく使われます。また、∀_f := Π_f :Pred(X) → Pred(Y) 、∃_f := Σ_f :Pred(X) → Pred(Y) という記法も使います、限量子記号ですね。

f^*, ∀_f, ∃_f を備えた f:X → Y in Set が述語論理のモデルです。Xを全論域〈{total | entire} domain of discourse〉、Yを底論域〈base domain of discourse〉と呼ぶことにします。底論域が単元集合1であるケースが典型的です。限量子とは、全論域上の述語を底論域に押し出す操作になっています。f:X → Y は、（典型的事例からの連想で）射影〈projection〉と呼びますが、全射であることは要求していません。

述語論理のモデル (f:X → Y, f^*, ∀_f, ∃_f) は、射影fが決まれば自動的に決まってしまうので、以下、「モデル f:X → Y」のような簡略な書き方もします。あくまで略記であることには注意してください。

h:Z → W と f:X → Y が2つの（述語論理の）モデルだとします。次の図式を可換にするような k:Z → X, g:W → Y in Set の組をモデルのあいだの準同型写像 (k, g):(h:Z → W) → (f:X → Y) だとします。

$`\require{AMScd}%
\newcommand{\LA}{\big[\!\!\big(\,}\newcommand{\RA}{\,\big)\!\!\big]}%
\begin{CD}
Z @>{h}>> W \\
@V{k}VV @VV{g}V \\
X @>{f}>> Y \\
\end{CD}\\
\mbox{commutes in }{\bf Set}
`$

モデルのあいだの準同型写像 (k, g) は、全論域を全論域に／底論域を底論域に移し、射影を保存するような写像（の組）です。

モデルの準同型写像を定義する上記可換図式にPred反変関手を作用させると次の可換図式が得られます。

$`
\begin{CD}
Pred(Y) @>{f^\ast}>> Pred(X) \\
@V{g^\ast}VV @VV{k^\ast}V \\
Pred(W) @>>{h^\ast}> Pred(Z)
\end{CD}\\
\mbox{commutes in }{\bf Ord}
`$

可換図式の可換四角形（等式）を2-射 f^*;k^* ⇒ g^*;h^*:Pred(Y) → Pred(Z) *1だと思ってストリング図で描くと次のようになります。イコールを2-射ノードと考えます。

$`
\xymatrix {
{} \ar[dr]^{f^\ast}
&{Pred(X)}
&*[.]{} \ar[dl]_{k^\ast}
\\
{Pred(Y)}
&*++[o][F]{=} \ar[dl]^{g^\ast} \ar[dr]_{h^\ast} % センターのノード
&{Pred(Z)}
\\
{}
&{Pred(W)}
&{}
}
`$

注意すべきは、ストリング図のワイヤー矢印方向は射の方向ではないことです。矢印方向を正面だと思って、右手から左手が射の方向です。

ベック／シュバレー条件

述語論理のモデル (f:X → Y) のなかには、2つの随伴 $` f^\ast \dashv \forall_f,\; \exists_f \dashv f^\ast`$ が（自動的に）含まれますが、$`\exists_f \dashv f^\ast `$ のほうに注目します。この随伴の単位と余単位は次のようだとします。

$` \eta:: {\rm id}_{Pred(X)} \Rightarrow \exists_f ; f^\ast : Pred(X)\to Pred(X)`$
$` \varepsilon:: h^\ast;\exists_h \Rightarrow {\rm id}_{Pred(W)} : Pred(W)\to Pred(W)`$

この記述では、随伴の一般論に従い2-射の形で書いてますが、不等号で書けば次のようです。

$` \eta:: \forall p\in Pred(X).(\, p \le f^\ast(\exists_f(p)) \,)`$
$` \varepsilon:: \forall q\in Pred(W).(\, h^\ast(\exists_h(q) ) \le q \,)`$

前節のストリング図に対し、左上に単位（η）を接続して、右下に余単位（ε）を接続すると、もとの2-射（イコール）のメイトと呼ばれる2-射 k^*;∃_h ⇒ ∃_f;k^* ができます（下図）。これが可逆であることがベック／シュバレー条件ですが、今の場合は再びイコールになることです。

$`
\xymatrix {
{}
&{{\rm id}_{Pred(X)} } \ar@{.}[d]
&{}
&{k^\ast} \ar[d]
&{\exists_h} \ar[d]
\\
{Pred(X)}
&*++[o][F]{\eta} \ar[dl]_{\exists_f} \ar[dr]^{f^\ast} %単位
&*[.]{Pred(X)}
&*[.]{} \ar[dl]_{k^\ast}
&*[.]{}
\\
*[.]{} \ar[d]
&{Pred(Y)}
&*++[o][F]{ = } \ar[dl]^{g^\ast} \ar[dr]_{h^\ast} % センターのノード
&{Pred(Z)}
&*[.]{} \ar@{<-}[u]
\\
*[.]{} \ar[d]
&*[.]{} \ar[d]
&{Pred(W)}
&*++[o][F]{\varepsilon} \ar@{<-}[ur]_{\exists_h} \ar@{.}[d] %余単位
&{Pred(W)}
\\
{\exists_f}
&{g^\ast}
&{}
&{{\rm id}_{Pred(W)}}
&
}
`$

ベック／シュバレー条件は次の等式になります。

$` k^\ast ; \exists_h = \exists_f ; g^\ast : Pred(X)\to Pred(W)`$

あるいは、

$` \forall p\in Pred(X).(\, \exists_h(k^\ast(p)) = g^\ast(\exists_f(p)) \,)`$

典型的な状況として、モデルの準同型写像が次のようになっているとしましょう。

$`
\begin{CD}
Z = C\times D @>{h = \pi_1}>> W = C \\
@V{k}VV @VV{g}V \\
X = A\times B @>{f = \pi_1}>> Y = A
\end{CD}\\
\mbox{commutes in }{\bf Set}
`$

$` a = k_1(c, d),\; b = k_2(c, d)`$ と置いたとき、上の可換図式から次のように書けます。