Абстракция актуальной бесконечности

[Someone]

epros в сообщении #196833 писал(а):

Так я не понял, каков ответ? Для любой совокупности натуральных чисел любое натуральное число будет "своим" или нет?

"Своим" будет только то, которое этой совокупности принадлежит (является её элементом). По-моему, я это прошлый раз написал. У разных совокупностей разные "свои" элементы.

epros в сообщении #196833 писал(а):

Я дал определение "такому понятию". Можете "считать" вместе со "всеми остальными" про конечные и бесконечные множества всё, что угодно, но это не имеет никакого отношения к вопросу о том, что я имею в виду, когда употребляю термин "актуальная бесконечность".

То есть, это Ваше собственное изобретение. Вопрос исчерпан. Такое "понимание" "актуальной бесконечности" - это Ваша собственная проблема, к математике отношения не имеющая.

epros в сообщении #196833 писал(а):

А я Вам о чём твержу? О том, что типы не являются объектами предметной теории, ибо определяются свойствами, а не предметными переменными или константами. Поэтому в предметной теории не может быть утверждения о "существовании" типа или о наличии у него каких либо свойств (например, свойства "конечности").

Ладно, цитируем учебник (Введение, пункт 7). Цитату с определениями различных свойств у "несуществующих" типов я уже приводил: http://dxdy.ru/post196244.html#196244.

Б.А.Кушнер писал(а):

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

Б.А.Кушнер писал(а):

Строгое использование множеств предполагает фиксацию формализованного логико-математического языка (см., например, Шанин [4]), средствами которого формулируются свойства (под свойствами понимаются однопараметрические формулы данного языка). При этом сами множества оказываются конструктивными объектами (словами в некотором алфавите) и, в частности, могут выступать в качестве исходных данных алгорифмов.

Б.А.Кушнер писал(а):

Мы будем использовать обычные теоретико-множественные обозначения. ...

(Здесь объясняется, как определяется подмножество, объединение, пересечение, дополнение, произведение множеств.)

Нормальным называется множество, задаваемое нормальной формулой с одной свободной переменной, то есть, формулой, не содержащей квантора существования и дизъюнкции.

Б.А.Кушнер писал(а):

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

Вы по-прежнему будете утверждать, что множество натуральных чисел $\mathscr H$ в конструктивном анализе не существует и не является объектом теории? Или что оно, вопреки своему определению, содержит не все натуральные числа?

Alexey Romanov в сообщении #196980 писал(а):

А с аксиомой выбора появляются такие странные объекты, как множества, неизмеримые по Лебегу.

Ага. Только отсутствие аксиомы выбора не означает автоматически отсутствие неизмеримых множеств. А совсем без аксиомы выбора континуум может оказаться объединением счётного множества счётных множеств. И где тогда у нас будет мера Лебега?

Alexey Romanov в сообщении #196980 писал(а):

В теории типов (о которой epros говорит) $x \in A$ даже не является высказыванием.

epros ничего не говорит ни о какой теории типов. Он просто называет множества типами. И $x\in\mathscr A$ в конструктивном анализе прекрасно является высказыванием. Откройте книжку Кушнера и посмотрите.
Я также говорю не о теории типов, а о теории множеств ZFC. О том, что множества ZFC можно интерпретировать как ограниченные свойства. И не требовать, чтобы все элементы множества "существовали одновременно" (я не понимаю, как можно было бы сформулировать в ZFC или в конструктивном анализе, что элементы множества "существуют" "одновременно" или "не одновременно").

epros в сообщении #196833 писал(а):

Так давайте договоримся об определениях. Я понимаю конечность, очевидно, таким же образом, как "финитность" у Кушнера. Тип является конечным, если есть алгоритм, который перечисляет все объекты данного типа и завершается.

Я об этом уже говорил. Определение финитного множества процитировано здесь: http://dxdy.ru/post196244.html#196244. Я понял причину разногласий, этого мне достаточно.

[Alexey Romanov]

Цитата:

Alexey Romanov в сообщении #196980 писал(а):

А с аксиомой выбора появляются такие странные объекты, как множества, неизмеримые по Лебегу.

