「不動点方程式／不動点不等式と不動点オペレーター」において、タルスキーの最小プレ不動点定理を出しましたが、記述が間違っていたので訂正し、省いていた証明を記します。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\In}{\text{ in } }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Name}[1]{[#1] :\equiv }
\newcommand{\Ref}[1]{[#1]}
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
%`$
内容：
タルスキーの最小プレ不動点定理
「不動点方程式／不動点不等式と不動点オペレーター」において」
タルスキーの最小プレ不動点定理は、$`\cat{C} = {\bf Ord}`$ のセッティング（追加条件なし）において次の命題を主張しています。
- 最小プレ不動点は最小不動点に一致する。
もう少し詳しくいうと：
- $`f`$ の最小プレ不動点が存在すれば、それは $`f`$ の最小不動点でもある。
- $`f`$ の最小不動点が存在すれば、それは $`f`$ の最小プレ不動点でもある。
「最小プレ不動点は最小不動点に一致する」は表現が曖昧なので、「詳しくいうと」で2つの命題に分けたのですが、二番目のほうは間違いです。以下で次の3つのことを行います。
- 「$`f`$ の最小不動点が存在すれば、それは $`f`$ の最小プレ不動点でもある」の反例を出す。
- 「$`f`$ の最小プレ不動点が存在すれば、それは $`f`$ の最小不動点でもある」を証明する。
- 「最小プレ不動点は最小不動点に一致する」を再解釈する。
この記事全体を通して次を仮定します。
$`\quad X = (X, \le) \in |{\bf Ord}|\\
\quad f: X \to X \In {\bf Ord}
`$
順序集合 $`X`$ と単調写像 $`f`$ に特に条件は付けません。次の記号を使います。
$`\quad \mrm{FP}(f) := \{x\in X\mid f(x) = x\} = (f\: の不動点の集合)
\quad \mrm{PreFP}(f) := \{x\in X\mid f(x) \le x\} = (f\: のプレ不動点の集合)
`$
二番目の命題の反例
- 二番目の命題： $`f`$ の最小不動点が存在すれば、それは $`f`$ の最小プレ不動点でもある。（これは間違い）
$`{\bf R} = ({\bf R}, \le)`$ を、実数の集合に通常の順序を考えた順序集合とします。$`f:{\bf R}\to{\bf R}`$ を次のように定義します。
$`\For x\in {\bf R}\\
\quad f(x) := \text{if }x \ge 0 \text{ then }\frac{1}{2}x \text{ else } \frac{3}{2}x
%`$
次のことが言えます。
- $`f`$ は単調関数。
- $`f(x) = x \Iff x = 0`$
- すべての $`x\in {\bf R}`$ に対して $`f(x) \le x`$
言い換えると：
- $`\mrm{FP}(f) = \{0\}`$
- $`\mrm{PreFP}(f) = {\bf R}`$
$`f`$ の最小不動点 $`0`$ が存在するが、$`0`$ は $`f`$ の最小プレ不動点にはなってないので、二番目の命題は成立しません。
一番目の命題の証明
証明の流れを完全に追えるように、中間の命題にいちいち名前（ブラケットで囲った文言）を付けて参照することにします。
セットアップとターゲット命題の記述
定義や命題に名前を付けるときは ’$`:\equiv`$’ を使うことにします。次のように使います。
$`\Name{P\: の定義} P := \mrm{PreFP}(f)`$
これは、$`f`$ のプレ不動点の集合に $`P`$ という名前を付けています。その名付けの式に $`\Ref{P\: の定義}`$ という名前を付けたわけです。
$`P`$ が $`f`$ のプレ不動点の集合であることから次が言えます。
$`\Name{P\: の要素はプレ不動点} \forall x\in X.\, x \in P \Iff f(x) \le x`$
同様に次のように名付けします。
$`\Name{F\: の定義} F := \mrm{FP}(f)`$
$`\Name{F\: の要素は不動点} \forall x\in X.\, x \in F \Iff f(x) = x`$
順序集合の部分集合の最小元〈least element〉を（それが存在する状況において） $`\mrm{least}(-)`$ で記すことにします*1。
「ある要素がある部分集合の最小限である」ことを示す述語を定義しておきます。
$`\For A \subseteq X\\
\For y \in X\\
\quad \mrm{IsLeast}(y, A) :\Iff y \in A \land \forall x\in A. y \le x
`$
以上のセッティングで、一番目の命題をヒルベルトのイプシロン記号を使って書いてみます。イプシロン記号については次の過去記事参照。
命題をちゃんと書くとけっこう複雑です*2。
$`\Name{定理} (\exists y \in X.\, \mrm{IsLeast}(y, P)) \Imp
\mrm{IsLeast} (\varepsilon y\in X.\,\mrm{IsLeast}(y, P) , F)
`$
これを示しましょう。
証明
[追記]「証明のツリー構造も描いてみる」にツリーの絵があるので、それも参照すると分かりやすいと思います。[/追記]
まず簡単な補題を準備します。全称限量子は省略します。
$`\Name{補題\: 1} x \in P \Imp f(x) \in P
`$
$`x \in P`$ とすると、$`\Ref{P\: の要素はプレ不動点}`$ から
$`\quad f(x) \le x`$
単調関数 $`f`$ を適用すると
$`\quad f(f(x)) \le f(x)`$
これは $`f(x)`$ がプレ不動点であることだから
$`\quad f(x) \in P`$
$`P`$ の最小元の存在を仮定してそれに名前を付けます。
$`\Name{a\: の定義} a := \mrm{least}(P)
`$
この名付けから次が言えます。
$`\Name{a\: は\: P \: の要素} a\in P \\
\Name{a\: は最小元} \forall x\in X.\, x\in P \Imp a \le x
`$
$`\Ref{a\: は\: P \: の要素}`$ と $`\Ref{P\: の要素はプレ不動点}`$ から
$`\Name{不等式\: 1}f(a) \le a`$
一方、$`\Ref{a\: は\: P \: の要素}`$ と $`\Ref{補題\: 1}`$ から
$`\Name{f(a)\: は\:P\: の要素} f(a) \in P`$
$`\Ref{f(a)\: は\:P\: の要素}`$ と $`\Ref{a\: は最小元}`$ から
$`\Name{不等式\: 2} a \le f(a)`$
$`\Ref{不等式\: 1}`$ と $`\Ref{不等式\: 2}`$ から $`a = f(a)`$ が出て、
$`\Name{a\: は\:F\: の要素}a \in F`$
ここで、もうひとつ補題を挙げます（全称限量子は省略）。これは明らかでしょう。
$`\Name{補題\: 2} B\subseteq A \subseteq X \land l = \mrm{least}(A) \land l \in B \Imp l = \mrm{least}(B)`$
$`\Ref{a\:の定義}`$ と $`\Ref{a\: は\: F\: の要素}`$ と $`\Ref{補題\: 2}`$ から
$`\Name{結論} a = \mrm{least}(F)`$
最小プレ不動点ならば最小不動点
「最小プレ不動点は最小不動点に一致する」という表現は誤解をまねく可能性があるので、「最小プレ不動点があれば、それは最小不動点になる」とかのほうがいいですね。もっと短く言うなら「最小プレ不動点ならば最小不動点」
単調自己関数の不動点よりプレ不動点のほうが容易に見つかることがあります。例えば、順序集合に最大元があればそれはプレ不動点になっています。プレ不動点の集まりから最小のものを特定できれば、それが自動的に最小不動点になっているのは確かに便利です。
しかし、「不動点の集まりが分かっていて最小プレ不動点が欲しい」という状況は無さそうなので、二番目の命題が成立して欲しいと思う人はどうせいないでしょう。
