ここでのタルスキーの定理は、不動点に関するタルスキーの定理です。不動点関連でも次のような「タルスキーの定理」があります。
- 最小プレ不動点と最小不動点の関係を述べた定理
- 最小不動点の存在定理
- 不動点集合の性質に関する定理
「最小プレ不動点ならば最小不動点」であることは「タルスキーの最小プレ不動点定理(訂正)」で詳しく述べました。この最小プレ不動点定理を使って、適当な条件のもとでの最小不動点の存在定理を示してみます。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\Name}[1]{[#1] :\equiv }
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Iff}{\Leftrightarrow }
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
`$
内容:
ミート半束
$`X = (X, \le)`$ を順序集合とします。$`a, b \in X`$ に対して、$`m\in X`$ が $`a, b`$ のミート〈meet〉であるとは次のことです。
- $`m \le a \land m \le b`$ (どっちと比べても小さい)
- $`\forall x\in X.(\, x \le a \land x \le b \Imp x \le m \,)`$ (小さいなかでは最大)
ミートがいつでも存在するとは限りませんが、存在するなら一意的です。「$`m\in X`$ が $`a, b`$ のミートである」ことを $`\mrm{IsMeet}(m, a, b)`$ と書くと、次の一意性が成立します。
$`\quad \forall a, b, x, y\in X.(\, \mrm{IsMeet}(x, a, b)\land \mrm{IsMeet}(y, a, b) \Imp x = y
\,)
%`$
どんなペア $`(a, b)`$ に対してもミートが存在する順序集合はミート半束〈meet semilattice〉と呼びます*1。ミートは一意的に存在するので、次のような二項演算が定義できます。(ヒルベルトのイプシロン記号を使っています。)
$`\For a, b\in X\\
\quad a \wedge b := \varepsilon x\in X.\, \mrm{IsMeet}(x, a, b)
`$
こうして定義した二項演算は次の法則を満たします。
- $`(a \wedge b) \wedge c = a \wedge (b \wedge c)`$
- $`a \wedge b = b \wedge a`$
- $`a \wedge a = a`$
これは、ベキ等可換半群〈idempotent commutative semigroup〉の公理になっています。逆に、ベキ等可換半群があるとき、以下のように定義した順序によりミート半束が構成できます(確認してみてください)。
$`\quad a \le b :\Iff a \wedge b = a`$
有限個(ゼロ個は除く)の要素に対するミートも定義できます。もし最大元があれば、0個の要素のミートも最大元として定義できます(次々節で説明しています)。
自然数の集合 $`{\bf N}`$ に普通の大小順序を考えると、$`n \wedge m = \mrm{min}(n, m)`$ としてミート半束になります。最大元はないので0個のミートは定義できません。同じ自然数の集合を約数倍数の順序で考えると、$`n \wedge m = \mrm{gcd}(n, m)`$ (最大公約数)としてミート半束になります。自然数 $`0`$ が0個のミートです。
ミート完備な順序集合
ミート半束では有限部分集合のミートしか定義できませんが、もっと強い条件として、任意の部分集合のミート(下限〈infimum | greatest lower bound〉ともいう)を要求しましょう。下限であることの定義は次です。
$`\For A \subseteq X\\
\For a \in X\\
\quad \mrm{IsInf}(a, A) :\Iff
(\forall x\in A. a \le x) \land
\forall y\in X.(\, (\forall x\in A.\, y \le x) \Imp y \le a \,)
%`$
任意の部分集合に下限が在るという条件は次のように書けます。以下の $`\mrm{Pow}`$ はベキ集合です。
$`\quad \forall A\in \mrm{Pow}(X). \exists a\in X.\mrm{IsInf}(a, A)
%`$
この条件を満たす順序集合をミート完備〈meet complete〉と形容することにします。下限を、無限(も許す)ミートと解釈します。完備ミート半束〈complete meet semilattice〉と呼んでもいいでしょう。
下限が存在するなら一意的なので、次のように書くことにします。(ここでもヒルベルトのイプシロンを使っています。)
$`\For A \subseteq X\\
\quad \mrm{inf}(A) = \bigwedge(A) := \varepsilon a\in X.\mrm{IsInf}(a, A)
`$
つまり、$`X = (X, \le)`$ がミート完備なら次の写像が定義できることになります。
$`\quad \mrm{inf} = \bigwedge : \mrm{Pow}(X) \to X`$
任意の集合のベキ集合は、包含順序 $`\subseteq`$ でミート完備な順序集合になります。自然数の集合に約数倍数の順序もミート完備です。実数の閉区間 $`[0, 1]\subseteq {\bf R}`$ もミート完備です。
最大元と最小元
最初の節で、「0個の要素のミートは最大元」と言いましたが、違和感を感じる人もいるようです。このことを「雰囲気」として理解するには以下のように考えます;
ミート半束で幾つかの要素 $`a_1, a_2, \cdots, a_n`$ のミート $`m`$ を考えます。$`m`$ は、$`a_1, a_2, \cdots, a_n`$ 達に上から抑えられていますが、上に昇りたがっていると想定します(あくまで「雰囲気」)。上にいる要素を減らしていきます。そのときミート $`m`$ は、条件が外されていくので(「雰囲気」としては)だんだん上にいくでしょう。すべての要素を取り除くと、一切の条件が外されて $`m`$ は行けるところまで大きくなるので最大元になります。
論理式の論理的操作によっても $`\inf(\emptyset) = \top`$ ($`\top`$ は最大元)は示せます。やってみましょう;
$`\inf(A) = m`$ であることは次の2つの条件で書けます。
- $`\forall x\in A. m \le x`$ (どれよりも小さい)
- $`\forall y\in X.(\, (\forall x\in A. y \le x) \Imp y \le m \,)`$ (小さいなかでは最大)
これは次のようにも書けます。
- $`\forall x\in X.(\, x\in A \Imp m \le x \,)`$
- $`\forall y\in X.(\, (\forall x\in X.(\, x \in A \Imp y \le x\,) ) \Imp y \le m \,)`$
$`m`$ が空集合のミート〈下限〉である条件は、$`A = \emptyset`$ と置けばいいので次のようになります。
- $`\forall x\in X.(\, x\in \emptyset \Imp m \le x \,)`$
- $`\forall y\in X.(\, (\forall x\in X.(\, x \in \emptyset \Imp y \le x\,) ) \Imp y \le m \,)`$
$`x\in \emptyset`$ という命題は偽になり、偽が前件となる含意(「$`\mrm{False} \Imp P`$」という命題)は真になります。したがって、一番の条件は真となり、ニ番の条件は次のように書き換えられます。
- $`\forall y\in X.(\, \mrm{True} \Imp y \le m \,)`$
さらに書き換えて:
- $`\forall y\in X. y \le m`$
これは $`m`$ が $`X`$ の最大元であることに他なりません。
双対的に「すべての要素のミートは最小元」です。$`\mrm{inf}(X) = \bot`$ ($`\bot`$ は最小元)と書けます。これは感覚的にも論理的にも納得のいくことだと思います。
ミート完備順序集合の不動点定理
順序集合 $`(X, \le)`$ と単調自己関数 $`f:X \to X`$ を勝手に選んだとき、プレ不動点や不動点の存在は全然保証されません。不動点の存在定理を示すには何らかの条件を課す必要があります。ここでは、順序集合がミート完備だという条件のもとで最小不動点の存在定理を示してみます。
単調自己関数 $`f`$ のプレ不動点の集合を次のように定義します。
$`\quad \mrm{PreFP}(f) := \{x\in X\mid f(x) \le x\}`$
ミート完備な順序集合 $`X`$ には最大元 $`\top`$ があるので、$`\mrm{PreFP}(f)`$ は空集合ではありません。
ミート完備性により、集合 $`\mrm{PreFP}(f) \subseteq X`$ にはミート〈下限〉が存在するので、それを $`m`$ とします。
$`\quad m := \mrm{inf}(\mrm{PreFP}(f))`$
一般には、下限がもとの部分集合に入るとは限りませんが、$`m \in \mrm{inf}(\mrm{PreFP}(f))`$ は言えます。なぜなら:
任意の $`x\in \mrm{PreFP}`$ に対して
$`\quad m \le x`$
は成立する。$`f`$ は単調だから
$`\quad f(m) \le f(x)`$
一方、 $`x\in \mrm{PreFP}`$ であることから
$`\quad f(x) \le x`$
上の2つの不等式から、任意の $`x\in \mrm{PreFP}`$ に対して $`f(m) \le x`$ 、つまり
$`\quad \forall x\in \mrm{PreFP}(f). f(m) \le x`$
$`m`$ は $`\mrm{PreFP}`$ の下限だったので、
$`\quad f(m) \le m`$
これは、$`m \in \mrm{PreFP}(f)`$ を意味する。
ミート〈下限〉 $`m`$ は、$`\mrm{PreFP}`$ の最小元になっています。
ここで、タルスキーの最小プレ不動点定理を思い出します。
- 最小プレ不動点があれば、それは最小不動点になる
ミート完備の条件のもとでは最小プレ不動点があるので、最小不動点もあります。
例えば、実数の閉区間 $`[0, 1]`$ は(普通の順序で)ミート完備になるので、単調関数 $`f:[0, 1]\to [0, 1]`$ には不動点が存在します。不動点のなかで最小なものも決まります。
*1:ミート半束の定義として、最大元の存在を要求する場合もあります。