Ага. Только отсутствие аксиомы выбора не означает автоматически отсутствие неизмеримых множеств. А совсем без аксиомы выбора континуум может оказаться объединением счётного множества счётных множеств. И где тогда у нас будет мера Лебега?

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

Цитата:

Alexey Romanov в сообщении #196980 писал(а):

В теории типов (о которой epros говорит) $x \in A$ даже не является высказыванием.

epros ничего не говорит ни о какой теории типов. Он просто называет множества типами. И $x\in\mathscr A$ в конструктивном анализе прекрасно является высказыванием. Откройте книжку Кушнера и посмотрите.

Дело в том, что конструктивную математику можно строить на основании теории множеств, а можно -- на основании теории типов. Точно так же и классическую математику можно строить на основании $ZFC$, а можно на основании $HOL$. (А ещё есть и другие теории множеств и теория категорий, которые тоже можно использовать как основание).

Кушнер использовал теорию множеств. Бишоп -- тоже. Это неудивительно хотя бы потому, что оба учебника были написаны до развития теории типов.

Цитата:

Я также говорю не о теории типов, а о теории множеств ZFC. О том, что множества ZFC можно интерпретировать как ограниченные свойства.

Как тогда обосновать аксиомы

1) существования множества всех подмножеств;

2) выделения (для произвольных свойств);

3) основания;

4) выбора?

[epros]

Alexey Romanov писал(а):

Если среди аксиом теории есть утверждение, что у Маши есть возраст. Но (если возраст Маши -- натуральное число) тогда в конструктивной логике это тоже выводится!

Я перечислил четыре аксиомы:
A) Маша старше 20-ти лет.
B) Маша не старше 30-ти лет.
C) Если Маша старше 25-ти лет, значит она вышла замуж за Васю.
D) Если Маша не старше 25-ти лет, значит она вышла замуж за Колю.

Аксиомы A) и B) можно записать так, что они будут означать "существование" возраста Маши в виде числа больше 20-ти и не больше 30-ти. Но это будет означать, что эти аксиомы сами по себе неконструктивны, поскольку способа вычислить конкретное число теория не даёт.

[Alexey Romanov]

epros писал(а):

Alexey Romanov писал(а):

Если среди аксиом теории есть утверждение, что у Маши есть возраст. Но (если возраст Маши -- натуральное число) тогда в конструктивной логике это тоже выводится!

Я перечислил четыре аксиомы:
A) Маша старше 20-ти лет.
B) Маша не старше 30-ти лет.
C) Если Маша старше 25-ти лет, значит она вышла замуж за Васю.
D) Если Маша не старше 25-ти лет, значит она вышла замуж за Колю.

Аксиомы A) и B) можно записать так, что они будут означать "существование" возраста Маши в виде числа больше 20-ти и не больше 30-ти. Но это будет означать, что эти аксиомы сами по себе неконструктивны, поскольку способа вычислить конкретное число теория не даёт.

Вот именно. Если записать эти аксиомы в таком виде, то и в классической и в конструктивной логике мы можем из них вывести, что у Маши есть муж.

Так что я не вижу никакого конструктивного понимания этих аксиом, при котором конструктивист 1) может их принять 2) может из них вывести, что неверно, что у Маши нет мужа 3) не может из них вывести, что у Маши есть муж.

И соответственно, в качестве примера неснимаемого двойного отрицания это не годится.

[epros]

Someone писал(а):

Такое "понимание" "актуальной бесконечности" - это Ваша собственная проблема, к математике отношения не имеющая.

То, что Вы не понимаете какое отношение имеет сформулированное определение понятия к математике, это уже Ваша проблема.

Someone писал(а):

Вы по-прежнему будете утверждать, что множество натуральных чисел $\mathscr H$ в конструктивном анализе не существует и не является объектом теории? Или что оно, вопреки своему определению, содержит не все натуральные числа?

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

Someone, я же Вам уже всё объяснил про "существование" $\mathscr{H}$ в конструктивном анализе, только не говорите мне, что Вы ни черта не поняли. Утверждение о существовании $\mathscr{H}$ является мета-теоретическим, а не относящимся к предметной теории. Вы же вроде бы сами где-то говорили о том, что не надо путать мета-теоретические утверждения с предметными. Мета-теория занимается только правилами написания буковок в предметной теории, поэтому она может сказать, что количество объектов предметной теории, которые обладают свойством $\mathscr{H}$, не является конечным. Но она ничего не может утверждать о существовании такого "объекта" предметной теории, как $\mathscr{H}$.

