Существует ли...

[Профессор Снэйп]

Someone писал(а):

В главе VIII доказано, что следующие утверждения арифметики бесконечных кардинальных чисел эквивалентны аксиоме выбора:

$$\text{1) }(\mathfrak m\leqslant\mathfrak n)\vee(\mathfrak n\leqslant\mathfrak m)\text{;}$$

$$\text{2) }\mathfrak m^2=\mathfrak m\text{;}$$

$$\text{3) }(\mathfrak m\cdot\mathfrak n=\mathfrak m+\mathfrak n=\mathfrak m)\vee(\mathfrak m\cdot\mathfrak n=\mathfrak m+\mathfrak n=\mathfrak n)\text{;}$$

$$\text{4) }(\mathfrak m^2=\mathfrak n^2)\Rightarrow(\mathfrak m=\mathfrak n)\text{;}$$

$$\text{5) }((\mathfrak m<\mathfrak n)\wedge(\mathfrak p<\mathfrak q))\Rightarrow(\mathfrak m+\mathfrak n<\mathfrak p+\mathfrak q)\text{;}$$

$$\text{6) }((\mathfrak m<\mathfrak n)\wedge(\mathfrak p<\mathfrak q))\Rightarrow(\mathfrak m\cdot\mathfrak n<\mathfrak p\cdot\mathfrak q)\text{;}$$

$$\text{7) }(\mathfrak m+\mathfrak p<\mathfrak n+\mathfrak p)\Rightarrow(\mathfrak m<\mathfrak n)\text{;}$$

$$\text{8) }(\mathfrak m\cdot\mathfrak p<\mathfrak n\cdot\mathfrak p)\Rightarrow(\mathfrak m<\mathfrak n)\text{.}$$

Пп. 7 и 8 выглядят сомнительно. Может, там $\mathfrak{p} \leqslant \mathfrak{m}, \mathfrak{n}$?

Пп. 5 и 6, очевидно, тоже набраны с ошибкой. Вероятно, должно быть так:

$$\text{5) }((\mathfrak m<\mathfrak n)\wedge(\mathfrak p<\mathfrak q))\Rightarrow(\mathfrak m+\mathfrak p<\mathfrak n+\mathfrak q)\text{;}$$

$$\text{6) }((\mathfrak m<\mathfrak n)\wedge(\mathfrak p<\mathfrak q))\Rightarrow(\mathfrak m\cdot\mathfrak p<\mathfrak n\cdot\mathfrak q)\text{;}$$

[Someone]

Профессор Снэйп писал(а):

Someone писал(а):

$$\text{7) }(\mathfrak m+\mathfrak p<\mathfrak n+\mathfrak p)\Rightarrow(\mathfrak m<\mathfrak n)\text{;}$$

$$\text{8) }(\mathfrak m\cdot\mathfrak p<\mathfrak n\cdot\mathfrak p)\Rightarrow(\mathfrak m<\mathfrak n)\text{.}$$

Пп. 7 и 8 выглядят сомнительно. Может, там $\mathfrak{p} \leqslant \mathfrak{m}, \mathfrak{n}$?

Нет, в этих пунктах всё правильно. Если у нас есть аксиома выбора, то неравенство $\mathfrak m+\mathfrak p<\mathfrak n+\mathfrak p$ или $\mathfrak m\cdot\mathfrak p<\mathfrak n\cdot\mathfrak p$, разумеется, будет выполняться только при $\mathfrak m<\mathfrak n$ и $\mathfrak p<\mathfrak n$, но без аксиомы выбора всякие чудеса случаются...

Профессор Снэйп писал(а):

Пп. 5 и 6, очевидно, тоже набраны с ошибкой. Вероятно, должно быть так:

$$\text{5) }((\mathfrak m<\mathfrak n)\wedge(\mathfrak p<\mathfrak q))\Rightarrow(\mathfrak m+\mathfrak p<\mathfrak n+\mathfrak q)\text{;}$$

$$\text{6) }((\mathfrak m<\mathfrak n)\wedge(\mathfrak p<\mathfrak q))\Rightarrow(\mathfrak m\cdot\mathfrak p<\mathfrak n\cdot\mathfrak q)\text{;}$$

