述語論理とインデックス付き圏と限量随伴性 - 檜山正幸のキマイラ飼育記 (はてなBlog)

命題論理の圏論的対応物としてデカルト閉圏やその拡張があります。述語論理の圏論的対応物はトポスだと思っている方が多いでしょう。確かにトポスがあれば（高階の）述語論理の入念な議論ができますが、トポスは複雑で難しいです。もう少し簡単な圏論的構造で（一階の）述語論理を展開できないでしょうか -- ここでは、インデックス付き圏（indexed category）による述語論理の定式化を紹介します。

全称限量子は随伴性（adjunction）により導入されます。この随伴性を分析すると、無意味限量（vacuous quantification）や変数水増しのようなバカげた操作が、実は重要な役割を演じていることが分かります。

この記事は入門を意図してません。命題論理／述語論理のひととおりの知識を仮定しています。プログラム・コードを使って論理について説明した入門的記事があります。プログラムなら分かるんだけど、って方にはいいかも知れません。

プログラマのための述語論理 (2006年)
述語論理はJavaScriptを使うべきだった (2006年)

論理と証明、論理とモデルの関係は次の記事で扱っています。

論理とはなにか？ (2006年) 4回シリーズ記事

内容：

命題論理
連言含意論理とデカルト閉圏
述語論理
シンタックスとセマンティクス
変数の型、inとonと変数注釈の使い方
全称限量子
直積の射影に沿った述語論理
随伴の単位と余単位
述語論理におけるニョロニョロ
おわりに

命題論理

まずは命題論理の話からはじめましょう。用語の整理をするだけなので、ご存知の方はこの節は飛ばしてもかまいません。

命題論理を構成する基本概念は次のようなものです。

基本命題： a, b, c, ...
論理結合子： ∧（連言）、∨（選言）、¬（否定）、⊃（含意）
論理定数： T（真）、⊥（偽）
推論／証明

基本命題（{atomic, primitive, basic} proposition）は内部構造をもたない（仮にあっても考えない）アトミックな表現で、命題変数（propositional variable）または命題文字（propositional letter）と呼ばれる記号で表します。

論理結合子（logical connective, propositional connective）の選び方は目的や好みで変わります。古典論理をやる場合、∧と¬だけでも済みます。残りの論理結合子は次のように定義できます。

A∨B := ¬(¬A∧¬B)
A⊃B := ¬A∨B := ¬(¬(¬A)∧¬B)

∧、⊃、⊥だけを選んで、残りを次のように定義することもできます。

¬A := A⊃⊥
T := ¬⊥ := ⊥⊃⊥
A∨B := ¬(¬A∧¬B) := (A⊃⊥)∧(B⊃⊥) ⊃ ⊥

Tと⊥は論理定数（logical constant, propositional constant）で、前もって値が固定された命題文字です。

基本命題（命題変数）と論理定数（真と偽）をもとに、論理結合子で組み立てた形が命題論理式（propositional formula）です。例えば、a ⊃ (a∧b ⊃ ¬c) は命題論理式の一例です。命題論理式を単に命題（proposition）、または単に論理式（formula）とも呼びます。ここでは、命題論理式をA, B, C, P, Q, Rなどで表します。A, B, C, P, Q, Rなどの文字は、命題論理内部の命題文字（基本命題、命題変数）ではありません。命題論理式を一般的に表すメタ変数です。

証明（proof）が何であるかをここでは定義しませんが、A₁, ..., A_n を仮定してBを結論とする証明を φ:A₁, ..., A_n→B と書きます。A₁, ..., A_n→B という証明が存在することを A₁, ..., A_n |- B と書きます。'|-'は「証明可能（provable）」と読みます。次の3つのメタな主張は同じことです。

A₁, ..., A_nからBを証明できる。
A₁, ..., A_n |- B
φ:A₁, ..., A_n→B という証明φが存在する。

一般的な証明を基本的な証明から組み立てる場合、基本的（アトミック）なモノとして選んだ証明を推論（inference）と呼びます。一般的な証明は、推論を素材とする複合物になります。しかしこの記事では、証明と推論を神経質に区別はしません。

