Просьба. Учебник по теории множеств.

[george66]

Конструктивно не утверждение, а вся теория. Интуиционистская арифметика конструктивна. Если мы доказали в ней формулу вида $\exists n\varphi(n)$, то мы можем доказать $\varphi(N)$ для некоторого конкретного натурального числа $N$. Для классической арифметики это неверно. Берём формулу $\varphi$, не доказуемую и не опровержимую (такая есть по теореме Гёделя) и доказываем формулу $\exists n((\varphi\wedge n=0)\vee(\neg\varphi\wedge n=1))$ используя закон исключённого третьего $\varphi\vee\neg\varphi$ (если $\varphi$ истинно, такое число есть, это ноль, если $\neg\varphi$ истинно, тоже есть, это единица). При этом ни для какого конкретного числа $N$ мы не можем доказать $(\varphi\wedge N=0)\vee(\neg\varphi\wedge N=1)$ (подставьте вместо $N$ ноль и посмотрите, что выйдет, затем подставьте единицу и посмотрите). До сих пор понятно?

[Someone]

Z1X в сообщении #1215819 писал(а):

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

Существует довольно много направлений конструктивизма, в которых конструктивность понимается по-разному.

Изменения начинаются с математической логики. Например, отрицается закон исключённого третьего, что запрещает доказательства "от противного"; доказательство дизъюнкции должно должно однозначно указывать верный член дизъюнкции. Доказательство существования должно состоять в явном предъявлении объекта. Такое направление конструктивизма, как финитизм, разрешает использовать только конечные множества, причём, множество считается заданным только в том случае, когда все его элементы явно перечислены.

Подробнее нужно смотреть в соответствующей литературе. Можно посмотреть обзорную статью А. С. Трулстры "Аспекты конструктивной математики" (Справочная книга по математической логике. Часть IV. Теория доказательств и конструктивная математика. Москва, "Наука", 1983).
Советскому направлению конструктивной математики посвящена книга
Б. А. Кушнер. Лекции по конструктивному математическому анализу. "Наука", Москва, 1973.

Я сталкивался с забавным случаем. Некто опубликовал без доказательств три очень сильные теоремы (к сожалению, за давностью лет я не помню ни автора, ни самих теорем; автор был "забугорный"). На семинаре П. С. Александрова в связи с этим был доклад, который назывался примерно так: "По меньшей мере одна из трёх теорем … неверна". Докладчик выступал полтора часа и за это время, основываясь на этих трёх теоремах, построил противоречие. Доказательство было совершенно неконструктивным, ибо так и осталось неизвестным, которая из трёх теорем неверна. Поскольку обсуждавшиеся теоремы относились не к общей топологии, я не знаю, что там было дальше.

[Z1X]

Someone в сообщении #1215857 писал(а):

Доказательство существования должно состоять в явном предъявлении объекта.

Вот это, как мне кажется, самый спорный момент. Неясно, что подразумевается под "предъявлением" объекта. В соответствии со строгим формализмом (к которому в идеале сводится вся математика), непосредственно предъявить объект вообще нельзя, можно лишь аксиоматически описать его свойства, и иногда это описание получается однозначным, то есть существует доказательство единственности объекта. Например в ZFC доказывается существование и единственность пустого множества. Пустое множество — это конструктивный объект?

Someone в сообщении #1215857 писал(а):

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

Опять же возникают сложности с этим так называемым "перечислением". Перечисленные конечные элементы могут иметь сложную внутреннюю структуру, которую сложно или вообще невозможно описать без аксиом. А кроме того, эти элементы могут быть сами бесконечными. А с точки зрения алгебраических систем, структура вообще не важна, важна изоморфность. То есть легко может оказаться, что несколько изоморфных алгебраических систем конструктивно разные.

Спасибо за книжки, полистаю. Ну и спасибо, что подтвердили мою догадку: четкого понятия конструктивности не существует.

[Someone]

Z1X в сообщении #1215869 писал(а):

Опять же возникают сложности с этим так называемым "перечислением". Перечисленные конечные элементы могут иметь сложную внутреннюю структуру, которую сложно или вообще невозможно описать без аксиом. А кроме того, эти элементы могут быть сами бесконечными.

В финитизме — не могут. И если там есть какая-то внутренняя структура, то она конечная, и Вы обязаны предъявить её в явном виде.

[george66]

Пример неэффективного доказательства в ZF. Мы можем доказать, что любое множество можно вполне упорядочить. Теперь попробуйте придумать порядок на множестве действительных чисел, который его вполне упорядочивает. Задайте его какой-нибудь формулой. Подумайте несколько минут.

[arseniiv]

(Оффтоп)

Z1X в сообщении #1215869 писал(а):

Вот это, как мне кажется, самый спорный момент. Неясно, что подразумевается под "предъявлением" объекта.

Потому, наверно, направлений конструктивистских и не одно. Хотя я из всего спектра отношений к конструктивности слышал только о классической и интуиционистской логике (+ теории типов). Если рассматривать теории типов, правила вывода перечисляют все возможные способы получать значения каких-то типов из значений каких-то других типов (в том числе из пустых наборов значений, как, например, правило вывода $\dfrac{}{*:1}$ для единичного типа), и правила образования могут аккомпанироваться правилами вычисления, придающим «конструктивность». Например, возьмём теорию типов Мартина-Лёфа (не важно какую) с типом-суммой и добавим правило $\dfrac{}{\mathsf{lem} : \Pi(A:\mathcal U).\, A+\neg A}$. Правило для вычисления $\mathsf{lem}(T)$ для произвольного $T$ мы тут никакое сочинить не сможем, но это не помешает нам строить значения с использованием $\mathsf{lem}$ — мы сможем в каком-то смысле «предъявлять» «неконструктивно».

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