Да, виноват, опечатался, а проверить не удосужился. Сейчас исправлю.

[epros]

Someone писал(а):

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

В метатеории можно перечислить все КДЧ, определённые теорией

А что у Вас является метатеорией?

Мета-теория - это теория, определяющая язык, синтаксис, аксиоматику и правила вывода, применяемые в теории.

Профессор Снэйп писал(а):

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

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

"Перечисление" - это определение формулы последовательности, содержащей в качестве своих элементов все объекты соответствующего типа. По-моему, стандартно.

Перечисление в метатеории определённых теорией КДЧ - это определение формулы последовательности, содержащей в качестве своих элементов все формулы теории, определяющие КДЧ (т.е. последовательности Коши). Естественно, если метатеория может перечислить все формулы теории, то формулы, определяющие КДЧ, - тем паче.

[Someone]

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

"Перечисление" - это определение формулы последовательности, содержащей в качестве своих элементов все объекты соответствующего типа.

И не содержащей ничего лишнего.

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

Естественно, если метатеория может перечислить все формулы теории, то формулы, определяющие КДЧ, - тем паче.

Ну, "конструктивист"! Слов нет.

Конечно, в рамках классической ZFC множество КДЧ счётно, так что "перечисление" существует (совершенно неконструктивное). Но Вы ведь не хотите в качестве метатеории для CRA (конструктивного рекурсивного анализа) иметь ZFC?

[epros]

Someone писал(а):

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

"Перечисление" - это определение формулы последовательности, содержащей в качестве своих элементов все объекты соответствующего типа.

И не содержащей ничего лишнего.

Чего лишнего то? Понятие о натуральных числах - оно "лишнее", т.е. Вы лишите метатеорию умения считать?

А-аа, т.е. Вы полагаете, что избавление от "лишнего" может стать проблемой для перечисляющего алгоритма? А может Вы намекаете также на то, что из-за алгоритмической нераспознаваемости равенства некоторых КДЧ при перечислении они могут дублироваться? Ну и что? Для нас главное, чтобы каждое КДЧ получило номер, не совпадающий с номером чего-то другого. Если номер не будет уникальным, то я не вижу в этом проблемы.

Someone писал(а):

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

Естественно, если метатеория может перечислить все формулы теории, то формулы, определяющие КДЧ, - тем паче.

Ну, "конструктивист"! Слов нет.

Конечно, в рамках классической ZFC множество КДЧ счётно, так что "перечисление" существует (совершенно неконструктивное). Но Вы ведь не хотите в качестве метатеории для CRA (конструктивного рекурсивного анализа) иметь ZFC?

А я разве говорил о ZFC? Сильные аксиомы ZFC тут совершенно не причём. Чтобы пересчитать формулы, нужно всего лишь:
1. Знать, что это такое.
2. Уметь считать.

Так что в качестве метатеории для CRA и CRA вполне подойдёт. Правда алфавит и синтаксис должны быть побогаче.

[Someone]

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

Чего лишнего то?

Читаем Вашу и мою фразу подряд: «"Перечисление" - это определение формулы последовательности, содержащей в качестве своих элементов все объекты соответствующего типа и не содержащей ничего лишнего».

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

Чтобы пересчитать формулы

А КДЧ - это не формулы. Вы здесь чего-то не понимаете. Объектами CRA являются слова в фиксированном конечном алфавите и (частично) рекурсивные функции (алгоритмы), преобразующие одни слова в другие. Эти слова интерпретируются как коды различных объектов (натуральных чисел, рациональных чисел, алгоритмов, КДЧ, множеств и т.д.). Но эти коды не являются формулами CRA.
В свою очередь, метатеория, чем бы они ни была, имеет дело как раз с формулами CRA, а не с её объектами, поэтому она не может перечислять КДЧ, так как она не имеет к ним доступа. Для перечисления требуется не метатеория CRA, а расширение CRA.

[epros]

Someone писал(а):

Читаем Вашу и мою фразу подряд: «"Перечисление" - это определение формулы последовательности, содержащей в качестве своих элементов все объекты соответствующего типа и не содержащей ничего лишнего».