連言含意論理とデカルト閉圏

命題論理のなかでも特に簡単なモノとして、連言含意論理（conjunctive-implicational logic）があります。連言含意論理では、その名の通り、論理結合子は連言と含意だけです。選言と否定は考えません。また、論理定数はTだけです。とても簡単ですね。これから、事例としては連言含意論理を扱うことにします。

連言含意論理のモデルとしてデカルト閉圏（cartesian closed category）を考えます。話を簡単にするために、厳密デカルトモノイド閉圏（strict cartesian monoidal closed category）を紹介しましょう。厳密デカルトモノイド閉圏は、デカルト閉圏のなかでも単純な種別で、次のような特徴を持ちます。

Cは圏だとして、その上に対称厳密モノイド積 $\otimes$ 、モノイド単位I、指数▷、カリー同型Λが付属している。
A $\otimes$ B がAとBの直積を与え、Iは終対象となる。
厳密モノイド積は、次の交替律を満たす。
- (φ $\otimes$ ψ);(φ' $\otimes$ ψ') = (φ;φ') $\otimes$ (ψ;ψ')
- id_A⊗B = id_A $\otimes$ id_B
厳密モノイド積は、次の結合律、左右の単位律を満たす。（これらの法則が等式で成立しているところが、“厳密”と言われるゆえんです。）
- (A $\otimes$ B $\otimes$ )C = A $\otimes$ (B $\otimes$ C)
- I $\otimes$ A = A, A $\otimes$ I = A
任意の対象Aに対して、自己関手 A(-) と自己関手 A▷(-) は互いに随伴で、Λが随伴同型を与える。
- Λ^A_X,Y: C(A $\otimes$ X, Y) $\stackrel{\sim}{=}$ C(X, A▷Y) （カリー同型）

上のカリー同型で、X = A▷B, Y=B と置くと、

Λ^A_A▷B,B: C(A $\otimes$ A▷B, B) $\stackrel{\sim}{=}$ C(A▷B, A▷B)

C(A▷B, A▷B)のなかにはid_A▷Bがあるので、それをΛ^-1（反カリー化）でC(A $\otimes$ X, Y)側に持ってくれば、 A $\otimes$ A▷B→B という射ができます。これは評価射（eval）で、評価射を中心とした定義も可能です。

一番簡単な厳密デカルトモノイド閉圏は次のモノです。

|C| = {0, 1}、0＜1 として順序を入れて、順序から作られるやせた圏をCとする。
モノイド積は普通の掛け算・、モノイド単位は1とする。
指数▷は次のように定義する。
- 0▷0 = 1
- 0▷1 = 1
- 1▷0 = 0
- 1▷1 = 1
随伴は、x・y≦z ⇔ x≦y▷z

より一般に、ハイティング代数（Heyting algebra）が与えられれば、それから厳密デカルトモノイド閉圏を作れます。厳密性の条件を外せば、集合圏のようなバカでかいデカルト閉圏も扱えます。非厳密*1で巨大なデカルト閉圏も、カリー／ハワード対応の観点からは重要です。

なお、デカルト閉圏については、過去の記事で色々と書いています。

なぜ「光が影を作ること」と「主張の一部を再主張すること」が関係するのか；あるいは、デカルト圏入門 (2007年)
圏論的指数の周辺：ラムダ計算、デカルト閉圏、ノイマン型コンピュータ (2007年)
圏論的指数の定義 (2007年)
デカルト閉圏におけるお絵描き計算の基礎 (2007年)
モノイド閉圏、オダンゴ、留め金、池袋 (2008年)
演繹系とお絵描き圏論 (2009年)
この世で一番簡単なデカルト閉圏 (2011年)

述語論理

前の2つの節でザッとおさらいした圏論的命題論理（デカルト閉圏をモデルとする連言含意論理）の知識は仮定して、述語論理（predicate logic）について考えます。述語論理では、次の概念が追加されます。

変数： x, y, z, ...
定数（関数記号含む）： i, j, k, ..., f, g, h, ...
基本述語： p, q, r, ...
限量子： ∀, ∃