А ZFC утверждает существование такого объекта в том же самом смысле, с котором утверждается существование пустого множества или множества из одного элемента. Чувствуете разницу?

Someone писал(а):

epros ничего не говорит ни о какой теории типов. Он просто называет множества типами.

Я называю множества, которые в силу их конечности могут существовать в предметном мире, "совокупностями". А типами я называю объекты совсем другого логического уровня, которые назызваны "множествами" у Кушнера (и я полагаю, что названы неудачно).

Someone писал(а):

я не понимаю, как можно было бы сформулировать в ZFC или в конструктивном анализе, что элементы множества "существуют" "одновременно" или "не одновременно"

А вот так:
$\exists x (x = \emptyset) \wedge \exists y (y = \omega_0)$

Понятное дело, что "одновременно" здесь никакого отношения ко "времени" не имеет.

Добавлено спустя 25 минут 6 секунд:

Alexey Romanov писал(а):

epros писал(а):

Я перечислил четыре аксиомы:
A) Маша старше 20-ти лет.
B) Маша не старше 30-ти лет.
C) Если Маша старше 25-ти лет, значит она вышла замуж за Васю.
D) Если Маша не старше 25-ти лет, значит она вышла замуж за Колю.

Аксиомы A) и B) можно записать так, что они будут означать "существование" возраста Маши в виде числа больше 20-ти и не больше 30-ти. Но это будет означать, что эти аксиомы сами по себе неконструктивны, поскольку способа вычислить конкретное число теория не даёт.

Вот именно. Если записать эти аксиомы в таком виде, то и в классической и в конструктивной логике мы можем из них вывести, что у Маши есть муж.

Так что я не вижу никакого конструктивного понимания этих аксиом, при котором конструктивист 1) может их принять 2) может из них вывести, что неверно, что у Маши нет мужа 3) не может из них вывести, что у Маши есть муж.

И соответственно, в качестве примера неснимаемого двойного отрицания это не годится.

Придумать такой детсадовский пример двойного отрицания было несколько затруднительно, но я не согласен, что он так уж "не годится".

Во-первых, две первые аксиомы я добавил только для того, чтобы привести примеры доказуемых и опровержимых утверждений в той же теории. Для вывода о невозможности несуществования у Маши мужа они не нужны.

Во-вторых, формулировки "старше стольки-то" и "не старше стольки-то" совсем не обязательно интерпретировать как утверждения о возрасте, измеряемом натуральным количеством лет (и, соответственно, привешивать к этой теории арифметику Пеано). Это Nxx заговорил о "возрасте", а мне такое понятие для вывода о невозможности несуществования у Маши мужа не требуется. Мне достаточно того, что высказывание "Маша не старше 25-ти лет" является отрицанием высказывания "Маша старше 25-ти лет".

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

[Alexey Romanov]

Цитата:

я не понимаю, как можно было бы сформулировать в ZFC или в конструктивном анализе, что элементы множества "существуют" "одновременно" или "не одновременно"

В $ZFC$ существует кумулятивная иерархия:

$V_0 = \varnothing;$

$V_{\alpha+1} = \mathcal P(V_\alpha);$ для любого ординала $\alpha$.

$V_\beta = \bigcup_{\alpha < \beta} V_\alpha$ для любого предельного ординала $\beta$.

Тогда $V_\omega$ содержит все натуральные числа фон Неймана, a $V_{\omega+1}$ содержит $\omega$. Кроме того мы можем доказать, что $\bigcup_\alpha V_\alpha = U$, где $U$ -- собственный класс всех множеств.

Поэтому мы можем представить, что все множества можно построить, начиная с пустого множества и применяя трансфинитное количество раз операцию $\mathcal P$ (а потом один раз взять элемент) -- сначала $V_1$, потом $V_2$ и т.д., потом $V_{\omega+1}$... Таким образом, мы можем представить, что "сначала" (в некотором смысле) существовали натуральные числа, а "потом" их собрали в множество $\omega$. См., например, книгу Шенфилда "Математическая логика", где вся теория множеств строится с этой позиции.