[Someone]

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

Хотя я из всего спектра отношений к конструктивности слышал только о классической и интуиционистской логике (+ теории типов).

На интуиционистской логике "сидит" не одно конструктивистское направление. Например, собственно интуиционизм и конструктивный рекурсивный анализ (советское направление конструктивизма). И, насколько мне известно, ещё некоторые.

[arseniiv]

Хм, а я уж решил, что с интерпретацией конструктивности в ней всё однозначно. Ясно.

[Someone]

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

Пример неэффективного доказательства в ZF. Мы можем доказать, что любое множество можно вполне упорядочить.

В ZF не можем. В ZFC можем.

За примером неконструктивности не надо далеко ходить. Если мы в доказательстве говорим "возьмём любое $c\in(a,b)$", не указывая никакого конкретного $c$, то наше доказательство заведомо не конструктивно. Но мы можем сказать "пусть $c=0{,}7a+0{,}3b$", тогда в этом месте наше рассуждение будет конструктивным.

Z1X в сообщении #1215704 писал(а):

Не ZF(C) сформулирована, а модель построена в X; ZF(C) формулируется чисто синтаксически, независимо от семантики.

Вы не правы. Для формулировки формальной теории нужна метатеория. В этой метатеории определяются алфавит, термы, формулы, задаются аксиомы, определяется понятие доказательства и доказываются метатеоремы (например, о доказуемости или недоказуемости какой-нибудь формулы). Кроме того, в ней же можно строить модели формальной теории. В каких-то случаях может потребоваться мета-метатеория. В качестве метатеории чаще всего используется естественный язык, но при нужде можно взять и какую-нибудь формализованную теорию.

Someone в сообщении #1215716 писал(а):

метамножество всех множеств ZFC не является множеством всех множеств в самой ZFC, даже если вследствие какой-то причуды модели оно принадлежит этой модели. Один и тот же объект в ZFC и в X может играть совершенно разную роль.

Я несколько разовью этот тезис, показав пример, когда отношение $\in$ в метатеории не совпадает с отношением $\in$ в построенной с её помощью модели.

В качестве метатеории X мы возьмём ZFC. В ней натуральный ряд (с нулём; кто не хочет считать ноль натуральным числом, может называть это множество первым бесконечным ординалом) определяется как наименьшее индуктивное множество. Аксиомы Пеано для этого множества являются теоремами ZFC. В этой модели натуральные числа являются множествами: $0=\varnothing$, $1=\{0\}=\{\varnothing\}$, $2=\{0,1\}=\{\varnothing,\{\varnothing\}\}$, $3=\{0,1,2\}=\{\varnothing,\{\varnothing\},\{\varnothing,\{\varnothing\}\}\}$,
$4=\{0,1,2,3\}=\{\varnothing,\{\varnothing\},\{\varnothing,\{\varnothing\}\},\{\varnothing,\{\varnothing\},\{\varnothing,\{\varnothing\}\}\}\}$,…; следующие натуральные числа определяются индуктивно формулой $n'=n\cup\{n\}$. Мы не будем рассматривать эту арифметику как отдельную теорию, будем считать её просто частью метатеории X, язык которой пополнен символами для арифметических операций и соответствующими правилами для образования арифметических формул.

Теперь, используя натуральные числа, мы построим модель теории наследственно конечных множеств, которая есть ZFC, в которой аксиома бесконечности заменена её отрицанием. Элементы этой модели являются определёнными выше натуральными числами. Связь между числами и изображаемыми ими множествами определяем так:
1) $\varnothing=0$;
2) если $n_1$, $n_2$, $n_3$,…, $n_k$ попарно различны, то $\{n_1,n_2,n_3,\ldots,n_k\}=2^{n_1}+2^{n_2}+2^{n_3}+\ldots+2^{n_k}$.
Тогда $\{\varnothing\}=\{0\}=2^0=1$, $\{\{\varnothing\}\}=\{1\}=2^1=2$, $\{\varnothing,\{\varnothing\}\}=\{0,1\}=2^0+2^1=3$, $\{\{\{\varnothing\}\}\}=\{2\}=2^2=4$, $\{\varnothing,\{\{\varnothing\}\}\}=\{0,2\}=2^0+2^2=5$,…

Сравнивая написанные равенства в метатеории X и в теории наследственно конечных множеств, видим, что, например, в первом случае символ $2$ обозначает множество с двумя элементами $0$ и $1$, а во втором — множество с одним элементом $1$, хотя с точки зрения метатеории $2$ — один и тот же объект в обоих случаях. По-хорошему, во второй теории следовало бы использовать другие символы для обозначения отношения принадлежности и для образования множеств.

Примечание. Теория наследственно конечных множеств встречается в книге П. Дж. Коэна "Теория множеств и континуум-гипотеза" (глава I, § 6, теория $Z_2$), где утверждается, что эта теория эквивалентна арифметике Пеано. Я не знаю, доказуема ли схема аксиом индукции в ZFC с отрицанием аксиомы бесконечности, но Коэн формулирует эту схему в явном виде.

-- Сб май 13, 2017 01:47:41 --

Нашёл статью, где этот вопрос проясняется. Действительно нужна дополнительная аксиома.

[arseniiv]

О, спасибо, полезна будет. Когда-то интересовался наследственно конечными множествами.