空虚な束縛とEPペア

昨日の記事「全称・存在限量子の色々をまとめた絵」に対するオマケのようなものです。が、昨日の記事とは独立に読めます。

空虚な束縛〈vacuous quantification〉の話をします。随伴関手対の観点からの説明です。

内容：

1. 空虚な束縛とは
2. 随伴ペアとEPペア
3. 変数水増しと空虚な束縛
4. 射影の逆像と像はEPペア

空虚な束縛とは

Pが、集合X×Y上の述語だとします。構文的には、Pは変数x, yを含む（可能性がある）とします。正確には、意味領域の述語（真偽値をとる関数） P:X×Y→{True, False} と、それを表現する構文領域の存在物である論理式は別物なんですが、ここではあまり区別しないで、同じ記号で表します。「命題」という言葉も、意味領域の述語だったり、構文領域の論理式だったり、文脈で指すものが変わります。

さて、全称命題 ∀x∈X.P(x, y) や存在命題 ∃x∈X.P(x, y) を作ると、変数xは束縛〈bind〉されるので、自由変数はyだけになり、集合Y上の述語となります。限量子（∀か∃）の束縛作用により、述語の領域〈domain of discourse〉が変わります -- 束縛作用とはそういうものです。

Pに変数xが出現してない場合はどうでしょうか。例えば、X = Y = R として、

• P ≡ (y² = 2)

ここで、'≡'は論理式（構文的表現）として同じことです。構文的な論理式を関数とみなすのに型付きラムダ記法を使うなら、

• P = λ(x, y)∈R×R.(y² = 2 : {True, False})

冒頭で「あまり区別しない」と言ったのは、論理式としての y² = 2 と、関数としての λ(x, y)∈R×R.(y² = 2 : {True, False}) をどちらも同じPで表すよ、という意思表示です。

論理式 P ≡ (y² = 2) を限量子で束縛すると：

• ∀x∈R.P ≡ ∀x∈R.(y² = 2)
• ∃x∈R.P ≡ ∃x∈R.(y² = 2)

形の上では束縛してますが、束縛変数が出現しないので、束縛は無意味にみえます。このような束縛を空虚な束縛〈vacuous quantification〉と呼びます。「述語論理とインデックス付き圏と限量随伴性」では、若干意訳して「無意味限量」と言ってました。

これは名前通り、空虚で無意味に思えますが、実はなかなか面白いものです。空虚な束縛を分析するために、順序集合（むしろプレ順序集合）における随伴性を復習しましょう（次節）。

随伴ペアとEPペア

A = (A, ≦), B = (B, ≦) をプレ順序集合とします。プレ順序'≦'は次を満たします。

• a ≦ a ---(反射律)
• a ≦ b, b ≦ c ⇒ a ≦ c ---(推移律)

写像 f:A→B が単調〈monotone〉だとは、

• a ≦ b ⇒ f(a) ≦ f(b)

であることです。

f:A→B, g:B→A が単調写像だとして、次の条件について考えます。

1. ∀a∈A. a = g(f(a))
2. ∀a∈A. a ≦ g(f(a))
3. ∀b∈B. f(g(b)) = b
4. ∀b∈B. f(g(b)) ≦ b

このなかから2つの条件を選んで組み合わせます。まず：

• (∀a∈A. a = g(f(a))) ∧ (∀b∈B. f(g(b)) = b)

このとき、fとgは互いに逆です。fとgは逆ペアと呼んでいいでしょう。

次に：

• (∀a∈A. a ≦ g(f(a))) ∧ (∀b∈B. f(g(b)) ≦ b)

このとき、fとgは随伴ペアです。詳しくは次の記事を参照してください。

• 順序随伴性： ガロア接続の圏論

逆ペアと随伴ペアの中間の存在として：

• (∀a∈A. a = g(f(a))) ∧ (∀b∈B. f(g(b)) ≦ b)

このとき、fとgはEPペア〈EP pair〉と呼びます。EPは"embedding-projection"のことで、fが単射埋め込み、gがそれに対する全射射影と解釈できます。∀a∈A. a = g(f(a)) だけなら、gをレトラクション〈引き込み〉と呼ぶので、ER〈embedding-retraction〉ペアです。（もっとも、EPペアとERペアは明確に区別されないようです。）詳しくは次の記事を参照してください。

• レトラクションとベキ等自己射
• 「円周率は3」についてキッチリ考えてみる -- EPペアの例として

変数水増しと空虚な束縛

集合（議論の領域）Y上の述語全体の集合をPred[Y]と書きます。'Pred'と太字にしたほうが圏論と相性がいいですが、面倒なんで太字にしません。Pred[X×Y]も同じ解釈です。

Ï€₂:X×Y→Y は第二射影とします。この第二射影により、述語（真偽値をとる関数）の引き戻し Ï€₂^*:Pred[Y]→Pred[X×Y] が誘導されます。

• Ï€₂^*(Q) := Ï€₂;Q = QÏ€₂