Конструктивно этой иерархии не существует. В частности, не получится доказать существование $V_{\omega+1}$ и поэтому утверждение, которое в $ZFC$ обозначает $\omega \in V_{\omega+1}$ тоже нельзя доказать.

[Nxx]

Какой смысл делать выводы из бессмысленных аксиом? Если у Маши нет возраста, то и высказывание "Маша старше 25-ти лет" бессмысленно, как и утверждение, что

$$\lim_{x\to\infty} \sin x <2$$

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

Правда аксиома, утверждающая, что возраст у Маши есть, без указания, где его брать, делает систему аксиом противоречивой. Вот если аксиома звучит так "возраст у Маши есть и он записан у нее в паспорте", то без сомнения, и муж у Маши есть (и тоже записан в паспорте, хе-хе).

[Alexey Romanov]

Цитата:

Мне достаточно того, что высказывание "Маша не старше 25-ти лет" является отрицанием высказывания "Маша старше 25-ти лет".

Слона-то я и не приметил! Тогда я снимаю возражение, из этого действительно следует то, что надо, без всяких утверждений о возрасте.

Добавлено спустя 13 минут 38 секунд:

Nxx писал(а):

Какой смысл делать выводы из бессмысленных аксиом? Если у Маши нет возраста, то и высказывание "Маша старше 25-ти лет" бессмысленно, как и утверждение, что

$$\lim_{x\to\infty} \sin x <2$$

, потому что предела этого нет.

Вообще-то

$$\lim_{x\to\infty} \sin x <2$$

понимается обычно как сокращение $\exists y ~ y = \lim_{x\to\infty} \sin x \land y < 2$. Так что оно не бессмысленно, а ложно.

Что Вы думаете насчёт утверждения $\lim_{x\to\infty} \sin x <2 \to \lim_{x\to\infty} \sin x <2$? Оно тоже бессмысленно?

[Nxx]

Согласен, оно ложно, если подразумевается ваш квантор. Также ложно и высказывание, что у Маши есть возраст, поскольку возраста у нее нет. Значит, система аксиом внутренне противоречива.

[ewert]

Alexey Romanov писал(а):

Что Вы думаете насчёт утверждения $\lim_{x\to\infty} \sin x <2 \to \lim_{x\to\infty} \sin x <2$? Оно тоже бессмысленно?

Конечно бессмысленнр -- стрелочка неправильная.

Nxx в сообщении #197400 писал(а):

, нужно по крайней мере, чтобы этот предел существовал.

Не нужно. Утверждение "из А следует А" верно независимо от истинности или ложности самого А.

[Nxx]

Цитата:

Не нужно. Утверждение "из А следует А" верно независимо от истинности или ложности самого А.

Если само А имеет смысл.

Верно ли, что

$$x^2 \ge 0$$

независимо от наличия или отсутствия смысла у выражения x?

[Alexey Romanov]

Цитата:

Конечно бессмысленнр -- стрелочка неправильная.

Вполне нормальное обозначение для импликации, ничем не хуже $\Rightarrow$ и уж тем более $\supset$.

Nxx в сообщении #197400 писал(а):

Также ложно и высказывание, что у Маши есть возраст, поскольку возраста у нее нет.

Возраст в этой системе аксиом нигде не упоминается. Упоминается только свойство натуральных чисел $\mathrm{MashaIsOlder}(n)$.

[ewert]

Alexey Romanov в сообщении #197416 писал(а):

Вполне нормальное обозначение для импликации, ничем не хуже

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

[Nxx]

Цитата:

Возраст в этой системе аксиом нигде не упоминается. Упоминается только свойство натуральных чисел $\mathrm{MashaIsOlder}(n)$.

Так или иначе, это свойство Маши не определено, значит, его нет.

[Alexey Romanov]

ewert в сообщении #197417 писал(а):

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

Не вижу смысла менять обозначения для логических связок из-за того, какие символы входят в выражения, которые они связывают (если есть причины беспокоиться о путанице -- другое дело, но тут я их не вижу).