変数（variable）と定数（constant）をもとに項（term）が組み立てられます。例えば、定数として 0, 1, +（関数記号、演算子記号）があれば、(1 + 1) + (x + y) のような項を作れます。

項は基本述語（{atomic, primitive, basic} predicate）の引数になります。いくつかの引数（0個でもよい）を伴った基本述語が命題論理の基本命題に相当します。論理式の組み立て方は述語論理も命題論理も同じです。ただし、命題論理の結合子（ここでは∧と⊃だけ）以外に述語論理では限量子（ここでは∀だけ）を使うことができます。

ここからは、述語論理のモデルの話をします。集合の上の真偽値関数を、述語（のモデル）と考えます。これは、標準的・典型的なモデルです。Ωを前節で定義した{0, 1}上のデカルト閉圏とします。モノイド積は掛け算・、モノイド単位は1, 指数は前節で定義した▷です。Xを集合とするとき、X→|Ω| （|Ω| = {0, 1}）という写像がX上の述語です。今はモデルの話をしているので、述語は単なる記号ではなくて、実体としての存在物です。

集合X上の述語の全体をPred[X]と書きます。

Pred[X] := Map(X, |Ω|) = {f:X→{0, 1} | fは任意の写像}

1 = {0} とするとき、次が成立します。

Pred[1] = {f:{0}→{0, 1} | fは任意の写像} $\stackrel{\sim}{=}$ {0, 1}

f:X→Y を任意の写像とするとき、Pred[f]:Pred[Y]→Pred[X] を次のように定義できます。

Q∈Pred[Y] に対して、(Pred[f](Q))(a) = Q(f(a))

記号が煩雑になるので、Pred[f]をf^*と略記しましょう。すると：

(f^*(Q))(a) = Q(f(a))

反図式順の写像の結合を $\circ$ で表すなら：

f^*(Q) = Q $\circ$ f

f^*の記述がだいぶ簡単になりました。この形を見れば分かるように、f^*(Q)は、fによるQの引き戻し（pullback）です。

今定義したX上の述語Pは、P:X→{0, 1}という写像ですが、1の逆像P^-1(1)を考えるとXの部分集合になります。P←→P^-1(1) という対応で、Pred[X]はXのベキ集合Pow(X)とみなせます。そうすると、f^*(Q)は、Yの部分集合Qのfによる逆像とみなせます。

Predは反変関手ですが、これは反変のベキ集合関手（contravariant power-set functor）と同じものです。ただし、ベキ集合関手がSet→Setの自己関手であるのに対し、Predは少し異なった解釈をします。その点を次節で述べます。

インデックス付き圏としての述語モデル

この節で、述語論理のモデル構成のための基本的枠組みとなるインデックス付き圏について説明します。

反変ベキ集合関手Pow^*を考えると、これは Pow^*:Set→Set の自己関手と考えることができます。ここで、Pow^*(X)はPow(X)とまったく同じですが、反変性の目印として上付き星印を付けています。Pow^*(f)は、fによる逆像として定義します。ベキ集合Pow^*(X)はブール代数の構造を持つことを思い出せば、Pow^*:Set→BooleAlg （BooleAlgはブール代数の圏）となります。ベキ集合の順序構造に着目すれば、Pow^*:Set→Ord （Ordは順序集合の圏）です。

さらには、ベキ集合は（順序から誘導される）圏の構造を持つので、Pow^*:Set→Cat という関手ともみなせます。一般に、適当な圏BからCat（小さな圏の圏）への反変関手をインデックス付き圏（indexed category）と呼びます。そう、反変ベキ集合関手はインデックス付き圏とみなせるんです。

インデックス付き圏については、次の過去記事にも説明があります。

インデックス付き圏のグロタンディーク構成

また、次の記事はこの節の内容に近いです。

ホーア論理の圏論的な定式化

さて、集合Xにその上の述語の全体Pred[X]を対応させる関手は、実質的に反変ベキ集合関手Pow^*と同じものですが、Pred[X]は圏だと解釈します。集合Xごとに圏がくっついているような構造ですね。