Согласен, что с "лишним" могут быть проблемы. Но это всего лишь вопрос определения "перечисления" - должно ли нас беспокоить "лишнее" или нет.

Someone писал(а):

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

Может я действительно чего-то не понимаю. Давайте разберёмся. Слова в заданном алфавите действительно кодируют объекты CRA. Но что такое КДЧ? Это - последовательность Коши. Например, вот такая последовательность:
$e_n = \sum\limits_{i=0}^n \frac{1}{i!}$
определяет число $e$ (предел данной последовательности: $e = \lim\limits_{n \to \infty} e_n$).

Чем определена эта последовательность? Она определена формулой теории:
$(\forall n)(e_n = \sum\limits_{i=0}^n \frac{1}{n!})$,
которая, конечно же, тоже является "словом в заданном алфавите". Но помимо того, что она просто слово, она ещё и код алгоритма, позволяющего по любому заданному $n$ вычислить $e$ с соответствующей точностью.

Someone писал(а):

В свою очередь, метатеория, чем бы они ни была, имеет дело как раз с формулами CRA, а не с её объектами, поэтому она не может перечислять КДЧ, так как она не имеет к ним доступа. Для перечисления требуется не метатеория CRA, а расширение CRA.

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

[Dandan]

а где можно подробно про CRA почитать?

[Someone]

Dandan в сообщении #204728 писал(а):

а где можно подробно про CRA почитать?

Б.А.Кушнер. Лекции по конструктивному математическому анализу. "Наука", Москва, 1973.

Кстати, я не утверждаю, что аббревиатура CRA является общепринятой. Просто она используется в статье

А.С.Трулстра. "Аспекты конструктивной математики." Справочная книга по математической логике. Часть IV. Теория доказательств и конструктивная математика. Москва, "Наука", 1983. Стр. 160 - 240.

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

Согласен, что с "лишним" могут быть проблемы. Но это всего лишь вопрос определения "перечисления" - должно ли нас беспокоить "лишнее" или нет.

Вы не знаете определения перечислимого множества? У Кушнера посмотрите. Глава 1, § 3. А Ваше "определение" совершенно бессмысленное. Если разрешить перечислять лишнее, то перечислимы будут вообще все множества, поскольку множество всех слов в заданном конечном (и даже счётном перечислимом) алфавите перечислимо.

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

Она определена формулой теории:
$(\forall n)(e_n = \sum\limits_{i=0}^n \frac{1}{n!})$,
которая, конечно же, тоже является "словом в заданном алфавите".

В CRA есть два алфавита. Один алфавит определён в метатеории. Он используется для записи формул CRA. Этот алфавит и формулы в CRA недоступны. Другой алфавит определён в CRA. Слова именно в этом алфавите являются кодами различных объектов и обрабатываются алгорифмами. Путать два этих алфавита нельзя. Теория, которая может работать со своими формулами как с объектами, очень легко оказывается противоречивой.

Возьмём, например, формулу

$$0\in\mathscr H\&\forall n(n\in\mathscr H\Rightarrow n|\in\mahtscr H)\text{.}$$

Здесь $\mathscr H$ - имя некоторого объекта CRA, определённое в языке CRA (и, следовательно, в метатеории), а в самом CRA этот объект задаётся некоторым кодом - словом в алфавите, с которым работают алгорифмы. Символы $0$ и $|$ также определены в метатеории и являются именами символов, которые используются в CRA при кодировании натуральных чисел, но не самими этими символами.

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

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

Мешает то, что объекты CRA в самом CRA задаются не формулами, а кодами. Метатеория же работает как раз с формулами, а не с кодами. Не говоря уже о том, что "перечисление с избыточностью" (то есть, включая посторонние элементы) - это не перечисление.

[epros]

Someone писал(а):

Вы не знаете определения перечислимого множества? У Кушнера посмотрите. Глава 1, § 3.

Я не стану утверждать, что в смысле этого определения КДЧ теории перечислимы в метатеории. Максимум, что можно предположить, что они "не могут не быть" перечислимыми (хотя это тоже под вопросом).

Someone писал(а):

А Ваше "определение" совершенно бессмысленное. Если разрешить перечислять лишнее, то перечислимы будут вообще все множества, поскольку множество всех слов в заданном конечном (и даже счётном перечислимом) алфавите перечислимо.

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

