Деревья в теории множеств

[beroal]

Теорема Кнастера — Тарского нужна для индуктивных определений. Пример. Если засунуть в неё функцию \(\{\langle\{\}, \{0\}\rangle\} \cup \{\langle\{n\}, \{n+2\}\rangle|n\in\mathbb{N} \} \), то она докажет существование множества всех чётных натуральных чисел.

Я правильно понимаю, что с помощью этой теоремы нельзя доказать существование \(\mathbb{N}\)? (Разумеется, при условии, что аксиома о существовании \(\mathbb{N}\) удалена из теории множеств.) Как в теории множеств доказать, что существует множество всех Лисп-деревьев? (Лисп-дерево сконструировано из пар и элементов \(\mathbb{N}\).) Как доказать существование произвольного рекурсивного типа данных?

[george66]

В теории множеств есть аксиома бесконечности. Допустим, есть множество $A$, взаимно однозначно отобразимое на собственную часть. Это значит, есть функция $s\colon A\to A$ со свойством
$\forall a_1,a_2\in A(s(a_1)=s(a_2)\Rightarrow a_1=a_2)$
и элемент $0$, в который ничего не переходит
$\forall a\in A\neg(s(a)=0)$
Берём функцию $f\colon P(A)\to P(A)$, которая к любому подмножеству $B\subseteq A$ добавляет $0$ и $s[B]$
$f(B)=B\cup\{0\}\cup s[B]$
Наименьшая неподвижная точка этой функции будет множеством натуральных чисел. Без аксиомы бесконечности, конечно, ничего сделать нельзя. Множество деревьев можно строить аналогично: надо сначала найти множество, содержащее все натуральные числа и замкнутое относительно образования пары, а затем выделить из него наименьшее подмножество с такими свойствами. Но, если уже есть натуральные числа, можно проще. Полагаем
$A_0=\mathfrac{N}$
$A_1=A_0\cup (A_0\times A_0)$
$A_2=A_1\cup (A_1\times A_1)$
и так далее
$A=\cup_{i\in\mathfrac{N}}A_i$

[beroal]

Спасибо за ответ. Меня интересует, как это сделано, исходя из официальных аксиом теории множеств. Всё-таки теория множеств претендует на звание фундамента математики. Я не помню, чтобы ради деревьев вводили какие-то специальные аксиомы.

Официальная аксиома: \(\exists I(\emptyset\in I \land \forall x\in I(x\cup\{x\}\in I))\).

george66 в сообщении #1243792 писал(а):

Множество деревьев можно строить аналогично: надо сначала найти множество, содержащее все натуральные числа и замкнутое относительно образования пары

Так вот откуда его взять? Неужели оно есть подмножество \(\mathbb{N}\)? Каждое Лисп-дерево есть натуральное число?

[george66]

Тут надо хитрить, теория множеств для таких вещей плохо приспособлена. Например, множество наследственно конечных множеств содержит все натуральные числа и замкнуто относительно образования пары.

[arseniiv]

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

Как доказать существование произвольного рекурсивного типа данных?

Наверно, в теории типов, а не в теории множеств? И в некоторых теориях типов индуктивные типы вводятся определениями, и никто не жалуется.

george66 в сообщении #1244296 писал(а):

Тут надо хитрить, теория множеств для таких вещей плохо приспособлена.

По-моему, для определения произвольных индуктивных множеств всё давно придумано. Правда, прямо сейчас не вспомню последовательность действий.

-- Пт сен 01, 2017 17:45:33 --

Нужно всего-то показать, что для всех разумных $s, z$ объединение $C[z, s] = \bigcup_{n\in N} A_n$ существует, где $A_0 = z$, $A_{n+1} = s(A_0)$. Вот как теоретико-множественными средствами $\mathbb N$ выделяется как наименьшее множество, удовлетворяющее аксиоме бесконечности, примерно так же можно будет определить и $C[z, s]$.

-- Пт сен 01, 2017 17:52:48 --

Куратовский, Мостовский. Теория множеств, гл. III §2 Определения по индукции; теорема 1.

-- Пт сен 01, 2017 18:21:46 --

arseniiv в сообщении #1244304 писал(а):

Нужно всего-то показать, что для всех разумных $s, z$ объединение $C[z, s] = \bigcup_{n\in N} A_n$ существует, где $A_0 = z$, $A_{n+1} = s(A_0)$.

Дополню, если вдруг непонятно, как это связано с деревьями. Определим алфавит $\Sigma = \mathbb N\cup\{\mathsf{nil},\mathsf{cons}\}$, где двухэлементное множество $\{\mathsf{nil},\mathsf{cons}\}\not\subset\mathbb N$ (у нас уже должно существовать полно всякого). Существование $\Sigma^* = \bigcup_{n\in N}\Sigma^n$ тоже должно легко доказываться. Определим теперь конструкторы как операции на этом $\Sigma^*$: $\mathrm{nil}() = (\mathsf{nil})$, $\mathrm{cons}(t_1, t_2) = \mathrm{concat}((\mathsf{cons}),t_1,t_2)$, где $\mathrm{concat}\colon (\Sigma^*)^*\to \Sigma^*$ — функция сцепки последовательностей (в принципе, достаточно и бинарной, применённой два раза). Теперь у нас есть деревья, но у нас есть и куча мусора. Сейчас выделим только деревья.