改めて、インデックス付き圏としてのPredを定義しましょう。まず、集合圏の部分圏Bを定めます。このBをベース圏（base category）と呼びます。集合圏の特定された終対象を1として、1∈Bは仮定しておきます。したがって、最小のベース圏は1だけからなる圏です。

ベース圏Bの対象（集合）Xに対して、Pred[X]は単なる圏ではなくてデカルト閉圏です。そこで、“小さなデカルト閉圏の圏”をCCCとして、Predを B→CCC という反変関手と解釈します。詳しく言えば：

X∈B に対して、Pred[X]は（小さな）デカルト閉圏である。
f:X→Y in B に対して、Pred[f]:Pred[Y]→Pred[X] は閉関手（closed functor）である。
f:X→Y, g:Y→Z in B に対して、Pred[f;g] = Pred[g]*Pred[f] （'*'は関手の図式順結合）
Pred[id_X] = Id_Pred[X] （恒等関手）

既に述べたように、Pred[f]はf^*と略記します。f^*:Pred[Y]→Pred[X] in CCC が閉関手ということは、f^*はデカルト閉圏としての構造を保つことを意味します。

ここで、閉関手について注意しておきます。一般的な閉関手では、指数▷に対して F(A▷B) = F(A)▷F(B) は要求しません。この等式条件はきつ過ぎて、応用を狭めてしまうからです。C, Dが厳密デカルト閉圏の場合でも、F:C→C に上記等式を要求するのは得策ではありません。 F(A▷B) = F(A)▷F(B) が成立したらもちろん嬉しいが、そこまでは期待しません、という態度をとります。閉関手についてもっと知りたいなら、nLabの記事などを参照してください。

https://ncatlab.org/nlab/show/closed+functor

まとめると、述語論理のモデルは次のようなものから構成されます。

集合圏の部分圏B。Bの対象は集合、Bの射は写像だが、すべての集合・写像を考える必要はない。Bはインデックス付き圏のベース圏である。
小さいデカルト閉圏を対象として、閉関手を射とする圏の圏CCC。デカルト閉圏を厳密デカルト閉圏に限る場合でも、射である閉関手は指数を等式的に保存することは仮定しない。（指数を等式的に保存したらラッキー。）
反変関手 Pred:B→CCC。これは、デカルト閉圏を値とするインデックス付き圏なので、インデックス付きデカルト閉圏（indexed cartesian closed category）と言える。
Pred[f]をf^*と略記する。インデックス付き圏の用語では、f^*を再インデキシング関手（reindexing functor）、またはベース取り替え関手（base-change functor）と呼ぶ。

一階述語論理の概念／用語と圏論の概念／用語の対応は次のようになります。

一階述語論理	圏論
解釈領域X	ベース圏Bの対象X（Xは集合）
X上の述語P	デカルト閉圏Pred[X]の対象P
X上の述語のあいだの証明／導出	デカルト閉圏Pred[X]の射
解釈領域のあいだの写像f	ベース圏Bの射f（fは写像）
写像fによる述語の引き戻し	デカルト閉圏のあいだの閉関手f^*
真偽値	デカルト閉圏Pred[1]の対象
連言	デカルト閉圏の直積
含意	デカルト閉圏の指数
論理定数の真	デカルト閉圏の単位対象（＝終対象）
演繹定理	カリー同型Λ

命題論理とは、特定の集合X上のデカルト閉圏Pred[X]だけを考えることです。特にPred[1]は真偽値を扱う命題論理となります。述語論理の（命題論理と対比した）特徴は、複数の解釈領域を同時に考えることです。そのときの“複数の解釈領域”がベース圏Bで指定されます。

シンタックスとセマンティクス

今まで、論理のシンタックス（構文論）とセマンティクス（意味論）をあまり区別せずに（有り体に言えば、ゴッチャにして）話してきました。シンタックスとセマンティクスをキチンと分けて話すのはとても労力がかかるからです。そして、その労力に見合った効果が得られると期待もできません。

述語論理を構成するさいに、変数記号、定数記号（関数記号を含む）、基本述語記号などの記号を準備します。それらの記号には型を与えておくのが便利です。構文的には、型もまた単なる記号です。基本型から複合型を作るには型構成記号も必要です。

