演繹系と閉包系

「演繹系とオペラッド」で演繹系について述べました。演繹系を、別な側面からさらに抽象化した構造として閉包系〈closure system〉があります。$`\newcommand{\Imp}{ \Rightarrow }
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\hyp}{\text{－}}
\newcommand{\Iff}{\Leftrightarrow}
`$

内容：

閉包作用素
閉包系
演繹系と閉包系

閉包作用素

プレ順序集合 $`(A, \le)`$ に対して、写像 $`f: A \to A`$ が閉包作用素〈closure operator〉だとは、$`a, b\in A`$ に対して次を満たすことです。

$`a \le b \Imp f(a) \le f(b)`$ （単調〈{monotone | monotonic}〉）
$`a \le f(a)`$ （増大的〈increasing〉）
$`f(f(a)) \le f(a)`$

この定義は、プレ順序集合をやせた圏とみなしてモナドの定義になっています。詳しくは以下の記事に書いてあります。

$`(A, \le)`$ が順序集合（反対称律を満たす）のときは、三番目の条件をイコールで書いてもかまいません。

$`f(f(a)) = f(a)`$ （ベキ等〈idempotent〉）

$`(A, \le)`$ を、べき集合に包含順序を入れた順序集合 $`(\mrm{Pow}(X), \subseteq)`$ に限定することもあります。Wikipedia項目 Closure operator の定義はそうなっています。つまり、閉包作用素 $`C: \mrm{Pow}(X) \to \mrm{Pow}(X)`$ とは、$`A, B\in \mrm{Pow}(X)`$ に対して次を満たすことです。

$`A\subseteq B \Imp C(A)\subseteq C(B)`$ （単調）
$`A \subseteq C(A)`$ （増大的）
$`C(C(A)) = C(A)`$ （ベキ等）

Wikipediaでは、単調性を increasing〈増大的〉、増大性を extensive〈広域的〉と呼んでいます。単調性・反単調性を monotone/antitone 、増大性・減少性を increasing/decreasing としたほうがバランスがいいと思います。

閉包系

集合 $`X`$ と、べき集合 $`\mrm{Pow}(X)`$ に作用する閉包作用素 $`C`$ を一緒にした構造 $`(X, C)`$ を閉包系〈closure system〉または閉包空間〈closure space〉と呼びます。ただし、いくつかの変種があるので、人名を付けてそれらを区別しましょう。

前節で述べた単調性／増大性／ベキ等性を持った作用素 $`C`$ を備えた $`(X, C)`$ をムーア閉包系〈Moore closure system〉と呼びます。

ムーア閉包系に次の条件を加えた構造はクラトフスキー閉包系〈Kuratowski closure system〉と呼びます。

$`C(\emptyset) = \emptyset`$ （ゼロ〈空集合〉を保存）
$`C(A\cup B) = C(A) \cup C(B)`$ （足し算〈合併〉を保存）

単調性は足し算〈合併〉を保存することから出るので冗長になりますが、冗長性に害はないので気にしないことにします。

クラトフスキー閉包系から、作用素 $`C`$ のベキ等性の条件を除いた構造はチェック閉包系〈Čech closure system〉です。

チェック閉包系を単に閉包空間〈closure space〉と呼ぶことがあるようです。一方で、閉包空間はクラトフスキー閉包系を意味することもあり、そのときチェック閉包系はプレ閉包空間〈preclosure space〉と呼ぶみたい。ちとややこしい。

クラトフスキー閉包空間 $`(X, C)`$ は、実は位相空間〈topological space〉です。適当な $`A\in \mrm{Pow}(X)`$ に対して $`C(A)`$ と書ける集合を“閉集合”と定義すると、閉集合族を持った集合（同じことだが開集合族を持った集合）となります。

$`(X, C)`$ がムーア閉包系のとき、クラトフスキー閉包空間＝位相空間の場合と同様に“閉集合”を定義すると、すべての閉集合の集合 $`\mathscr{C}`$ は次の性質を持ちます。

$`(A_i)_{i\in I}`$ が $`\forall i\in I.\, A_i \in \mathscr{C}`$ である集合族のとき、$`\bigcap_{i\in I}A_i \in \mathscr{C}`$ である。

この性質を持つ集合族をムーア族〈Moore collection〉と呼びます。ムーア閉包空間は、ムーア族を備えた集合としても定義できます。