Someone писал(а):

В CRA есть два алфавита. Один алфавит определён в метатеории. Он используется для записи формул CRA. Этот алфавит и формулы в CRA недоступны. Другой алфавит определён в CRA. Слова именно в этом алфавите являются кодами различных объектов и обрабатываются алгорифмами. Путать два этих алфавита нельзя.

Разумеется. Алфавитов может быть даже больше двух. Например, натуральные числа могут определяться как строки в алфавите из одного символа "|". Рациональные числа могут определяться уже как строки в алфавите из двух символов: "|" и "/". Скажем, число "две третьих": "||/|||".

А вот КДЧ определяются уже как строки в алфавите, позволяющем записывать коды алгоритмов. Например, для определения "нормального алгоритма" Маркова нужны два служебных символа сверх алфавита, используемого для построения слов, которые может обрабатывать данный алгоритм.

Someone писал(а):

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

Разумеется. Поэтому с формулами теории (по крайней мере, с любыми формулами теории) может работать только метатеория.

Someone писал(а):

Возьмём, например, формулу

$$0\in\mathscr H\&\forall n(n\in\mathscr H\Rightarrow n|\in\mahtscr H)\text{.}$$

Здесь $\mathscr H$ - имя некоторого объекта CRA, определённое в языке CRA (и, следовательно, в метатеории), а в самом CRA этот объект задаётся некоторым кодом - словом в алфавите, с которым работают алгорифмы.

Как Вы думате, каким именно словом? Я напомню: это слово - есть код алгоритма, проверяющего, что предъявленная строка состоит только из символов "|" (т.е. является натуральным числом).

Someone писал(а):

Символы $0$ и $|$ также определены в метатеории и являются именами символов, которые используются в CRA при кодировании натуральных чисел, но не самими этими символами.

По-моему, вводя различия между "символами" и "именами символов", Вы всё излишне усложняете. И теория, и метатеория имеют право интерпретировать "|" просто как символ. Соответственно, строку из этих символов - как натуральное число. Понятное дело, что представления о свойствах натуральных чисел в теории и в метатеории могут быть разными. Например, некое недоказуемое в теории свойство может оказаться доказуемым в метатеории.

Someone писал(а):

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

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

Мешает то, что объекты CRA в самом CRA задаются не формулами, а кодами. Метатеория же работает как раз с формулами, а не с кодами.

Ну и что? КДЧ - это ведь последовательности Коши, а последовательности определяются формулами?

[Pi]

1. Собственно ответ на вопрос, а чем не подходит тождествественная функуия I(x)=x? Тогда I(x+y)=I(x)+I(y)=x+y.

2. А вот я не понимаю ценность конструктивизма. Из практических и теоритических задач я не могу ничего вспомнить где бы применялась конструктивисткие теории кроме одного случая - теории информационной сложности Колмогорова. И больше нигде. Поскольку конструктивизм ничего нового не дает и не облегчает и не подводит никакой базы под что либо. В общем, на мой взгляд перспектив никаких и думать что здесь может быть прорыв, это питать иллюзии.

[Someone]

epros, я прошу прощения, но с Вами обсуждать что-либо малоинтересно. Вот я сейчас думаю: Вы действительно ничего не поняли из моих объяснений или в очередной раз "включили дурочку"? За последнее время я уже как минимум три обсуждения с Вами забросил.

И опять: стоило Вам появиться в этой теме, и тут же вылезла конструктивная математика, в которой Вы разбираетесь на дилетантском уровне (даже не понимаете разницу между алфавитом, с которым работают алгорифмы, и алфавитом, в котором записываются формулы теории, формулируются и доказываются теоремы), но претендуете на обладание божественными откровениями.

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

Someone писал(а):

P.S. Просто поразительно. Стоит в какой-нибудь теме появиться Nxx или eprosу, в ней сразу начинается обсуждение актуальной бесконечности и "преимуществ" конструктивной математики. Посмотрите на название этой темы. Много ли сообщений в ней посвящено именно теореме Гёделя?

Между прочим, в этой теме об этом Вы заговорили первый, я лишь Вам отвечал.