例えば、自然数論を展開するには、型記号（あくまで記号）N、種々の型の変数記号、定数記号、述語記号を準備します。型構成記号として','（カンマ）と'♂'もあるとしましょう。

変数記号の型宣言 n, m:N （変数記号'n', 'm'の型（の記号）は、'N'である）
定数記号の型宣言 0, 1:N （定数記号'0', '1'の型（の記号）は、'N'である）
関数記号の型宣言 a:(N,N)♂N （関数記号'a'の型（の記号）は、'(N,N)♂N'である）
述語記号の型宣言 e:N,N （述語記号'e'の型（の記号）は、'N,N'である）

このような構文的な型宣言をして、その上で記号の意味を確定していきます。記号に意味を対応させる写像（の記号）は、〚 … 〛がよく使われます。スコット・ブラケット（Scott brackets）とか意味ブラケット（semantic brackets）と呼ばれます。まずは型の意味：

〚N〛 = N （型記号'N'の意味は、自然数の集合N）
〚α,β〛 = 〚α〛×〚β〛（型構成記号','の意味は、集合の直積）
〚α♂β〛 = Map(〚α〛,〚β〛) （型構成記号'♂'の意味は、写像（関数）の集合）

定数、関数、述語の意味：

〚0〛 = (自然数の0) 〚0〛∈N
〚1〛 = (自然数の1) 〚1〛∈N
〚a〛 = (自然数の足し算 +_N) 〚a〛∈Map(N×N, N)
〚e〛 = (自然数の等号 =_N) 〚e〛∈Rel(N, N)、Relは二項関係の集合

このような定義の後で、項'a(1,1)'とか論理式'e(a(0,1), a(1,0))'などの意味が計算できます。

    〚a(1,1)〛
  = 〚a〛(〚1〛,〚1〛)
  = +_N(1,1)
  = 自然数としての 1 + 1
  = 2

    〚e(a(0,1), a(1,0))〛
  =  =_N(+_N(0,1), +_N(1,0))
  = =_N(1, 1)
  = 自然数に関する命題 “1 = 1”
  = true

どうでしょうか？しっちめんどくさいなー！と思いませんか。面倒でもこういうキッチリした議論を一度くらいは体験する価値はあるかも知れません。けど、一度で十分。僕は毎度繰り返す気力はありません。したがって、このテの話は割愛します。

次のような方針にします。

記号とそれに対応する実体をいちいち区別しない。
構文的な型と、ベース圏Bの対象（集合）を同一視する。
特定の型の定数は、ベース圏Bの射と同一視する。
c : X という型宣言を持つ定数cは、c:1→X in B と解釈する。
f : X→Y という型宣言を持つ関数fは、f:X→Y in B と解釈する。
P : X という型宣言を持つ述語Pは、デカルト閉圏Pred[X]の対象と解釈する。
論理結合子∧、⊃と、デカルト閉圏の直積、指数を同じ記号で表す。つまり、' $\otimes$ ', '×', '・'などの代わりに'∧'を使ってもよく、'▷'の代わりに'⊃'を使ってもよい。
構文的な意味での証明・推論をここでは定義しないが、デカルト閉圏Pred[X]の射 φ:A₁∧...∧A_n→B があれば、A₁, ... ,A_nからBが証明できる、と考える。つまり、デカルト閉圏Pred[X]の射は、解釈領域X上の証明とみなす。

このような“ある程度はイイカゲン”な方針を採用するので、「命題」（proposition）、「論理式」（formula）、「述語」（predicate）は区別しません、同義語です。

変数の型、inとonと変数注釈の使い方

定数／関数、述語（命題）、証明／推論／導出は、ベース圏B上のインデックス付きデカルト閉圏Predのなかで実体を持ちます。前節の方針にしたがい、記号と対応する実体の区別はしません。しかし、変数は例外です。変数記号に対応する実体はありません。変数に対する型宣言は、従来通り「変数 : 型」の形を使います。型はBの対象なので、「変数 : Bの対象」です。

実体の型宣言はコロンではなくて、'in'を使うことにします。