ムーア族に関しては、nLab項目 Moore closure に記述があります。チェック閉包空間は、次の論文で扱っています。

Title: Model Checking Spatial Logics for Closure Spaces
Authors: Vincenzo Ciancia, Diego Latella, Michele Loreti, Mieke Massink
Submitted: 21 Sep 2016 (v1), 7 Oct 2016 (v2)
Pages: 51p
URL: https://arxiv.org/abs/1609.06513

インスティチューション〈institution〉は、論理の意味論〈モデル論〉を抽象化した構造です。論理の構文論〈証明論〉を抽象化した構造としてπ-インスティチューションがあります。π-インスティチューションについては、例えば次の論文など：

Title: Refinement by interpretation in π-institutions
Authors: César Rodrigues, Manuel A. Martins, Alexandre Madeira, Luis S. Barbosa
Submitted: 21 Jun 2011
Pages: 12p
URL: https://arxiv.org/abs/1106.4093

π-インスティチューションにおいて、推論や証明の機構は、閉包系によって定義されます。閉じた論理式に対応する論理文〈logical sentence〉の集合を $`S`$ として、閉包系〈ムーア閉包系〉 $`(S, C)`$ を考えます。$`C`$ は、$`\mrm{Pow}(S)`$ 上の単調・増大的・ベキ等な作用素です。

「演繹系とオペラッド」では、推論や証明の機構として演繹系について述べました。演繹系と閉包系はどう関係するのでしょう？実は、演繹系から閉包系を構成できます。

$`(S, R, \mrm{src}, \mrm{trg})`$ が演繹系（オペラッドの生成系）だとします。演繹系から生成されたオペラッド〈複圏〉を $`\cat{P}`$ とします。

項〈文〉のリストを $`\vec{s} \in \mrm{List}(S)`$ のように書くことにします。$`(\vec{s}, t) \in \mrm{List}(S)\times S`$ に対して、複ホムセット $`\cat{P}(\vec{s}, t)`$ が決まります（空集合のときもあります）。複ホムセットの要素は証明ツリーなので、次のようにも書きます。

$`\quad \mrm{Proof}(\vec{s}, t) := \cat{P}(\vec{s}, t)`$

リスト $`\vec{s}\in \mrm{List}(S)`$ に対して、リストに出現する文（$`S`$ の要素）の集合を $`|\vec{s}|`$ と書くことにします。$`|\vec{s}| \in \mrm{Pow}(S)`$ であり、次が成立します。

$`\quad |\vec{s}| = \emptyset \Iff \vec{s} = ()`$

これから、閉包作用素 $`C: \mrm{Pow}(S) \to \mrm{Pow}(S)`$ を構成しましょう。任意の部分集合 $`A \subseteq S`$ に対して、$`C(A)`$ は次のように定義します。

$`\quad t \in C(A) :\Iff \exists s\in \mrm{List}(S).\, |\vec{s}| \subseteq A \land \mrm{Proof}(\vec{s}, t) \ne \emptyset`$

$`\mrm{Proof}(\vec{s}, t) \ne \emptyset`$ を $`\vec{s} \vdash t`$ とも書くので、この書き方を使うと：

$`\quad t \in C(A) :\Iff \exists s\in \mrm{List}(S).\, |\vec{s}| \subseteq A \land \vec{s} \vdash t`$

おおざっぱに言えば、$`t \in C(A)`$ とは、$`A`$ の要素を有限個取った仮説〈仮定 | 前提〉から $`t`$ を証明できることです。

こうして定義した $`C: \mrm{Pow}(S) \to \mrm{Pow}(S)`$ が閉包作用素であるためには、次が成立する必要があります。

$`A \subseteq B \Imp C(A) \subseteq C(B)`$ （単調性）
$`A \subseteq C(A)`$ （増大性）
$`C(C(A)) = C(A)`$ （ベキ等性）

それぞれ次を意味します。

仮説を増やせば定理（仮説から証明される文）も増える。
仮説は定理（仮説から証明される文）である。
仮説からの定理を仮説とする定理は、もとの仮説からの定理である（新しい定理ではない）。

どれも、推論や証明として当たり前の性質です。演繹系（オペラッドの生成系）と閉包作用素 $`C`$ の定義に基づいて確認できます。