Если почитать начало темы, то легко обнаружить, что первым был Nxx:

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

Все, что связано с абстракцией актуальной бесконечности, очевидно не имеет отношения к реальности.

Добавлено спустя 1 час 1 минуту 33 секунды:

Pi в сообщении #205053 писал(а):

Собственно ответ на вопрос, а чем не подходит тождествественная функуия I(x)=x? Тогда I(x+y)=I(x)+I(y)=x+y

Профессор Снэйп писал(а):

Существует ли биекция $f$ из $R^2$ на $R$, для которой $f(x+y) = f(x)+f(y)$?

Функция $f\colon\mathbb R^2\to\mathbb R$ не может быть тождественной просто потому, что слева и справа стоят разные множества.

Pi в сообщении #205053 писал(а):

А вот я не понимаю ценность конструктивизма. Из практических и теоритических задач я не могу ничего вспомнить где бы применялась конструктивисткие теории кроме одного случая - теории информационной сложности Колмогорова.

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

A.S.Troelstra писал(а):

In recent years (after ca. 1985) the number of contributions to CRM has considerably decreased. Many researchers in CRM have turned to more computer-science oriented topics.

(Ссылка взята здесь: http://en.wikipedia.org/wiki/Constructivism_(mathematics)).

[epros]

Someone писал(а):

epros, я прошу прощения, но с Вами обсуждать что-либо малоинтересно. Вот я сейчас думаю: Вы действительно ничего не поняли из моих объяснений или в очередной раз "включили дурочку"? За последнее время я уже как минимум три обсуждения с Вами забросил.

И опять: стоило Вам появиться в этой теме, и тут же вылезла конструктивная математика, в которой Вы разбираетесь на дилетантском уровне (даже не понимаете разницу между алфавитом, с которым работают алгорифмы, и алфавитом, в котором записываются формулы теории, формулируются и доказываются теоремы), но претендуете на обладание божественными откровениями.

Стало быть, когда по существу сказать нечего, начинаются наезды на предмет "дилетантского уровня" и т.п.? Я не претендую ни на "божественное откровение", ни даже на профессиональное понимание вопроса. Но у Вас-то, Someone, даже понимание базовых концепций конструктивности по-моему отсутствует (хотя в других вопросах, возможно, Вы и профессионал). Чего бы уж проще, казалось бы, понять, что если математика - это "игра в буковки", то стало быть конструктивно только буковки и рассматривать, а не то, что за ними якобы "реально стоит". Но Вы, похоже, твёрдо следуете "классической" традиции, согласно которой математические объекты якобы существуют в некоем "идеальном мире" (даже если это - мир фантазий "профессионального математика"), а то, что изложено на бумаге - всего лишь "обозначения" этих объектов. И меряете конструктивизм той же линейкой. Наверное поэтому Вы в очередной раз не услышали то, что я сказал относительно различий алфавитов (с которыми работают алгоритмы, в которых записыватся алгоритмы и в которых записываются теории).

[Pi]

Как я понял все отличие конструктивисткой логики от классической только в том что в классической логике используется булева (двоичная) алгебра, а в конструктивисткой - троичная алгебра (1/2 - "не известно" ). Отсюдо отсутствие "закона исключенного третьего" и "двойтого отрицания". Что собственно допустимо, непротиворичиво, это таже логика первого порядка - поэтому ничего нового она добавить не может.
Как я уже говорил тогда первым конструктивистом был Льюис Кэррол.
Поскольку она слабее булевой логики смысла для развития математики в ней большого нет. Все логики первого порядка достаточно равнозначны. Только в некотрых вопросах чистой логики высказываний она может пригодиться. И конечно ломать копья по этому поводу совершенно неинтересно. Например куда интересней логика более высокого порядка построенная на нечетких множествах.

[epros]

Pi писал(а):

а в конструктивисткой - троичная алгебра (1/2 - "не известно" )

Конструктивная логика - не троичная.

Pi писал(а):

И конечно ломать копья по этому поводу совершенно неинтересно.

Вот ведь фигня какая: Собрались "неконструктивисты" и давай рассуждать, что "это никому не нужно", да "этим никто не пользуется"...