型＝解釈領域： X in B ⇔ X∈|B|
関数／項： f:X→Y in B ⇔ f∈B(X, Y)
述語： P in Pred[X] ⇔ P∈|Pred[X]|
証明： φ:P→Q in Pred[X] ⇔ φ∈Pred[X](P, Q)

述語と証明に関しては、より短く書くために'on'を使います。

述語： P on X ⇔ P in Pred[X]
証明： φ:P→Q on X ⇔ φ:P→Q in Pred[X]

「P on X」は「Pは集合X上の述語である」、「φ:P→Q on X」は「φはPからQを導出する集合X上の証明である」と読みます。

変数の実体はないのですが、構文的な話のなかで変数は重要です。我々は、変数を実体に対する付加的な注釈と考えます。xが型Xの変数のとき、述語Pに対して P[x:X] という書き方を認めます。これは、X上の述語Pを変数xと共に考える、といった意味です。

x:X が前もって宣言されているなら、P[x:X]をP[x]と書いてもかまいません。P[x]は、述語Pに引数を渡した値ではありません。P[x] = P ですが、使用する変数の情報が付加されているだけです。どんな変数を使おうがPに変わりはないので、P[x] = P[y] = P です。

φ:P→Q on X の代わりに、φ:P[x:X]→Q[x:X] と書いても同じです。あるいは、x:X, φ:P[x]→Q[x] でもいいです。いずれの書き方でも、P, Qは集合X上を走る変数で記述され、φはX上での証明だと主張しています。

全称限量子

述語論理の特徴は、同時にたくさんの解釈領域を考えることだと言いました。解釈領域とは、ベース圏Bの対象のことです。異なる解釈領域上の述語は、写像（Bの射）による引き戻しで関連付けられます。

ただ、これだけだと述語論理だと呼ぶには物足りない。述語論理といえば、… そうです、限量子（quantifier; 量化子）ですね。ここでは、全称限量子（universal quantifier）だけ扱います。

限量子を、引き戻し関手の随伴関手として定義できることに気づいたのはローヴェル（William Lawvere）とのことです。全称限量子は引き戻し関手の右随伴（存在限量子は引き戻し関手の左随伴）です。

ベース圏Bの射 f:X→Y に対して引き戻し f^*:Pred[Y]→Pred[X] が決まります。f^*の右随伴関手があれば、それもfから決まります。f^*の右随伴関手を∀_fと書くことにします。（f_*とかΠ_fとかも使われます。左随伴関手は、f_!, Σ_f など。）

f^* -| ∀_f （∀_fはf^*の右随伴、f^*は∀_fの左随伴）から、次の同型が存在します。

Pred[Y](f^*(P), Q) $\stackrel{\sim}{=}$ Pred[X](P, ∀_f(Q))

左から右へと読むなら、f^*(P)→Q on Y という証明があれば、P→∀_f(Q) on X という証明があることを意味します。証明から証明への導出規則はシーケントの推論図として書けるので、次のシーケント推論があるとも言えます。シーケントの推論図の上下区切りは二重線とします。

   f^*(P)→Q on Y
  ================
   P→∀_f(Q) on X

二値論理で考えるなら、任意の写像 f:X→Y に対してf^*の右随伴∀_fが存在します。全称記号'∀'を使って表しましたが、∀_fは我々の全称の概念を超えるものです。例えば、fが単射のとき、∀_fは命題の定義範囲の拡張を与えます。

通常の述語論理では、fをものすごく制限して考えます。具体的には、自明な写像 !_X:X→1 か、直積の射影 π¹_X,Y:X×Y→X くらいしか考えません。実用上はそれで足りているのですが、任意のfに対する一般化限量子∀_fを考えるほうがたぶん楽しいです*2。

直積の射影に沿った述語論理

X, Y in B のとき、X上の論理系Pred[X]とY上の論理系Pred[Y]を考えることができます。これらをバラバラに考えている限り、単に2つの命題論理があるだけです。f:X→Y in B に対して、命題の引き戻し関手 f^*:Pred[Y]→Pred[X] in CCC と全称限量子 ∀_f:Pred[X]→Pred[Y] in CCC を一緒に考えた論理系を、写像fに沿った述語論理（predicate logic along f）と呼ぶことにします。

