Теорема Кнастера — Тарского и её частный случай

[beroal]

Сначала формулировка теоремы. Пусть \(X\) — множество, \(\bigwedge\) — полная решётка на \(X\), \(f:X\to X\ \) монотонна относительно \(\bigwedge\). Тогда существует полная решётка \(\hat{\bigwedge}\) на множестве всех \(f\)-неподвижных точек.

В учебниках излагается частный случай теоремы. А именно, что существует наименьшая \(f\)-неподвижная точка. Я пытаюсь понять ту часть доказательства, где конструируется \(\hat{\bigwedge}\). Доказательство я взял из английской Википедии. Если кто-то знает лучшее, предлагайте.

Я застрял на таком месте. \([a, b] := \{x\in X | a\leq x\land x\leq b \} \). Надо доказать, что если \(a\leq b \), то \(\bigwedge\) — полная решётка на \([a, b]\). Пусть \(Y\subseteq [a, b] \). \(a\) — нижняя грань \(Y\). \(a\leq\bigwedge Y \) по свойствам инфимума. Как доказать, что \(\bigwedge Y\leq b \)?

Почему описываются именно неподвижные точки? Если в доказательстве вышеуказанного частного случая заменить «\(f\)-неподвижная точка» на «\(f\)-убывающая точка», доказательство становится даже проще. (\(x\) есть \(f\)-убывающая точка \(\leftrightarrow \) \(f(x)\leq x \).) Рассмотрим такой типичный частный случай. Если \(X\) — множество всех множеств суждений, и \(f\) сконструирована из consequence relation \(R\) на множестве всех суждений, то \(f\)-убывающая точка есть множество суждений, замкнутое относительно \(R\). \(f\)-неподвижная точка — это что-то другое. Можно ли переделать теорию под понятие «убывающая точка»?

[Xaositect]

beroal в сообщении #1243776 писал(а):

Я застрял на таком месте. $[a, b] := \{x\in X | a\leq x\land x\leq b \} $. Надо доказать, что если $a\leq b $, то $\bigwedge$ — полная решётка на $[a, b]$. Пусть $Y\subseteq [a, b] $. $a$ — нижняя грань $Y$. $a\leq\bigwedge Y $ по свойствам инфимума. Как доказать, что $\bigwedge Y\leq b $?

Тоже по свойствам инфинума, для любого $y \in Y$ имеем $\bigwedge Y \leq y \leq b$

[beroal]

А если \(Y=\emptyset\)? Тогда \(\bigwedge Y\) может быть вне интервала. Подозреваю, что я не прав, что \(\bigwedge\) — полная решётка на \([a, b]\). Нужна другая…

[Xaositect]

А это зависит от того, определяем мы решетку как частичный порядок или как алгебраическую структуру.
Ну, в $[a,b]$ есть максимальный и минимальный элемент, так что $\bigwedge \varnothing = b$. Это не то же самое $\bigwedge$, что в большой решетке. Но она порождается тем же порядком, что и в большой решетке, ограниченным на $[a,b]$.

[beroal]

Xaositect в сообщении #1244006 писал(а):

А это зависит от того, определяем мы решетку как частичный порядок или как алгебраическую структуру.

Я знаю только такие алгебраические структуры, где операции принимают список аргументов. А «большой» инфимум принимает множество аргументов, то есть оно может быть бесконечным. Будем говорить о частичном порядке. ☺ Мне кажется, что все подрешётки, которые фигурируют в этой теореме, имеют один и тот же порядок. К сожалению, в тексте это не сказано явно.

-- Thu Aug 31, 2017 10:20:39 --

Я думаю, что \(Y\mapsto \bigwedge(Y\cup\{b\})\) будет решёткой на \([a, b]\).

Чтобы рассматривать случаи, когда \(Y\) пусто или населено, нужна аксиома исключения третьего; мне это не нравится.

[Xaositect]

beroal в сообщении #1244044 писал(а):

Мне кажется, что все подрешётки, которые фигурируют в этой теореме, имеют один и тот же порядок. К сожалению, в тексте это не сказано явно.

Да, решетки вида $[a,b]$ и решетка неподвижных точек имеют тот же порядок, что и большая решетка.

[beroal]

Мне кажется, что доказательство в Википедии слишком мудрёное. Попробую доказать эту теорему с нуля.

Лемма 0. Пусть \(X\) — множество, \(\leq\) — полная решётка на \(X\), \(Y\subseteq X \). Пусть \(A\subseteq Y \). Если \(b\) — инфимум \(A\) и \(b\in Y \), то \(b\) — инфимум \(A\) в \(Y\).

Доказательство. \(A'\) — множество всех нижних граней \(A\) в \(Y\). \(b\in A' \) так как \(b\) — инфимум \(A\) и \(b\in Y \). [Пусть \(a'\in A' \). \(a'\) — нижняя грань \(A\); \(a'\leq b \), так как \(b\) — инфимум \(A\).] Следовательно, \(b\) — верхняя грань \(A'\). Следовательно, \(b\) — наибольший элемент \(A'\), другими словами, \(b\) — инфимум \(A\) в \(Y\). \(\square \)

Теорема 1. Пусть \(X\) — множество, \(\leq\) — полная решётка на \(X\), \(f:X\to X \) монотонна относительно \(\leq\). Пусть \(D\) — множество \(f\)-убывающих точек. Если \(e\) — инфимум \(D\), то \(e\) — инфимум \(D\) во множестве всех \(f\)-убывающих точек.

Доказательство. Пусть \(D'\) — множество всех нижних граней \(D\). [Пусть \(d'\in D' \). [Пусть \(d\in D \). \(d'\leq d \); \(f(d')\leq f(d) \), так как \(f\) монотонна; \(f(d')\leq d \), так как \(d\) \(f\)-убывающая.] Следовательно, \(f(d')\in D' \).] Следовательно, \(f\) сохраняет \(D'\). \(e\) — наибольший элемент \(D'\), так как \(e\) — инфимум \(D\). \(f(e)\in D' \) согласно доказанному ранее; \(f(e)\leq e \); \(e\) \(f\)-убывающая. \(e\) — инфимум \(D\) и \(f\)-убывающая; \(e\) — инфимум \(D\) во множестве всех \(f\)-убывающих точек согласно Лемме 0. \(\square \)

Согласно теореме 1, \(\leq \) — полная решётка на множестве всех \(f\)-убывающих точек. Следовательно, инфимум множества всех \(f\)-убывающих точек в нём же существует, и он есть наименьшая \(f\)-убывающая точка. В доказательствах не понадобилось никаких интервалов или головоломных трюков.