すぐ上の定義は、意味的に考えたものですが、構文的にπ₂^*を考えると、変数yだけを含む（可能性がある）論理式Qを、ニ変数x, yの論理式だと“思い直す”ことです。“思い直す”だけなので、実際には何も起きず、分かりにくい操作です。

例えば、Q ≡ (y² = 2) として、π₂^*(Q) は、見た目はQとまったく変わりません。見て区別できません。しかし、変数xとyを持つ論理式とみなした y² = 2 なので、π₂^*(Q) = P なのです。ここで、Pは前節で定義した「たまたまxを含まない二変数論理式」です。

P, Qを意味的に考えて、真偽値をとる関数と解釈するなら：

• Q = λy∈R.(y² = 2)
• P = λ(x, y)∈R.(y² = 2)

実際には出現しない変数を足していくことを変数水増し〈variable thinning〉と呼びます。定数を関数とみなすのも変数水増しです。

• C0 = 3 （ほんとの定数）
• C1 = λx∈R.3 （一変数の定数関数）
• C2 = λ(x, y)∈R×R.3 （ニ変数の定数関数）

空虚な束縛や変数水増しは、構文的な操作ですが、構文的に考えていると分かりにくく正体不明です。意味的に考えましょう。集合X上の命題Pは、P:X→{True, False} という真偽値関数とみなせば意味的解釈になりますが、さらに、外延的に考えて {x∈X | P(x)} のような集合を命題の意味としましょう。

すると、π₂:X×Y→Y に伴って、逆像関数 Ï€₂^*:Pow(Y)→Pow(X×Y) が定義できます。ここで、Pow(-) はベキ集合を表します。

• Ï€₂^*(B) := {(x, y)∈X×Y | Ï€₂(x, y)∈B} = {(x, y)∈X×Y | y∈B}

存在記号∃に対応する写像は π_2*:Pow(X×Y)→Pow(Y) で、次のように定義される像関数 π_2*:Pow(X×Y)→Pow(Y) です。

• Ï€_2*(A) := {y∈Y | ∃x∈X.(Ï€₂(x, y) = y ∧ (x, y)∈A)} = {y∈Y | ∃x∈X.((x, y)∈A)}

この状況ならば、π₂^*, Ï€_2* の随伴性が見えやすくなります。次の図は「存在記号の除去規則について考える」で出したもので、設定が少し違います（第二射影じゃなくて第一射影）が、ヒントになるでしょう。

射影の逆像と像はEPペア

ここから先は、X×Y→Y という射影を単にπと書くことにします。毎回下付き'2'を書くのはめんどくさいし、第一射影でも第二射影でも話は変わらないので。

前節で述べた逆像写像は、π^*:Pow(Y)→Pow(X×Y) です。逆像写像を引き戻し〈pullback〉とも呼びますが、πと逆方向に部分集合を移すからです。述語（真偽値関数）Pに対するπの前結合 Pπ も、部分集合Bの逆像 {(x, y)∈X×Y | π(x, y)∈B} も、どちらも引き戻しと呼び、π^*(-) で表します。圏論のファイバー積も引き戻しなので、「引き戻し」は多義語です。

A∈Pow(X×Y) に対する像 π_*(A) は、

• Ï€_*(A) = {y∈Y | (x, y)∈A である x∈X が存在する}

像を対応させるπ_*、その値 π_*(A) を前送り〈pushuout | push-forward〉とも呼びます。

π^*とπ_*のあいだに次の関係があるのはすぐに分かるでしょう。

• B∈Pow(Y) に対して、π_*(Ï€^*(B)) = B
• A∈Pow(X×Y) に対して、A ⊆ Ï€^*(Ï€_*(A))

これは、π^*とπ_*がEPペアになっていることです。π^*がembeddingで、π_*がprojectionです。

π_*の論理的構文的解釈が存在限量子∃なので、π^*と∃がEPペアと言っても同じです。さらに、π^*の論理的構文的解釈が変数水増しオペレータなので、変数水増しオペレータと存在限量子がEPペアとも言えます。EPペアは、随伴ペアの特殊なものだったので、変数水増しオペレータと存在限量子は実際に随伴ペアです。

上記の事実を、論理的構文的にいえば：

• ∃x∈X.Q(y) ⇔ Q(y)
• P(x, y) ⇒ ∃x∈X.P(x, y)

変数水増しオペレータは表面に現れないので、[x, y]という形で無理に表現すれば：

• (∃x∈X.[x, y]Q(y)) ⇔ Q(y)
• P(x, y) ⇒ [x, y](∃x∈X.P(x, y))

全称限量子の場合は、少し複雑になりますが、同じスジミチをたどって、次が得られます。

• P(x, y) ⇔ ([x, y]∀x∈X.P(x, y))
• ([x, y]∀x∈X.P(x, y)) ⇒ P(x, y)

ここまで話した内容は、射影、像、逆像、補集合などの意味的（集合論的）な事実を、EPペアや随伴性を介して論理的構文的に再解釈してみたのです。論理では構文論（論理式と証明）のウェイトが高いですが、構文論だけではなかなか理解しにくいこともあるので、意味的解釈を併用しましょう -- というハナシでした。