集合X, 1と、自明な写像 !_X:X→1 in B に対して、!_Xに沿った述語論理を考えると、それはX上の単項述語に関する述語論理になります。Pred[1]は真偽値の圏で、二値論理ならΩ（|Ω| = {0, 1}）です。引き戻し (!_X)^*:Pred[1]→Pred[X] は、真偽値をX上の命題とみなすことで、構文的には論理定数（命題定数）の導入です。全称限量子 ∀_{!_X}:Pred[X]→Pred[1] は、単項述語 P = P[x:X] を単一の変数xで全称束縛すること P[x:X] |→ ∀x.P[x:X] です。

もうひとつのｆの例として、f:X×Y→X を第一射影とします。第一射影を以下πと書きます。具体的には、π(x, y) = x です。P = P[x:X] に対して、引き戻し π^*(P) は、X上の述語Pに、ダミー変数 y:Y を追加してX×Y上の述語とみなしたものです。P[x:X]にダミー変数を追加した述語を [x:X, y:X].P[x:X] と書くことにします。

[x:X, y:X].P[x:X] = (P $\circ$ π)[x:X, y:Y] = (π^*(P))[x:X, y:Y]

"[x:X, y:X]."を“述語に対する作用素”と考えて、変数水増し（variable thinning）作用素と呼ぶことにします。同様な操作を型理論では、文脈弱化（context weakening）と呼ぶことがあります。変数の型が分かっているときは、[x:X, y:Y]. を [x, y]. と略記します。

射影 π:X×Y→X に沿った述語論理を考える際に、∀_πを、変数を使った次の形で書きましょう。

∀_π(P) = ∀y:Y.P[x:X, y:Y]

これも∀y.P[x, y]のような略記を許します。束縛変数は自由にリネームできるので、∀w.P[x, w]でも同じです。

πに沿った述語論理では、π^*と∀_πの随伴性は次の形です。

   π^*(P)→Q on X×Y
  ===================
   P→∀_π(Q) on X

変数を使った記法で書けば：

   [x, y].P[x]→Q[x, y]  on X×Y
  ===============================
   P[x]→∀w.Q[x, w] on X

この規則には、異なる解釈領域上の2つの述語P, Qが登場していることに注目してください。証明の仮定側の変数水増し、証明の結論側の全称束縛により、異なる解釈領域上の証明を互いに融通できることを示しています。

述語P, Qを、対応する部分集合として解釈してみましょう。つまり P⊆X, Q⊆X×Y とみなします。このとき、π^*:Pow(X)→Pow(X×Y) は射影の逆像、∀_π:Pow(X×Y)→Pow(X) は補集合(-)^cと順像π_*を組み合わせた次の対応です。

∀_π(Q) := (π_*(Q^c))^c

ちなみに、存在限量子∃_πなら、単なる順像π_*です。

引き戻しと全称限量子の随伴性は次の形に書けます。

(π_*(P)⊆Q in Pow(X×Y)) ⇔ (P⊆∀_π(Q) in Pow(X))

随伴の単位と余単位

射影 π:X×Y→X に沿った述語論理では、述語の引き戻しπ^*と全称限量子∀_π のあいだに随伴関係 π^* -| ∀_π があり、次の同型が成立するのでした。

Pred[X×Y](π^*(P), Q) $\stackrel{\sim}{=}$ Pred[X](P, ∀_π(Q))

随伴ペア π^*, ∀_π があると、随伴の単位（unit）ηと随伴の余単位（counit）εが計算できます。ηとεは、関手と関手をつなぐ自然変換です。

η::Id ⇒ ∀_π・π^* : Pred[X]→Pred[X]
ε::π^*・∀_π ⇒ Id : Pred[X×Y]→Pred[X×Y]

ここで、'・'は関手の反図式順結合だとします。

随伴の単位と余単位の計算は定型的な操作ですが、めんどくさいので結果だけを示します。自然演繹の証明図の形で書きます。

                P[x] on X
  ---------------------------[η P]
   ∀w:Y.[x, w].P[x] on X


    [x, y].∀w:Y.Q[x, w] on X×Y
  -------------------------------[ε Q]
    Q[x, y] on X×Y