Возьмём $A_0 = \varnothing$ и $A_{n+1} = \{\mathrm{nil}(a) : a\in A_n^0\}\cup\{\mathrm{cons}(a) : a\in A_n^2\}$. $A' = \bigcup_{n\in N} A_n$ — это наше множество деревьев, являющееся подмножеством $\Sigma^*$, про что можно смело забыть. Можно доказать, что ограничения $\mathrm{nil}$ и $\mathrm{cons}$ на $A'$ имеют и образом подмножество $A'$, так что вот нам конструкторы. Структурную индукцию тоже можно доказать, воспользовавшись, например, функцией глубины терма (высоты дерева) и сведя к обычной натуральночисленной, которая уже должна быть доказана.

Пришлось выдумывать $\Sigma^*$, чтобы определить «протоконструкторы», использованные для индуктивного определения $A'$, да. Можно ли определить всё без этого, не в курсе.

[arseniiv]

Кстати, я читал тему-читал, а когда стал писать, забыл. Вместо $\mathsf{nil}$ должны быть всевозможные натуральные числа и т. д..

Ещё одно дополнение: можно спросить, зачем было городить огород с $\Sigma^*$, если george66 уже предложил кандидат на такое множество, из которого можно выделить множество деревьев. Ответ в том, что аналогичное построение легко сделать для произвольного множества конструкторов без угадывания подходящего множества.

[beroal]

(Извиняюсь, что долго не отвечал. Ну, математика срочной не бывает. )

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

Каждое Лисп-дерево есть натуральное число?

Это я сказал, не подумав. Каждое натуральное число по фон Нейману содержит пустое множество. Все элементы каждой пары по Куратовскому населены. Так что эти понятия не совместимы.

george66 в сообщении #1244296 писал(а):

Тут надо хитрить, теория множеств для таких вещей плохо приспособлена. Например, множество наследственно конечных множеств содержит все натуральные числа и замкнуто относительно образования пары.

Можно уточнить, что такое «наследственно конечные множества»? Гугл не выдаёт ничего толкового. Наверное, есть другое название?

arseniiv в сообщении #1244304 писал(а):

Наверно, в теории типов, а не в теории множеств?

Именно в теории множеств.

arseniiv в сообщении #1244304 писал(а):

По-моему, для определения произвольных индуктивных множеств всё давно придумано.

Всё придумано для определения произвольных индуктивных подмножеств. Теорема Кнастера-Тарского. Индуктивное определение задаёт подмножество какого-то множества $X$. $X$ надо определить ранее. Да, если есть множество деревьев любого типа, из них можно выделять списки, кодировать деревья других типов…

arseniiv в сообщении #1244333 писал(а):

george66 уже предложил кандидат на такое множество

Не очень формальное определение. Чтобы определить $A_i$, нужна рекурсивная функция на множестве всех множеств?

[arseniiv]

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

Это я сказал, не подумав. Каждое натуральное число по фон Нейману содержит пустое множество. Все элементы каждой пары по Куратовскому населены. Так что эти понятия не совместимы.

Если вы о путанице, является ли множество натуральным числом или парой, то её в таком случае быть не должно: если $s$ — натуральное, то $\exists p.\, s = p\cup\{p\}$ и $p$ натуральное, а если $s$ — пара, то $\exists a,b.\; s = \{\{a\},\{a,b\}\}$. Значит, если оно и то, и то, оно есть $1 = \{\varnothing\}$ или $2 = \{\varnothing,\{\varnothing\}\}$ и не является парой.

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

Можно уточнить, что такое «наследственно конечные множества»? Гугл не выдаёт ничего толкового. Наверное, есть другое название?

Hereditarily finite set.

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

Не очень формальное определение. Чтобы определить $A_i$, нужна рекурсивная функция на множестве всех множеств?

Хм, ну раз все наследственно конечные множества составляют множество (счётное), то как-то выделить его в ZFC должно быть можно. Что-то мне не приходит в голову только. Однако это должно быть просто.

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

Индуктивное определение задаёт подмножество какого-то множества $X$. $X$ надо определить ранее. Да, если есть множество деревьев любого типа, из них можно выделять списки, кодировать деревья других типов…

В общем, на любой не обобщённый алгебраический тип данных должно хватить, если все его потенциальные аргументы уже представлены. На обобщённый — не думал.

[george66]

Наследственно конечные множества - это множества, которые сами конечны, их элементы конечны, элементы элементов конечны и т.д. Это наименьшее семейство множеств, содержащее $\emptyset$ и замкнутое относительно операции добавления элемента, которая по множествам $X,Y$ выдаёт $X\cup\{Y\}$
Подробно про них написано в книге Коэн "Континуум-гипотеза" (вводные главы)