1番目の規則の下段は、無駄な全称限束縛が導入されています。束縛変数wがPに入ってないので、束縛しても何の意味もないのです。この操作を無意味全称化（vacuous universal quantification）と呼びます。

2番めの規則は、二項述語の一方の変数による全称記号を取り除いているので、全称除去規則と言ってもいいでしょう。下段の変数yは自由変数になってますから、全称束縛変数を自由変数へ置き換えています。この操作は全称変数の自由化と呼びましょう。

以上のことをまとめると、射影による引き戻しπ^*と全称限量子∀_πの随伴（adjunction）に関して：

随伴の単位ηは、無意味全称化によって与えられる。
随伴の余単位εは、全称変数の自由化によって与えられる。

述語論理におけるニョロニョロ

2つの関手の随伴性は、単位と余単位を用いたニョロニョロ関係式（snake relation）で表現できます。ニョロニョロが随伴性の本質だ、と言ってもいいでしょう。

F -| G （FはGの左随伴、GはFの右随伴）で、η, εをその単位、余単位とするとき、（厳密な）ニョロニョロ関係は、次の2つの等式のことです。

(G*η);(ε*G) = G
(η*F);(F*ε) = F

ここで、'*'は関手／自然変換の図式順ヒゲ結合（whiskering）、';'は自然変換の図式順縦結合です。右辺のF, Gは、関手そのものではなくて、関手の恒等自然変換の略記です。

π^* -| ∀_π という随伴に対するニョロニョロ関係式は次です。

(∀_π*η);(ε*∀_π) = ∀_π
(η*π^*);(π^**ε) = π^*

自然演繹の図示の習慣と合わせるには、ヒゲ結合／横結合のほうは反図式順にする必要があります。反図式順のヒゲ結合／横結合を'・'で表すと：

(η・∀_π);(∀_π・ε) = ∀_π
(π^*・η);(ε・π^*) = π^*

途中経過は省略しますが、(η・∀_π);(∀_π・ε) を自然演繹の証明風に表すと次の図になります。

               ∀w.Q[x, w] on X
  --------------------------------(無意味全称束縛)
   ∀y.[x, y].(∀w.Q[x, w]) on X
  ---------------------------------------(括弧の付け替え)
   ∀y.([x, y].∀w.Q[w, y] on X×Y) on X
  ---------------------------------------(括弧の内側に対して全称変数wの自由化)
   ∀y.(Q[x, y] on X×Y) on X

この証明図が次の自明な証明図と同じ（束縛変数のリネームは無視！）であることを主張するのがニョロニョロ関係その1です。

   ∀w.Q[x, w] on X
  ------------------(何もしない)
   ∀w.Q[x, w] on X

同様に、(π^*・η);(ε・π^*) に対応する証明図は：

                 [x, y].P[x] on X×Y
  ------------------------------------(Pに対して無意味全称束縛)
   [x, y].(∀w:Y.[x, w].P[x]) on X×Y
  ------------------------------------(全称変数wの自由化)
   [x, y].P[x] on X×Y

この証明図も、ニョロニョロ関係その2から、次の自明な証明図と同じになります。

   [x, y].P[x] on X×Y
  ---------------------(何もしない)
   [x, y].P[x] on X×Y

おわりに

僕がこの記事を書いた動機は、ローヴェル流の限量随伴性（quantification adjunction）に付随するニョロニョロ関係式が、自然演繹風証明図の同値変形に対応することを紹介したかったからです。その割には、随伴などの圏論的概念と証明図との関係をあまり述べていません。この辺を述べると、現状の証明図の欠陥を指摘することになり、まーた自然演繹の悪口になります。

自然演繹の悪口は以前にも述べました。

上記の記事では命題論理しか扱ってないので、述語論理を含めた自然演繹の悪口（欠陥の指摘）の文脈で、ニョロニョロ計算の話をしたいと思っています。

*1:ここでの「非厳密」は正確さに欠けるということではありません。法則が等式としては成立しないことです。

*2:依存型（dependent type）の理論などでは、一般化限量子を考えるほうが整合的です。